Metamath Proof Explorer


Theorem isnzr2

Description: Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis isnzr2.b
|- B = ( Base ` R )
Assertion isnzr2
|- ( R e. NzRing <-> ( R e. Ring /\ 2o ~<_ B ) )

Proof

Step Hyp Ref Expression
1 isnzr2.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 5 adantr
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1r ` R ) e. B )
7 1 3 ring0cl
 |-  ( R e. Ring -> ( 0g ` R ) e. B )
8 7 adantr
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 0g ` R ) e. B )
9 simpr
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) )
10 df-ne
 |-  ( x =/= y <-> -. x = y )
11 neeq1
 |-  ( x = ( 1r ` R ) -> ( x =/= y <-> ( 1r ` R ) =/= y ) )
12 10 11 bitr3id
 |-  ( x = ( 1r ` R ) -> ( -. x = y <-> ( 1r ` R ) =/= y ) )
13 neeq2
 |-  ( y = ( 0g ` R ) -> ( ( 1r ` R ) =/= y <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
14 12 13 rspc2ev
 |-  ( ( ( 1r ` R ) e. B /\ ( 0g ` R ) e. B /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> E. x e. B E. y e. B -. x = y )
15 6 8 9 14 syl3anc
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> E. x e. B E. y e. B -. x = y )
16 15 ex
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= ( 0g ` R ) -> E. x e. B E. y e. B -. x = y ) )
17 1 2 3 ring1eq0
 |-  ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( ( 1r ` R ) = ( 0g ` R ) -> x = y ) )
18 17 3expb
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( ( 1r ` R ) = ( 0g ` R ) -> x = y ) )
19 18 necon3bd
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( -. x = y -> ( 1r ` R ) =/= ( 0g ` R ) ) )
20 19 rexlimdvva
 |-  ( R e. Ring -> ( E. x e. B E. y e. B -. x = y -> ( 1r ` R ) =/= ( 0g ` R ) ) )
21 16 20 impbid
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= ( 0g ` R ) <-> E. x e. B E. y e. B -. x = y ) )
22 1 fvexi
 |-  B e. _V
23 1sdom
 |-  ( B e. _V -> ( 1o ~< B <-> E. x e. B E. y e. B -. x = y ) )
24 22 23 ax-mp
 |-  ( 1o ~< B <-> E. x e. B E. y e. B -. x = y )
25 21 24 bitr4di
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= ( 0g ` R ) <-> 1o ~< B ) )
26 1onn
 |-  1o e. _om
27 sucdom
 |-  ( 1o e. _om -> ( 1o ~< B <-> suc 1o ~<_ B ) )
28 26 27 ax-mp
 |-  ( 1o ~< B <-> suc 1o ~<_ B )
29 df-2o
 |-  2o = suc 1o
30 29 breq1i
 |-  ( 2o ~<_ B <-> suc 1o ~<_ B )
31 28 30 bitr4i
 |-  ( 1o ~< B <-> 2o ~<_ B )
32 25 31 bitrdi
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= ( 0g ` R ) <-> 2o ~<_ B ) )
33 32 pm5.32i
 |-  ( ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) <-> ( R e. Ring /\ 2o ~<_ B ) )
34 4 33 bitri
 |-  ( R e. NzRing <-> ( R e. Ring /\ 2o ~<_ B ) )