Metamath Proof Explorer

Theorem el0ldepsnzr

Description: A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

Ref Expression
Assertion el0ldepsnzr 
|- ( ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> M e. LMod )
2 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
3 2 isnzr2hash 
 |-  ( ( Scalar ` M ) e. NzRing <-> ( ( Scalar ` M ) e. Ring /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) )
4 3 simprbi 
 |-  ( ( Scalar ` M ) e. NzRing -> 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) )
5 4 adantl 
 |-  ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) -> 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) )
6 5 3ad2ant1 
 |-  ( ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) )
7 1 6 jca 
 |-  ( ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) )
8 el0ldep 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )
9 7 8 syld3an1 
 |-  ( ( ( M e. LMod /\ ( Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )