ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
⊢ ¬v x ∈ span R (v '' s)
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
⊢ ¬v x ∈ span R (v '' s)
have h' : v x ∈ Submodule.span R (v '' {x}) := by
  rw [Set.image_singleton]
  exact mem_span_singleton_self (v x)
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
⊢ ¬v x ∈ span R (v '' s)
intro w
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ v x = 0
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False
apply LinearIndependent.ne_zero x hv
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ Disjoint {x} s
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ v x = 0
refine' disjoint_def.1 (hv.disjoint_span_image _) (v x) h' w
no goals
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ Disjoint {x} s
simpa using h
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
⊢ v x ∈ span R {v x}
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
⊢ v x ∈ span R (v '' {x})
rw [Set.image_singleton]
no goals
ι : Type u'
ι' : Type ?u.344052
R : Type u_1
K : Type ?u.344058
M : Type u_2
M' : Type ?u.344064
M'' : Type ?u.344067
V : Type u
V' : Type ?u.344072
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : ¬x ∈ s
⊢ v x ∈ span R {v x}
exact mem_span_singleton_self (v x)