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 = 1 st ⁡ R
isdmn3.2 ⊢ H = 2 nd ⁡ 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 ∈ X a H b = Z → a = Z ∨ b = Z

Proof

Step Hyp Ref Expression
1 isdmn3.1 ⊢ G = 1 st ⁡ R
2 isdmn3.2 ⊢ H = 2 nd ⁡ 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 ∈ X a H b ∈ 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 ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ Z ∈ Idl ⁡ R ∧ Z ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ 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 ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ Z ∈ Idl ⁡ R ∧ Z ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z
15 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
16 3 15 eqtri ⊢ X = ran ⁡ 1 st ⁡ 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 ⊢ a H b ∈ V
33 32 elsn ⊢ a H b ∈ Z ↔ a H b = 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 ⊢ a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ a H b = Z → a = Z ∨ b = Z
38 37 a1i ⊢ R ∈ CRingOps → a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ a H b = Z → a = Z ∨ b = Z
39 38 2ralbidv ⊢ R ∈ CRingOps → ∀ a ∈ X ∀ b ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
40 31 39 anbi12d ⊢ R ∈ CRingOps → Z ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
41 14 40 bitr3d ⊢ R ∈ CRingOps → Z ∈ Idl ⁡ R ∧ Z ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
42 11 41 syl5bb ⊢ R ∈ CRingOps → Z ∈ Idl ⁡ R ∧ Z ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ Z → a ∈ Z ∨ b ∈ Z ↔ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
43 8 10 42 3bitr3d ⊢ R ∈ CRingOps → R ∈ RingOps ∧ Z ∈ PrIdl ⁡ R ↔ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
44 7 43 syl5bb ⊢ R ∈ CRingOps → R ∈ PrRing ↔ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
45 44 pm5.32i ⊢ R ∈ CRingOps ∧ R ∈ PrRing ↔ R ∈ CRingOps ∧ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
46 ancom ⊢ R ∈ PrRing ∧ R ∈ CRingOps ↔ R ∈ CRingOps ∧ R ∈ PrRing
47 3anass ⊢ R ∈ CRingOps ∧ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z ↔ R ∈ CRingOps ∧ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
48 45 46 47 3bitr4i ⊢ R ∈ PrRing ∧ R ∈ CRingOps ↔ R ∈ CRingOps ∧ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z
49 6 48 bitri ⊢ R ∈ Dmn ↔ R ∈ CRingOps ∧ U ≠ Z ∧ ∀ a ∈ X ∀ b ∈ X a H b = Z → a = Z ∨ b = Z