𝕜 : Type u_2
E : Type u_1
F : Type ?u.635187
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = ↑(‖v‖ ^ 2) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.635187
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = inner v w • v
rw [← smul_orthogonalProjection_singleton 𝕜 w]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.635187
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w) = ↑(‖v‖ ^ 2) • ↑(↑(orthogonalProjection (Submodule.span 𝕜 {v})) w)
simp [hv]