ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
⊢ Disjoint ((fun i => span R {v i}) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j)
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
⊢ CompleteLattice.Independent fun i => span R {v i}
refine' CompleteLattice.independent_def.mp fun i => _
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
⊢ ((fun i => span R {v i}) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j) ≤ ⊥
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
⊢ Disjoint ((fun i => span R {v i}) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j)
rw [disjoint_iff_inf_le]
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
m : M
hm : m ∈ (fun i => span R {v i}) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j
⊢ m ∈ ⊥
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
⊢ ((fun i => span R {v i}) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j) ≤ ⊥
intro m hm
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ span R (range fun i_1 => v ↑i_1)
⊢ m ∈ ⊥
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
m : M
hm : m ∈ (fun i => span R {v i}) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => span R {v i}) j
⊢ m ∈ ⊥
simp only [mem_inf, mem_span_singleton, iSup_subtype', ← span_range_eq_iSup] at hm
case intro.intro
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r • v i ∈ ⊥
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ span R (range fun i_1 => v ↑i_1)
⊢ m ∈ ⊥
obtain ⟨⟨r, rfl⟩, hm⟩ := hm
case intro.intro
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r = 0
case intro.intro
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r • v i ∈ ⊥
suffices r = 0 by simp [this]
case intro.intro.a
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r • v i ∈ span R (v '' (univ \ {i}))
case intro.intro
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r = 0
apply linearIndependent_iff_not_smul_mem_span.mp hv i
case intro.intro.a
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ v '' (univ \ {i}) = range fun j => v ↑j
case intro.intro.a
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ r • v i ∈ span R (v '' (univ \ {i}))
suffices v '' (univ \ {i}) = range fun j : { j // j ≠ i } => v j by rwa [this]
case intro.intro.a.h
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
x✝ : M
⊢ x✝ ∈ v '' (univ \ {i}) ↔ x✝ ∈ range fun j => v ↑j
case intro.intro.a
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
⊢ v '' (univ \ {i}) = range fun j => v ↑j
ext
no goals
case intro.intro.a.h
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
x✝ : M
⊢ x✝ ∈ v '' (univ \ {i}) ↔ x✝ ∈ range fun j => v ↑j
simp
no goals
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
this : r = 0
⊢ r • v i ∈ ⊥
simp [this]
no goals
ι : Type u'
ι' : Type ?u.484575
R : Type u_1
K : Type ?u.484581
M : Type u_2
M' : Type ?u.484587
M'' : Type ?u.484590
V : Type u
V' : Type ?u.484595
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun i_1 => v ↑i_1)
this : v '' (univ \ {i}) = range fun j => v ↑j
⊢ r • v i ∈ span R (v '' (univ \ {i}))
rwa [this]