case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ w = ↑(↑(orthogonalProjection K) w) + ↑(↑(orthogonalProjection Kᗮ) w)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w : E
⊢ w = ↑(↑(orthogonalProjection K) w) + ↑(↑(orthogonalProjection Kᗮ) w)
obtain ⟨y, hy, z, hz, hwyz⟩ := K.exists_sum_mem_mem_orthogonal w
case h.e'_3.h.e'_5
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ ↑(↑(orthogonalProjection K) w) = y

case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ ↑(↑(orthogonalProjection Kᗮ) w) = z
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ w = ↑(↑(orthogonalProjection K) w) + ↑(↑(orthogonalProjection Kᗮ) w)
convert hwyz
no goals
case h.e'_3.h.e'_5
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ ↑(↑(orthogonalProjection K) w) = y
exact eq_orthogonalProjection_of_mem_orthogonal' hy hz hwyz
case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = z + y
⊢ ↑(↑(orthogonalProjection Kᗮ) w) = z
case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = y + z
⊢ ↑(↑(orthogonalProjection Kᗮ) w) = z
rw [add_comm] at hwyz
case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = z + y
⊢ y ∈ Kᗮᗮ
case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = z + y
⊢ ↑(↑(orthogonalProjection Kᗮ) w) = z
refine' eq_orthogonalProjection_of_mem_orthogonal' hz _ hwyz
no goals
case h.e'_3.h.e'_6
𝕜 : Type u_2
E : Type u_1
F : Type ?u.946458
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hwyz : w = z + y
⊢ y ∈ Kᗮᗮ
simp [hy]