Metamath Proof Explorer

Theorem 0ringnnzr

Description: A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion 0ringnnzr 
|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 1 ltnri 
 |-  -. 1 < 1
3 breq2 
 |-  ( ( # ` ( Base ` R ) ) = 1 -> ( 1 < ( # ` ( Base ` R ) ) <-> 1 < 1 ) )
4 2 3 mtbiri 
 |-  ( ( # ` ( Base ` R ) ) = 1 -> -. 1 < ( # ` ( Base ` R ) ) )
5 4 adantl 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> -. 1 < ( # ` ( Base ` R ) ) )
6 5 intnand 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) )
7 6 ex 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 -> -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) ) )
8 ianor 
 |-  ( -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) <-> ( -. R e. Ring \/ -. 1 < ( # ` ( Base ` R ) ) ) )
9 pm2.21 
 |-  ( -. R e. Ring -> ( R e. Ring -> ( # ` ( Base ` R ) ) = 1 ) )
10 fvex 
 |-  ( Base ` R ) e. _V
11 hashxrcl 
 |-  ( ( Base ` R ) e. _V -> ( # ` ( Base ` R ) ) e. RR* )
12 10 11 ax-mp 
 |-  ( # ` ( Base ` R ) ) e. RR*
13 1xr 
 |-  1 e. RR*
14 xrlenlt 
 |-  ( ( ( # ` ( Base ` R ) ) e. RR* /\ 1 e. RR* ) -> ( ( # ` ( Base ` R ) ) <_ 1 <-> -. 1 < ( # ` ( Base ` R ) ) ) )
15 12 13 14 mp2an 
 |-  ( ( # ` ( Base ` R ) ) <_ 1 <-> -. 1 < ( # ` ( Base ` R ) ) )
16 15 bicomi 
 |-  ( -. 1 < ( # ` ( Base ` R ) ) <-> ( # ` ( Base ` R ) ) <_ 1 )
17 simpr 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( # ` ( Base ` R ) ) <_ 1 )
18 1nn0 
 |-  1 e. NN0
19 hashbnd 
 |-  ( ( ( Base ` R ) e. _V /\ 1 e. NN0 /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( Base ` R ) e. Fin )
20 10 18 17 19 mp3an12i 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( Base ` R ) e. Fin )
21 hashcl 
 |-  ( ( Base ` R ) e. Fin -> ( # ` ( Base ` R ) ) e. NN0 )
22 simpr 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) e. NN0 ) -> ( # ` ( Base ` R ) ) e. NN0 )
23 hasheq0 
 |-  ( ( Base ` R ) e. _V -> ( ( # ` ( Base ` R ) ) = 0 <-> ( Base ` R ) = (/) ) )
24 10 23 mp1i 
 |-  ( ( # ` ( Base ` R ) ) e. NN0 -> ( ( # ` ( Base ` R ) ) = 0 <-> ( Base ` R ) = (/) ) )
25 24 biimpd 
 |-  ( ( # ` ( Base ` R ) ) e. NN0 -> ( ( # ` ( Base ` R ) ) = 0 -> ( Base ` R ) = (/) ) )
26 25 necon3d 
 |-  ( ( # ` ( Base ` R ) ) e. NN0 -> ( ( Base ` R ) =/= (/) -> ( # ` ( Base ` R ) ) =/= 0 ) )
27 26 impcom 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) e. NN0 ) -> ( # ` ( Base ` R ) ) =/= 0 )
28 elnnne0 
 |-  ( ( # ` ( Base ` R ) ) e. NN <-> ( ( # ` ( Base ` R ) ) e. NN0 /\ ( # ` ( Base ` R ) ) =/= 0 ) )
29 22 27 28 sylanbrc 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) e. NN0 ) -> ( # ` ( Base ` R ) ) e. NN )
30 29 ex 
 |-  ( ( Base ` R ) =/= (/) -> ( ( # ` ( Base ` R ) ) e. NN0 -> ( # ` ( Base ` R ) ) e. NN ) )
31 30 adantr 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( ( # ` ( Base ` R ) ) e. NN0 -> ( # ` ( Base ` R ) ) e. NN ) )
32 21 31 syl5com 
 |-  ( ( Base ` R ) e. Fin -> ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( # ` ( Base ` R ) ) e. NN ) )
33 20 32 mpcom 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( # ` ( Base ` R ) ) e. NN )
34 nnle1eq1 
 |-  ( ( # ` ( Base ` R ) ) e. NN -> ( ( # ` ( Base ` R ) ) <_ 1 <-> ( # ` ( Base ` R ) ) = 1 ) )
35 33 34 syl 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( ( # ` ( Base ` R ) ) <_ 1 <-> ( # ` ( Base ` R ) ) = 1 ) )
36 17 35 mpbid 
 |-  ( ( ( Base ` R ) =/= (/) /\ ( # ` ( Base ` R ) ) <_ 1 ) -> ( # ` ( Base ` R ) ) = 1 )
37 36 ex 
 |-  ( ( Base ` R ) =/= (/) -> ( ( # ` ( Base ` R ) ) <_ 1 -> ( # ` ( Base ` R ) ) = 1 ) )
38 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
39 eqid 
 |-  ( Base ` R ) = ( Base ` R )
40 39 grpbn0 
 |-  ( R e. Grp -> ( Base ` R ) =/= (/) )
41 38 40 syl 
 |-  ( R e. Ring -> ( Base ` R ) =/= (/) )
42 37 41 syl11 
 |-  ( ( # ` ( Base ` R ) ) <_ 1 -> ( R e. Ring -> ( # ` ( Base ` R ) ) = 1 ) )
43 16 42 sylbi 
 |-  ( -. 1 < ( # ` ( Base ` R ) ) -> ( R e. Ring -> ( # ` ( Base ` R ) ) = 1 ) )
44 9 43 jaoi 
 |-  ( ( -. R e. Ring \/ -. 1 < ( # ` ( Base ` R ) ) ) -> ( R e. Ring -> ( # ` ( Base ` R ) ) = 1 ) )
45 8 44 sylbi 
 |-  ( -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) -> ( R e. Ring -> ( # ` ( Base ` R ) ) = 1 ) )
46 45 com12 
 |-  ( R e. Ring -> ( -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) -> ( # ` ( Base ` R ) ) = 1 ) )
47 7 46 impbid 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) ) )
48 39 isnzr2hash 
 |-  ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) )
49 48 bicomi 
 |-  ( ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) <-> R e. NzRing )
50 49 notbii 
 |-  ( -. ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) <-> -. R e. NzRing )
51 47 50 bitrdi 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )