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∈Dmn↔R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=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∈Dmn↔R∈PrRing∧R∈CRingOps
7 1 4 isprrngo ⊢R∈PrRing↔R∈RingOps∧Z∈PrIdl⁡R
8 1 2 3 ispridlc ⊢R∈CRingOps→Z∈PrIdl⁡R↔Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z
9 crngorngo ⊢R∈CRingOps→R∈RingOps
10 9 biantrurd ⊢R∈CRingOps→Z∈PrIdl⁡R↔R∈RingOps∧Z∈PrIdl⁡R
11 3anass ⊢Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z
12 1 4 0idl ⊢R∈RingOps→Z∈Idl⁡R
13 9 12 syl ⊢R∈CRingOps→Z∈Idl⁡R
14 13 biantrurd ⊢R∈CRingOps→Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z
15 1 rneqi ⊢ran⁡G=ran⁡1st⁡R
16 3 15 eqtri ⊢X=ran⁡1st⁡R
17 16 2 5 rngo1cl ⊢R∈RingOps→U∈X
18 eleq2 ⊢Z=X→U∈Z↔U∈X
19 elsni ⊢U∈Z→U=Z
20 18 19 syl6bir ⊢Z=X→U∈X→U=Z
21 17 20 syl5com ⊢R∈RingOps→Z=X→U=Z
22 1 2 4 5 3 rngoueqz ⊢R∈RingOps→X≈1𝑜↔U=Z
23 1 3 4 rngo0cl ⊢R∈RingOps→Z∈X
24 en1eqsn ⊢Z∈X∧X≈1𝑜→X=Z
25 24 eqcomd ⊢Z∈X∧X≈1𝑜→Z=X
26 25 ex ⊢Z∈X→X≈1𝑜→Z=X
27 23 26 syl ⊢R∈RingOps→X≈1𝑜→Z=X
28 22 27 sylbird ⊢R∈RingOps→U=Z→Z=X
29 21 28 impbid ⊢R∈RingOps→Z=X↔U=Z
30 9 29 syl ⊢R∈CRingOps→Z=X↔U=Z
31 30 necon3bid ⊢R∈CRingOps→Z≠X↔U≠Z
32 ovex ⊢aHb∈V
33 32 elsn ⊢aHb∈Z↔aHb=Z
34 velsn ⊢a∈Z↔a=Z
35 velsn ⊢b∈Z↔b=Z
36 34 35 orbi12i ⊢a∈Z∨b∈Z↔a=Z∨b=Z
37 33 36 imbi12i ⊢aHb∈Z→a∈Z∨b∈Z↔aHb=Z→a=Z∨b=Z
38 37 a1i ⊢R∈CRingOps→aHb∈Z→a∈Z∨b∈Z↔aHb=Z→a=Z∨b=Z
39 38 2ralbidv ⊢R∈CRingOps→∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
40 31 39 anbi12d ⊢R∈CRingOps→Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
41 14 40 bitr3d ⊢R∈CRingOps→Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
42 11 41 bitrid ⊢R∈CRingOps→Z∈Idl⁡R∧Z≠X∧∀a∈X∀b∈XaHb∈Z→a∈Z∨b∈Z↔U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
43 8 10 42 3bitr3d ⊢R∈CRingOps→R∈RingOps∧Z∈PrIdl⁡R↔U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
44 7 43 bitrid ⊢R∈CRingOps→R∈PrRing↔U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
45 44 pm5.32i ⊢R∈CRingOps∧R∈PrRing↔R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
46 ancom ⊢R∈PrRing∧R∈CRingOps↔R∈CRingOps∧R∈PrRing
47 3anass ⊢R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z↔R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
48 45 46 47 3bitr4i ⊢R∈PrRing∧R∈CRingOps↔R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z
49 6 48 bitri ⊢R∈Dmn↔R∈CRingOps∧U≠Z∧∀a∈X∀b∈XaHb=Z→a=Z∨b=Z