Metamath Proof Explorer

Theorem isdmn3

Description: The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses isdmn3.1 
|- G = ( 1st ` R )
isdmn3.2 
|- H = ( 2nd ` R )
isdmn3.3 
|- X = ran G
isdmn3.4 
|- Z = ( GId ` G )
isdmn3.5 
|- U = ( GId ` H )
Assertion isdmn3 
|- ( R e. Dmn <-> ( R e. CRingOps /\ U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )

Proof

Step Hyp Ref Expression
1 isdmn3.1 
 |-  G = ( 1st ` R )
2 isdmn3.2 
 |-  H = ( 2nd ` R )
3 isdmn3.3 
 |-  X = ran G
4 isdmn3.4 
 |-  Z = ( GId ` G )
5 isdmn3.5 
 |-  U = ( GId ` H )
6 isdmn2 
 |-  ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )
7 1 4 isprrngo 
 |-  ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )
8 1 2 3 ispridlc 
 |-  ( R e. CRingOps -> ( { Z } e. ( PrIdl ` R ) <-> ( { Z } e. ( Idl ` R ) /\ { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) ) )
9 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
10 9 biantrurd 
 |-  ( R e. CRingOps -> ( { Z } e. ( PrIdl ` R ) <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) ) )
11 3anass 
 |-  ( ( { Z } e. ( Idl ` R ) /\ { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) <-> ( { Z } e. ( Idl ` R ) /\ ( { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) ) )
12 1 4 0idl 
 |-  ( R e. RingOps -> { Z } e. ( Idl ` R ) )
13 9 12 syl 
 |-  ( R e. CRingOps -> { Z } e. ( Idl ` R ) )
14 13 biantrurd 
 |-  ( R e. CRingOps -> ( ( { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) <-> ( { Z } e. ( Idl ` R ) /\ ( { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) ) ) )
15 1 rneqi 
 |-  ran G = ran ( 1st ` R )
16 3 15 eqtri 
 |-  X = ran ( 1st ` R )
17 16 2 5 rngo1cl 
 |-  ( R e. RingOps -> U e. X )
18 eleq2 
 |-  ( { Z } = X -> ( U e. { Z } <-> U e. X ) )
19 elsni 
 |-  ( U e. { Z } -> U = Z )
20 18 19 syl6bir 
 |-  ( { Z } = X -> ( U e. X -> U = Z ) )
21 17 20 syl5com 
 |-  ( R e. RingOps -> ( { Z } = X -> U = Z ) )
22 1 2 4 5 3 rngoueqz 
 |-  ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )
23 1 3 4 rngo0cl 
 |-  ( R e. RingOps -> Z e. X )
24 en1eqsn 
 |-  ( ( Z e. X /\ X ~~ 1o ) -> X = { Z } )
25 24 eqcomd 
 |-  ( ( Z e. X /\ X ~~ 1o ) -> { Z } = X )
26 25 ex 
 |-  ( Z e. X -> ( X ~~ 1o -> { Z } = X ) )
27 23 26 syl 
 |-  ( R e. RingOps -> ( X ~~ 1o -> { Z } = X ) )
28 22 27 sylbird 
 |-  ( R e. RingOps -> ( U = Z -> { Z } = X ) )
29 21 28 impbid 
 |-  ( R e. RingOps -> ( { Z } = X <-> U = Z ) )
30 9 29 syl 
 |-  ( R e. CRingOps -> ( { Z } = X <-> U = Z ) )
31 30 necon3bid 
 |-  ( R e. CRingOps -> ( { Z } =/= X <-> U =/= Z ) )
32 ovex 
 |-  ( a H b ) e. _V
33 32 elsn 
 |-  ( ( a H b ) e. { Z } <-> ( a H b ) = Z )
34 velsn 
 |-  ( a e. { Z } <-> a = Z )
35 velsn 
 |-  ( b e. { Z } <-> b = Z )
36 34 35 orbi12i 
 |-  ( ( a e. { Z } \/ b e. { Z } ) <-> ( a = Z \/ b = Z ) )
37 33 36 imbi12i 
 |-  ( ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) <-> ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) )
38 37 a1i 
 |-  ( R e. CRingOps -> ( ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) <-> ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )
39 38 2ralbidv 
 |-  ( R e. CRingOps -> ( A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) <-> A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )
40 31 39 anbi12d 
 |-  ( R e. CRingOps -> ( ( { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) <-> ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
41 14 40 bitr3d 
 |-  ( R e. CRingOps -> ( ( { Z } e. ( Idl ` R ) /\ ( { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) ) <-> ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
42 11 41 syl5bb 
 |-  ( R e. CRingOps -> ( ( { Z } e. ( Idl ` R ) /\ { Z } =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. { Z } -> ( a e. { Z } \/ b e. { Z } ) ) ) <-> ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
43 8 10 42 3bitr3d 
 |-  ( R e. CRingOps -> ( ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) <-> ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
44 7 43 syl5bb 
 |-  ( R e. CRingOps -> ( R e. PrRing <-> ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
45 44 pm5.32i 
 |-  ( ( R e. CRingOps /\ R e. PrRing ) <-> ( R e. CRingOps /\ ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
46 ancom 
 |-  ( ( R e. PrRing /\ R e. CRingOps ) <-> ( R e. CRingOps /\ R e. PrRing ) )
47 3anass 
 |-  ( ( R e. CRingOps /\ U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) <-> ( R e. CRingOps /\ ( U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) ) )
48 45 46 47 3bitr4i 
 |-  ( ( R e. PrRing /\ R e. CRingOps ) <-> ( R e. CRingOps /\ U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )
49 6 48 bitri 
 |-  ( R e. Dmn <-> ( R e. CRingOps /\ U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )