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 e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> S linIndS M )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> -. ( Scalar ` M ) e. NzRing )
2 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
3 2 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
4 3 3ad2ant1 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> ( Scalar ` M ) e. Ring )
5 0ringnnzr 
 |-  ( ( Scalar ` M ) e. Ring -> ( ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 <-> -. ( Scalar ` M ) e. NzRing ) )
6 4 5 syl 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> ( ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 <-> -. ( Scalar ` M ) e. NzRing ) )
7 1 6 mpbird 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 )
8 7 olcd 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( 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 e. LMod /\ ( ( # ` ( Base ` ( Scalar ` M ) ) ) = 0 \/ ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 ) /\ S e. ~P ( Base ` M ) ) -> S linIndS M )
12 8 11 syld3an2 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> S linIndS M )