ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) ↔ ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ LinearIndependent K v ↔ ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
apply linearIndependent_iff_not_smul_mem_span.trans
case mp
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) → ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))

case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))) → ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) ↔ ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
constructor
case mp
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ False
case mp
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) → ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
intro h i h_in_span
no goals
case mp
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ False
apply one_ne_zero (h i 1 (by simp [h_in_span]))
no goals
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ 1 • v i ∈ span K (v '' (univ \ {i}))
simp [h_in_span]
case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
i : ι
a : K
ha : a • v i ∈ span K (v '' (univ \ {i}))
⊢ a = 0
case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ (∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))) → ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
intro h i a ha
case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
i : ι
a : K
ha : a • v i ∈ span K (v '' (univ \ {i}))
ha' : ¬a = 0
⊢ False
case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
i : ι
a : K
ha : a • v i ∈ span K (v '' (univ \ {i}))
⊢ a = 0
by_contra ha'
no goals
case mpr
ι : Type u'
ι' : Type ?u.1204971
R : Type ?u.1204974
K : Type u_1
M : Type ?u.1204980
M' : Type ?u.1204983
M'' : Type ?u.1204986
V : Type u
V' : Type ?u.1204991
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
h : ∀ (i : ι), ¬v i ∈ span K (v '' (univ \ {i}))
i : ι
a : K
ha : a • v i ∈ span K (v '' (univ \ {i}))
ha' : ¬a = 0
⊢ False
exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))