Metamath Proof Explorer

Theorem lmod0rng

Description: If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019)

Ref Expression
Assertion lmod0rng 
|- ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing ) -> ( Base ` M ) = { ( 0g ` M ) } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
2 1 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
3 0ringnnzr 
 |-  ( ( Scalar ` M ) e. Ring -> ( ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 <-> -. ( Scalar ` M ) e. NzRing ) )
4 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
5 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
6 eqid 
 |-  ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) )
7 4 5 6 0ring01eq 
 |-  ( ( ( Scalar ` M ) e. Ring /\ ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 ) -> ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) )
8 eqid 
 |-  ( Base ` M ) = ( Base ` M )
9 eqid 
 |-  ( .s ` M ) = ( .s ` M )
10 8 1 9 6 lmodvs1 
 |-  ( ( M e. LMod /\ v e. ( Base ` M ) ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = v )
11 eqcom 
 |-  ( ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = v <-> v = ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) )
12 11 biimpi 
 |-  ( ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = v -> v = ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) )
13 oveq1 
 |-  ( ( 1r ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = ( ( 0g ` ( Scalar ` M ) ) ( .s ` M ) v ) )
14 13 eqcoms 
 |-  ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = ( ( 0g ` ( Scalar ` M ) ) ( .s ` M ) v ) )
15 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
16 8 1 9 5 15 lmod0vs 
 |-  ( ( M e. LMod /\ v e. ( Base ` M ) ) -> ( ( 0g ` ( Scalar ` M ) ) ( .s ` M ) v ) = ( 0g ` M ) )
17 14 16 sylan9eqr 
 |-  ( ( ( M e. LMod /\ v e. ( Base ` M ) ) /\ ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = ( 0g ` M ) )
18 12 17 sylan9eq 
 |-  ( ( ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = v /\ ( ( M e. LMod /\ v e. ( Base ` M ) ) /\ ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) ) ) -> v = ( 0g ` M ) )
19 18 exp32 
 |-  ( ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) v ) = v -> ( ( M e. LMod /\ v e. ( Base ` M ) ) -> ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) -> v = ( 0g ` M ) ) ) )
20 10 19 mpcom 
 |-  ( ( M e. LMod /\ v e. ( Base ` M ) ) -> ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) -> v = ( 0g ` M ) ) )
21 20 com12 
 |-  ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) -> ( ( M e. LMod /\ v e. ( Base ` M ) ) -> v = ( 0g ` M ) ) )
22 21 impl 
 |-  ( ( ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) /\ M e. LMod ) /\ v e. ( Base ` M ) ) -> v = ( 0g ` M ) )
23 22 ralrimiva 
 |-  ( ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) /\ M e. LMod ) -> A. v e. ( Base ` M ) v = ( 0g ` M ) )
24 8 lmodbn0 
 |-  ( M e. LMod -> ( Base ` M ) =/= (/) )
25 eqsn 
 |-  ( ( Base ` M ) =/= (/) -> ( ( Base ` M ) = { ( 0g ` M ) } <-> A. v e. ( Base ` M ) v = ( 0g ` M ) ) )
26 24 25 syl 
 |-  ( M e. LMod -> ( ( Base ` M ) = { ( 0g ` M ) } <-> A. v e. ( Base ` M ) v = ( 0g ` M ) ) )
27 26 adantl 
 |-  ( ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) /\ M e. LMod ) -> ( ( Base ` M ) = { ( 0g ` M ) } <-> A. v e. ( Base ` M ) v = ( 0g ` M ) ) )
28 23 27 mpbird 
 |-  ( ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) /\ M e. LMod ) -> ( Base ` M ) = { ( 0g ` M ) } )
29 28 ex 
 |-  ( ( 0g ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) ) -> ( M e. LMod -> ( Base ` M ) = { ( 0g ` M ) } ) )
30 7 29 syl 
 |-  ( ( ( Scalar ` M ) e. Ring /\ ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 ) -> ( M e. LMod -> ( Base ` M ) = { ( 0g ` M ) } ) )
31 30 ex 
 |-  ( ( Scalar ` M ) e. Ring -> ( ( # ` ( Base ` ( Scalar ` M ) ) ) = 1 -> ( M e. LMod -> ( Base ` M ) = { ( 0g ` M ) } ) ) )
32 3 31 sylbird 
 |-  ( ( Scalar ` M ) e. Ring -> ( -. ( Scalar ` M ) e. NzRing -> ( M e. LMod -> ( Base ` M ) = { ( 0g ` M ) } ) ) )
33 32 com23 
 |-  ( ( Scalar ` M ) e. Ring -> ( M e. LMod -> ( -. ( Scalar ` M ) e. NzRing -> ( Base ` M ) = { ( 0g ` M ) } ) ) )
34 2 33 mpcom 
 |-  ( M e. LMod -> ( -. ( Scalar ` M ) e. NzRing -> ( Base ` M ) = { ( 0g ` M ) } ) )
35 34 imp 
 |-  ( ( M e. LMod /\ -. ( Scalar ` M ) e. NzRing ) -> ( Base ` M ) = { ( 0g ` M ) } )