case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.813852
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
h : ContinuousLinearMap.comp (orthogonalProjection U) (Submodule.subtypeL V) = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ v = v - ↑(↑(orthogonalProjection U) v)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.813852
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
h : ContinuousLinearMap.comp (orthogonalProjection U) (Submodule.subtypeL V) = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ inner v u = 0
convert orthogonalProjection_inner_eq_zero v u hu using 2
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.813852
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
h : ContinuousLinearMap.comp (orthogonalProjection U) (Submodule.subtypeL V) = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
this : ↑(orthogonalProjection U) v = 0
⊢ v = v - ↑(↑(orthogonalProjection U) v)
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.813852
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
h : ContinuousLinearMap.comp (orthogonalProjection U) (Submodule.subtypeL V) = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ v = v - ↑(↑(orthogonalProjection U) v)
have : orthogonalProjection U v = 0 := FunLike.congr_fun h (⟨_, hv⟩ : V)
no goals
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.813852
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
h : ContinuousLinearMap.comp (orthogonalProjection U) (Submodule.subtypeL V) = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
this : ↑(orthogonalProjection U) v = 0
⊢ v = v - ↑(↑(orthogonalProjection U) v)
rw [this, Submodule.coe_zero, sub_zero]