Metamath Proof Explorer

Theorem lindszr

Description: Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019)

Ref Expression
Assertion lindszr ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → S linIndS M

Proof

Step Hyp Ref Expression
1 simp2 ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → ¬ Scalar ⁡ M ∈ NzRing
2 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
3 2 lmodring ⊢ M ∈ LMod → Scalar ⁡ M ∈ Ring
4 3 3ad2ant1 ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → Scalar ⁡ M ∈ Ring
5 0ringnnzr ⊢ Scalar ⁡ M ∈ Ring → Base Scalar ⁡ M = 1 ↔ ¬ Scalar ⁡ M ∈ NzRing
6 4 5 syl ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → Base Scalar ⁡ M = 1 ↔ ¬ Scalar ⁡ M ∈ NzRing
7 1 6 mpbird ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → Base Scalar ⁡ M = 1
8 7 olcd ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → Base Scalar ⁡ M = 0 ∨ Base Scalar ⁡ M = 1
9 eqid ⊢ Base M = Base M
10 eqid ⊢ Base Scalar ⁡ M = Base Scalar ⁡ M
11 9 2 10 lindsrng01 ⊢ M ∈ LMod ∧ Base Scalar ⁡ M = 0 ∨ Base Scalar ⁡ M = 1 ∧ S ∈ 𝒫 Base M → S linIndS M
12 8 11 syld3an2 ⊢ M ∈ LMod ∧ ¬ Scalar ⁡ M ∈ NzRing ∧ S ∈ 𝒫 Base M → S linIndS M