R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
⊢ (x ∈ s → x = 0) → ∀ (x_1 : E), x_1 ∈ s → x_1 ∈ span K {x} → x_1 = 0
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
⊢ Disjoint s (span K {x}) ↔ x ∈ s → x = 0
refine' disjoint_def.trans ⟨fun H hx => H x hx <| subset_span <| mem_singleton x, _⟩
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
y : E
hy : y ∈ s
hyx : y ∈ span K {x}
⊢ y = 0
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
⊢ (x ∈ s → x = 0) → ∀ (x_1 : E), x_1 ∈ s → x_1 ∈ span K {x} → x_1 = 0
intro H y hy hyx
case intro
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
⊢ c • x = 0
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
y : E
hy : y ∈ s
hyx : y ∈ span K {x}
⊢ y = 0
obtain ⟨c, rfl⟩ := mem_span_singleton.1 hyx
case pos
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : c = 0
⊢ c • x = 0

case neg
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0
case intro
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
⊢ c • x = 0
by_cases hc : c = 0
no goals
case pos
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : c = 0
⊢ c • x = 0
rw [hc, zero_smul]
case neg
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0
case neg
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0
rw [s.smul_mem_iff hc] at hy
no goals
case neg
R : Type ?u.153486
R₂ : Type ?u.153489
K✝ : Type ?u.153492
M : Type ?u.153495
M₂ : Type ?u.153498
V : Type ?u.153501
S : Type ?u.153504
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x✝ : M
p p' : Submodule R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
s✝ t : Set M
K : Type u_1
E : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup E
inst✝ : Module K E
s : Submodule K E
x : E
H : x ∈ s → x = 0
c : K
hy : x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0
rw [H hy, smul_zero]