Metamath Proof Explorer

Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 01eq0ring 
|- ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )

Proof

Step Hyp Ref Expression
1 0ring.b 
 |-  B = ( Base ` R )
2 0ring.0 
 |-  .0. = ( 0g ` R )
3 0ring01eq.1 
 |-  .1. = ( 1r ` R )
4 1 fvexi 
 |-  B e. _V
5 hashv01gt1 
 |-  ( B e. _V -> ( ( # ` B ) = 0 \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) ) )
6 4 5 ax-mp 
 |-  ( ( # ` B ) = 0 \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) )
7 hasheq0 
 |-  ( B e. _V -> ( ( # ` B ) = 0 <-> B = (/) ) )
8 4 7 ax-mp 
 |-  ( ( # ` B ) = 0 <-> B = (/) )
9 ne0i 
 |-  ( .0. e. B -> B =/= (/) )
10 eqneqall 
 |-  ( B = (/) -> ( B =/= (/) -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
11 9 10 syl5com 
 |-  ( .0. e. B -> ( B = (/) -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
12 8 11 syl5bi 
 |-  ( .0. e. B -> ( ( # ` B ) = 0 -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
13 1 2 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
14 12 13 syl11 
 |-  ( ( # ` B ) = 0 -> ( R e. Ring -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
15 eqneqall 
 |-  ( ( # ` B ) = 1 -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) )
16 15 a1d 
 |-  ( ( # ` B ) = 1 -> ( R e. Ring -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
17 1 3 2 ring1ne0 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .1. =/= .0. )
18 17 necomd 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .0. =/= .1. )
19 18 ex 
 |-  ( R e. Ring -> ( 1 < ( # ` B ) -> .0. =/= .1. ) )
20 19 a1i 
 |-  ( ( # ` B ) =/= 1 -> ( R e. Ring -> ( 1 < ( # ` B ) -> .0. =/= .1. ) ) )
21 20 com13 
 |-  ( 1 < ( # ` B ) -> ( R e. Ring -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
22 14 16 21 3jaoi 
 |-  ( ( ( # ` B ) = 0 \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) ) -> ( R e. Ring -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) ) )
23 6 22 ax-mp 
 |-  ( R e. Ring -> ( ( # ` B ) =/= 1 -> .0. =/= .1. ) )
24 23 necon4d 
 |-  ( R e. Ring -> ( .0. = .1. -> ( # ` B ) = 1 ) )
25 24 imp 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> ( # ` B ) = 1 )
26 1 2 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
27 25 26 syldan 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )