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 ) )