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