[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
a✝ b✝ : E
hx : a✝ ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0}
hy : b✝ ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0}
u : E
hu : u ∈ K
⊢ inner u (a✝ + b✝) = 0
[PROOFSTEP]
rw [inner_add_right, hx u hu, hy u hu, add_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
c : 𝕜
x : E
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {v | ∀ (u : E), u ∈ K → inner u v = 0},
              add_mem' :=
                (_ :
                  ∀ {a b : E},
                    a ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0} →
                      b ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0} → ∀ (u : E), u ∈ K → inner u (a + b) = 0) },
          zero_mem' := (_ : ∀ (x : E), x ∈ K → inner x 0 = 0) }.toAddSubsemigroup.carrier
u : E
hu : u ∈ K
⊢ inner u (c • x) = 0
[PROOFSTEP]
rw [inner_smul_right, hx u hu, mul_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → inner v u = 0
[PROOFSTEP]
simp_rw [mem_orthogonal, inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner v u = 0
[PROOFSTEP]
rw [inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner u v = 0
[PROOFSTEP]
exact inner_right_of_mem_orthogonal hu hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner u v = 0
[PROOFSTEP]
refine' ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ inner u v = 0 → v ∈ (span 𝕜 {u})ᗮ
[PROOFSTEP]
intro hv w hw
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : w ∈ span 𝕜 {u}
⊢ inner w v = 0
[PROOFSTEP]
rw [mem_span_singleton] at hw 
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : ∃ a, a • u = w
⊢ inner w v = 0
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hw
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
c : 𝕜
⊢ inner (c • u) v = 0
[PROOFSTEP]
simp [inner_smul_left, hv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner v u = 0
[PROOFSTEP]
rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ x - y ∈ Kᗮ
[PROOFSTEP]
rw [mem_orthogonal']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ ∀ (u : E), u ∈ K → inner (x - y) u = 0
[PROOFSTEP]
intro u hu
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0
[PROOFSTEP]
rw [inner_sub_left, sub_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u
[PROOFSTEP]
exact h ⟨u, hu⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
⊢ x - y ∈ Kᗮ
[PROOFSTEP]
intro u hu
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0
[PROOFSTEP]
rw [inner_sub_right, sub_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y
[PROOFSTEP]
exact h ⟨u, hu⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥
[PROOFSTEP]
rw [mem_inf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥
[PROOFSTEP]
exact fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Disjoint K Kᗮ
[PROOFSTEP]
simp [disjoint_iff, K.inf_orthogonal_eq_bot]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
[PROOFSTEP]
rw [le_iInf_iff]
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (i : { x // x ∈ K }), Kᗮ ≤ LinearMap.ker (↑(innerSL 𝕜) ↑i)
[PROOFSTEP]
rintro ⟨v, hv⟩ w hw
[GOAL]
case a.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker (↑(innerSL 𝕜) ↑{ val := v, property := hv })
[PROOFSTEP]
simpa using hw _ hv
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v) ≤ Kᗮ
[PROOFSTEP]
intro v hv w hw
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0
[PROOFSTEP]
simp only [mem_iInf] at hv 
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : { x // x ∈ K }), v ∈ LinearMap.ker (↑(innerSL 𝕜) ↑i)
⊢ inner w v = 0
[PROOFSTEP]
exact hv ⟨w, hw⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑Kᗮ
[PROOFSTEP]
rw [orthogonal_eq_inter K]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
[PROOFSTEP]
have := fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
[PROOFSTEP]
convert isClosed_iInter this
[GOAL]
case h.e'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) =
    ⋂ (i : { x // x ∈ K }), ↑(LinearMap.ker (↑(innerSL 𝕜) ↑i))
[PROOFSTEP]
simp only [iInf_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊤ᗮ = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ ⊤ᗮ ↔ x ∈ ⊥
[PROOFSTEP]
rw [mem_bot, mem_orthogonal]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ (∀ (u : E), u ∈ ⊤ → inner u x = 0) ↔ x = 0
[PROOFSTEP]
exact
  ⟨fun h => inner_self_eq_zero.mp (h x mem_top), by
    rintro rfl
    simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x = 0 → ∀ (u : E), u ∈ ⊤ → inner u x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (u : E), u ∈ ⊤ → inner u 0 = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊥ᗮ = ⊤
[PROOFSTEP]
rw [← top_orthogonal_eq_bot, eq_top_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊤ ≤ ⊤ᗮᗮ
[PROOFSTEP]
exact le_orthogonal_orthogonal ⊤
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ ↔ K = ⊥
[PROOFSTEP]
refine'
  ⟨_, by
    rintro rfl
    exact bot_orthogonal_eq_top⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K = ⊥ → Kᗮ = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
⊢ ⊥ᗮ = ⊤
[PROOFSTEP]
exact bot_orthogonal_eq_top
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ → K = ⊥
[PROOFSTEP]
intro h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥
[PROOFSTEP]
have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
h : Kᗮ = ⊤
this : K ⊓ Kᗮ = ⊥
⊢ K = ⊥
[PROOFSTEP]
rwa [h, inf_comm, top_inf_eq] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
U : Submodule 𝕜 E
V : Set (Submodule 𝕜 E)
⊢ (∀ (Uᵢ : Submodule 𝕜 E), Uᵢ ∈ V → Uᵢ ⟂ U) ↔ ∀ (Vᵢ : Submodule 𝕜 E), Vᵢ ∈ V → U ⟂ Vᵢ
[PROOFSTEP]
simp_rw [isOrtho_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
ι : Sort u_4
U : Submodule 𝕜 E
V : ι → Submodule 𝕜 E
⊢ (∀ (i : ι), V i ⟂ U) ↔ ∀ (i : ι), U ⟂ V i
[PROOFSTEP]
simp_rw [isOrtho_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
s t : Set E
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → inner u v = 0
[PROOFSTEP]
simp_rw [span_eq_iSup_of_singleton_spans s, span_eq_iSup_of_singleton_spans t, isOrtho_iSup_left, isOrtho_iSup_right,
  isOrtho_iff_le, span_le, Set.subset_def, SetLike.mem_coe, mem_orthogonal_singleton_iff_inner_left,
  Set.mem_singleton_iff, forall_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ Submodule.map f U ⟂ Submodule.map f V
[PROOFSTEP]
rw [isOrtho_iff_inner_eq] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (u : F), u ∈ Submodule.map f U → ∀ (v : F), v ∈ Submodule.map f V → inner u v = 0
[PROOFSTEP]
simp_rw [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, LinearIsometry.inner_map_map]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (a : E), a ∈ U → ∀ (a_2 : E), a_2 ∈ V → inner a a_2 = 0
[PROOFSTEP]
exact h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : U ⟂ V
⊢ Submodule.comap f U ⟂ Submodule.comap f V
[PROOFSTEP]
rw [isOrtho_iff_inner_eq] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), u ∈ Submodule.comap f U → ∀ (v : E), v ∈ Submodule.comap f V → inner u v = 0
[PROOFSTEP]
simp_rw [mem_comap, ← f.inner_map_map]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → inner (↑f u) (↑f v) = 0
[PROOFSTEP]
intro u hu v hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
u : E
hu : ↑f u ∈ U
v : E
hv : ↑f v ∈ V
⊢ inner (↑f u) (↑f v) = 0
[PROOFSTEP]
exact h _ hu _ hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
⊢ U ⟂ V
[PROOFSTEP]
have hf : ∀ p : Submodule 𝕜 E, (p.map f).comap f.toLinearIsometry = p := comap_map_eq_of_injective f.injective
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap (LinearIsometryEquiv.toLinearIsometry f) (Submodule.map f p) = p
⊢ U ⟂ V
[PROOFSTEP]
simpa only [hf] using h.comap f.toLinearIsometry
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
⊢ U ⟂ V
[PROOFSTEP]
have hf : ∀ p : Submodule 𝕜 F, (p.comap f).map f.toLinearIsometry = p := map_comap_eq_of_surjective f.surjective
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
hf : ∀ (p : Submodule 𝕜 F), Submodule.map (LinearIsometryEquiv.toLinearIsometry f) (Submodule.comap f p) = p
⊢ U ⟂ V
[PROOFSTEP]
simpa only [hf] using h.map f.toLinearIsometry
