K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator (dualAnnihilator W) ≤ W
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator (dualAnnihilator W) = W
refine' le_antisymm _ (le_dualAnnihilator_dualCoannihilator _)
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∈ dualCoannihilator (dualAnnihilator W) → v ∈ W
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator (dualAnnihilator W) ≤ W
intro v
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ (φ : Module.Dual K V), (∀ (w : V), w ∈ W → ↑φ w = 0) → ↑φ v = 0) → v ∈ W
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∈ dualCoannihilator (dualAnnihilator W) → v ∈ W
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ ¬v ∈ W → ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ (φ : Module.Dual K V), (∀ (w : V), w ∈ W → ↑φ w = 0) → ↑φ v = 0) → v ∈ W
contrapose!
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ ¬v ∈ W → ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
intro hv
case intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
W' : Submodule K V
hW : IsCompl W W'
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
obtain ⟨W', hW⟩ := Submodule.exists_isCompl W
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
W' : Submodule K V
hW : IsCompl W W'
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
obtain ⟨⟨w, w'⟩, rfl, -⟩ := existsUnique_add_of_isCompl_prod hW v
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
have hw'n : (w' : V) ∉ W := by
  contrapose! hv
  exact Submodule.add_mem W w.2 hv
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
have hw'nz : w' ≠ 0 := by
  rintro rfl
  exact hw'n (Submodule.zero_mem W)
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ¬∀ (φ : Module.Dual K { x // x ∈ W' }), ↑φ w' = 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
rw [Ne.def, ← Module.forall_dual_apply_eq_zero_iff K w'] at hw'nz
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ∃ φ, ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ¬∀ (φ : Module.Dual K { x // x ∈ W' }), ↑φ w' = 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
push_neg  at hw'nz
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ∃ φ, ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
obtain ⟨φ, hφ⟩ := hw'nz
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V),
      w ∈ W → ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ) w = 0) ∧
    ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ)
        (↑(w, w').fst + ↑(w, w').snd) ≠
      0
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
exists ((LinearMap.ofIsComplProd hW).comp (LinearMap.inr _ _ _)) φ
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0) ∧ ¬↑φ w' = 0
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V),
      w ∈ W → ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ) w = 0) ∧
    ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ)
        (↑(w, w').fst + ↑(w, w').snd) ≠
      0
simp only [coe_comp, coe_inr, Function.comp_apply, ofIsComplProd_apply, map_add,
  ofIsCompl_left_apply, zero_apply, ofIsCompl_right_apply, zero_add, Ne.def]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0) ∧ ¬↑φ w' = 0
refine' ⟨_, hφ⟩
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv✝ : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
v : V
hv : v ∈ W
⊢ ↑(ofIsCompl hW 0 φ) v = 0
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0
intro v hv
no goals
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv✝ : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
v : V
hv : v ∈ W
⊢ ↑(ofIsCompl hW 0 φ) v = 0
apply LinearMap.ofIsCompl_left_apply hW ⟨v, hv⟩
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ↑w' ∈ W
⊢ ↑w + ↑w' ∈ W
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
⊢ ¬↑w' ∈ W
contrapose! hv
no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ↑w' ∈ W
⊢ ↑w + ↑w' ∈ W
exact Submodule.add_mem W w.2 hv
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
hv : ¬↑(w, 0).fst + ↑(w, 0).snd ∈ W
hw'n : ¬↑0 ∈ W
⊢ False
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
⊢ w' ≠ 0
rintro rfl
no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
hv : ¬↑(w, 0).fst + ↑(w, 0).snd ∈ W
hw'n : ¬↑0 ∈ W
⊢ False
exact hw'n (Submodule.zero_mem W)