This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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