case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
⊢ K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂
ext x
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
rw [Submodule.mem_sup]
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
let v : K₁ := orthogonalProjection K₁ x
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
have hvm : x - v ∈ K₁ᗮ := sub_orthogonalProjection_mem_orthogonal x
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) → x ∈ K₂

case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) ↔ x ∈ K₂
constructor
case h.mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) (y + z)
hvm : y + z - ↑v ∈ K₁ᗮ
⊢ y + z ∈ K₂
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ (∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x) → x ∈ K₂
rintro ⟨y, hy, z, hz, rfl⟩
no goals
case h.mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) (y + z)
hvm : y + z - ↑v ∈ K₁ᗮ
⊢ y + z ∈ K₂
exact K₂.add_mem (h hy) hz.2
no goals
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.757872
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : CompleteSpace { x // x ∈ K₁ }
x : E
v : { x // x ∈ K₁ } := ↑(orthogonalProjection K₁) x
hvm : x - ↑v ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y, y ∈ K₁ ∧ ∃ z, z ∈ K₁ᗮ ⊓ K₂ ∧ y + z = x
exact fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel'_right _ _⟩