Metamath Proof Explorer

Theorem rngoueqz

Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uznzr.1 
|- G = ( 1st ` R )
uznzr.2 
|- H = ( 2nd ` R )
uznzr.3 
|- Z = ( GId ` G )
uznzr.4 
|- U = ( GId ` H )
uznzr.5 
|- X = ran G
Assertion rngoueqz 
|- ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )

Proof

Step Hyp Ref Expression
1 uznzr.1 
 |-  G = ( 1st ` R )
2 uznzr.2 
 |-  H = ( 2nd ` R )
3 uznzr.3 
 |-  Z = ( GId ` G )
4 uznzr.4 
 |-  U = ( GId ` H )
5 uznzr.5 
 |-  X = ran G
6 1 5 3 rngo0cl 
 |-  ( R e. RingOps -> Z e. X )
7 en1eqsn 
 |-  ( ( Z e. X /\ X ~~ 1o ) -> X = { Z } )
8 1 rneqi 
 |-  ran G = ran ( 1st ` R )
9 8 2 4 rngo1cl 
 |-  ( R e. RingOps -> U e. ran G )
10 eleq2 
 |-  ( X = { Z } -> ( U e. X <-> U e. { Z } ) )
11 10 biimpd 
 |-  ( X = { Z } -> ( U e. X -> U e. { Z } ) )
12 elsni 
 |-  ( U e. { Z } -> U = Z )
13 11 12 syl6com 
 |-  ( U e. X -> ( X = { Z } -> U = Z ) )
14 5 eqcomi 
 |-  ran G = X
15 13 14 eleq2s 
 |-  ( U e. ran G -> ( X = { Z } -> U = Z ) )
16 9 15 syl 
 |-  ( R e. RingOps -> ( X = { Z } -> U = Z ) )
17 7 16 syl5com 
 |-  ( ( Z e. X /\ X ~~ 1o ) -> ( R e. RingOps -> U = Z ) )
18 17 ex 
 |-  ( Z e. X -> ( X ~~ 1o -> ( R e. RingOps -> U = Z ) ) )
19 18 com23 
 |-  ( Z e. X -> ( R e. RingOps -> ( X ~~ 1o -> U = Z ) ) )
20 6 19 mpcom 
 |-  ( R e. RingOps -> ( X ~~ 1o -> U = Z ) )
21 1 5 rngone0 
 |-  ( R e. RingOps -> X =/= (/) )
22 oveq2 
 |-  ( U = Z -> ( x H U ) = ( x H Z ) )
23 22 ralrimivw 
 |-  ( U = Z -> A. x e. X ( x H U ) = ( x H Z ) )
24 3 5 1 2 rngorz 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( x H Z ) = Z )
25 24 ralrimiva 
 |-  ( R e. RingOps -> A. x e. X ( x H Z ) = Z )
26 5 8 eqtri 
 |-  X = ran ( 1st ` R )
27 2 26 4 rngoridm 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( x H U ) = x )
28 27 ralrimiva 
 |-  ( R e. RingOps -> A. x e. X ( x H U ) = x )
29 r19.26 
 |-  ( A. x e. X ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) <-> ( A. x e. X ( x H U ) = x /\ A. x e. X ( x H U ) = ( x H Z ) ) )
30 r19.26 
 |-  ( A. x e. X ( ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ ( x H Z ) = Z ) <-> ( A. x e. X ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ A. x e. X ( x H Z ) = Z ) )
31 eqtr 
 |-  ( ( x = ( x H U ) /\ ( x H U ) = ( x H Z ) ) -> x = ( x H Z ) )
32 eqtr 
 |-  ( ( x = ( x H Z ) /\ ( x H Z ) = Z ) -> x = Z )
33 32 ex 
 |-  ( x = ( x H Z ) -> ( ( x H Z ) = Z -> x = Z ) )
34 31 33 syl 
 |-  ( ( x = ( x H U ) /\ ( x H U ) = ( x H Z ) ) -> ( ( x H Z ) = Z -> x = Z ) )
35 34 ex 
 |-  ( x = ( x H U ) -> ( ( x H U ) = ( x H Z ) -> ( ( x H Z ) = Z -> x = Z ) ) )
36 35 eqcoms 
 |-  ( ( x H U ) = x -> ( ( x H U ) = ( x H Z ) -> ( ( x H Z ) = Z -> x = Z ) ) )
37 36 imp31 
 |-  ( ( ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ ( x H Z ) = Z ) -> x = Z )
38 37 ralimi 
 |-  ( A. x e. X ( ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ ( x H Z ) = Z ) -> A. x e. X x = Z )
39 eqsn 
 |-  ( X =/= (/) -> ( X = { Z } <-> A. x e. X x = Z ) )
40 ensn1g 
 |-  ( Z e. X -> { Z } ~~ 1o )
41 6 40 syl 
 |-  ( R e. RingOps -> { Z } ~~ 1o )
42 breq1 
 |-  ( X = { Z } -> ( X ~~ 1o <-> { Z } ~~ 1o ) )
43 41 42 imbitrrid 
 |-  ( X = { Z } -> ( R e. RingOps -> X ~~ 1o ) )
44 39 43 biimtrrdi 
 |-  ( X =/= (/) -> ( A. x e. X x = Z -> ( R e. RingOps -> X ~~ 1o ) ) )
45 44 com3l 
 |-  ( A. x e. X x = Z -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) )
46 38 45 syl 
 |-  ( A. x e. X ( ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ ( x H Z ) = Z ) -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) )
47 30 46 sylbir 
 |-  ( ( A. x e. X ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) /\ A. x e. X ( x H Z ) = Z ) -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) )
48 47 ex 
 |-  ( A. x e. X ( ( x H U ) = x /\ ( x H U ) = ( x H Z ) ) -> ( A. x e. X ( x H Z ) = Z -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) ) )
49 29 48 sylbir 
 |-  ( ( A. x e. X ( x H U ) = x /\ A. x e. X ( x H U ) = ( x H Z ) ) -> ( A. x e. X ( x H Z ) = Z -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) ) )
50 49 ex 
 |-  ( A. x e. X ( x H U ) = x -> ( A. x e. X ( x H U ) = ( x H Z ) -> ( A. x e. X ( x H Z ) = Z -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) ) ) )
51 50 com24 
 |-  ( A. x e. X ( x H U ) = x -> ( R e. RingOps -> ( A. x e. X ( x H Z ) = Z -> ( A. x e. X ( x H U ) = ( x H Z ) -> ( X =/= (/) -> X ~~ 1o ) ) ) ) )
52 28 51 mpcom 
 |-  ( R e. RingOps -> ( A. x e. X ( x H Z ) = Z -> ( A. x e. X ( x H U ) = ( x H Z ) -> ( X =/= (/) -> X ~~ 1o ) ) ) )
53 25 52 mpd 
 |-  ( R e. RingOps -> ( A. x e. X ( x H U ) = ( x H Z ) -> ( X =/= (/) -> X ~~ 1o ) ) )
54 23 53 syl5com 
 |-  ( U = Z -> ( R e. RingOps -> ( X =/= (/) -> X ~~ 1o ) ) )
55 54 com13 
 |-  ( X =/= (/) -> ( R e. RingOps -> ( U = Z -> X ~~ 1o ) ) )
56 21 55 mpcom 
 |-  ( R e. RingOps -> ( U = Z -> X ~~ 1o ) )
57 20 56 impbid 
 |-  ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )