𝕜 : Type u_2
E : Type u_1
F : Type ?u.498264
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
hw : w ∈ K
⊢ inner w (v - ↑(↑(orthogonalProjection K) v)) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.498264
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v - ↑(↑(orthogonalProjection K) v) ∈ Kᗮ
intro w hw
𝕜 : Type u_2
E : Type u_1
F : Type ?u.498264
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
hw : w ∈ K
⊢ inner (v - ↑(↑(orthogonalProjection K) v)) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.498264
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
hw : w ∈ K
⊢ inner w (v - ↑(↑(orthogonalProjection K) v)) = 0
rw [inner_eq_zero_symm]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.498264
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v w : E
hw : w ∈ K
⊢ inner (v - ↑(↑(orthogonalProjection K) v)) w = 0
exact orthogonalProjection_inner_eq_zero _ _ hw