𝕜 : Type u_2
E : Type u_1
F : Type ?u.822903
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
this : IsCompl K Kᗮ
⊢ ↑(orthogonalProjection K) x = ↑(Submodule.linearProjOfIsCompl K Kᗮ (_ : IsCompl K Kᗮ)) x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.822903
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ ↑(orthogonalProjection K) x = ↑(Submodule.linearProjOfIsCompl K Kᗮ (_ : IsCompl K Kᗮ)) x
have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_completeSpace
𝕜 : Type u_2
E : Type u_1
F : Type ?u.822903
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
this : IsCompl K Kᗮ
⊢ ↑(orthogonalProjection K)
      (↑(↑(Submodule.linearProjOfIsCompl K Kᗮ this) x) +
        ↑(↑(Submodule.linearProjOfIsCompl Kᗮ K (_ : IsCompl Kᗮ K)) x)) =
    ↑(Submodule.linearProjOfIsCompl K Kᗮ (_ : IsCompl K Kᗮ)) x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.822903
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
this : IsCompl K Kᗮ
⊢ ↑(orthogonalProjection K) x = ↑(Submodule.linearProjOfIsCompl K Kᗮ (_ : IsCompl K Kᗮ)) x
conv_lhs => rw [← Submodule.linear_proj_add_linearProjOfIsCompl_eq_self this x]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.822903
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
this : IsCompl K Kᗮ
⊢ ↑(orthogonalProjection K)
      (↑(↑(Submodule.linearProjOfIsCompl K Kᗮ this) x) +
        ↑(↑(Submodule.linearProjOfIsCompl Kᗮ K (_ : IsCompl Kᗮ K)) x)) =
    ↑(Submodule.linearProjOfIsCompl K Kᗮ (_ : IsCompl K Kᗮ)) x
rw [map_add, orthogonalProjection_mem_subspace_eq_self,
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]