Metamath Proof Explorer

Theorem isnzr2hash

Description: Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 . (Contributed by AV, 14-Apr-2019)

Ref Expression
Hypothesis isnzr2hash.b 
|- B = ( Base ` R )
Assertion isnzr2hash 
|- ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 isnzr2hash.b 
 |-  B = ( Base ` R )
2 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 2 3 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
5 1 2 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
6 1 3 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. B )
7 1xr 
 |-  1 e. RR*
8 7 a1i 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> 1 e. RR* )
9 prex 
 |-  { ( 1r ` R ) , ( 0g ` R ) } e. _V
10 hashxrcl 
 |-  ( { ( 1r ` R ) , ( 0g ` R ) } e. _V -> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) e. RR* )
11 9 10 mp1i 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) e. RR* )
12 1 fvexi 
 |-  B e. _V
13 hashxrcl 
 |-  ( B e. _V -> ( # ` B ) e. RR* )
14 12 13 mp1i 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( # ` B ) e. RR* )
15 1lt2 
 |-  1 < 2
16 hashprg 
 |-  ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) -> ( ( 1r ` R ) =/= ( 0g ` R ) <-> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) = 2 ) )
17 16 biimpa 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) = 2 )
18 15 17 breqtrrid 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> 1 < ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) )
19 simpl 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) )
20 fvex 
 |-  ( 1r ` R ) e. _V
21 fvex 
 |-  ( 0g ` R ) e. _V
22 20 21 prss 
 |-  ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) <-> { ( 1r ` R ) , ( 0g ` R ) } C_ B )
23 19 22 sylib 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> { ( 1r ` R ) , ( 0g ` R ) } C_ B )
24 hashss 
 |-  ( ( B e. _V /\ { ( 1r ` R ) , ( 0g ` R ) } C_ B ) -> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) <_ ( # ` B ) )
25 12 23 24 sylancr 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( # ` { ( 1r ` R ) , ( 0g ` R ) } ) <_ ( # ` B ) )
26 8 11 14 18 25 xrltletrd 
 |-  ( ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> 1 < ( # ` B ) )
27 26 ex 
 |-  ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B ) -> ( ( 1r ` R ) =/= ( 0g ` R ) -> 1 < ( # ` B ) ) )
28 5 6 27 syl2anc 
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= ( 0g ` R ) -> 1 < ( # ` B ) ) )
29 28 imdistani 
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( R e. Ring /\ 1 < ( # ` B ) ) )
30 simpl 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> R e. Ring )
31 1 2 3 ring1ne0 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> ( 1r ` R ) =/= ( 0g ` R ) )
32 30 31 jca 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
33 29 32 impbii 
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) <-> ( R e. Ring /\ 1 < ( # ` B ) ) )
34 4 33 bitri 
 |-  ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` B ) ) )