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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
isdmn3.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
isdmn3.3 ⊢ 𝑋 = ran 𝐺
isdmn3.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
isdmn3.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion isdmn3 ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 isdmn3.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 isdmn3.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 isdmn3.3 ⊢ 𝑋 = ran 𝐺
4 isdmn3.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 isdmn3.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 isdmn2 ⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) )
7 1 4 isprrngo ⊢ ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )
8 1 2 3 ispridlc ⊢ ( 𝑅 ∈ CRingOps → ( { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ↔ ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ) )
9 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
10 9 biantrurd ⊢ ( 𝑅 ∈ CRingOps → ( { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) ) )
11 3anass ⊢ ( ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ↔ ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ ( { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ) )
12 1 4 0idl ⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
13 9 12 syl ⊢ ( 𝑅 ∈ CRingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
14 13 biantrurd ⊢ ( 𝑅 ∈ CRingOps → ( ( { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ↔ ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ ( { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ) ) )
15 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
16 3 15 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
17 16 2 5 rngo1cl ⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )
18 eleq2 ⊢ ( { 𝑍 } = 𝑋 → ( 𝑈 ∈ { 𝑍 } ↔ 𝑈 ∈ 𝑋 ) )
19 elsni ⊢ ( 𝑈 ∈ { 𝑍 } → 𝑈 = 𝑍 )
20 18 19 biimtrrdi ⊢ ( { 𝑍 } = 𝑋 → ( 𝑈 ∈ 𝑋 → 𝑈 = 𝑍 ) )
21 17 20 syl5com ⊢ ( 𝑅 ∈ RingOps → ( { 𝑍 } = 𝑋 → 𝑈 = 𝑍 ) )
22 1 2 4 5 3 rngoueqz ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑈 = 𝑍 ) )
23 1 3 4 rngo0cl ⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ 𝑋 )
24 en1eqsn ⊢ ( ( 𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o ) → 𝑋 = { 𝑍 } )
25 24 eqcomd ⊢ ( ( 𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o ) → { 𝑍 } = 𝑋 )
26 25 ex ⊢ ( 𝑍 ∈ 𝑋 → ( 𝑋 ≈ 1o → { 𝑍 } = 𝑋 ) )
27 23 26 syl ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o → { 𝑍 } = 𝑋 ) )
28 22 27 sylbird ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 = 𝑍 → { 𝑍 } = 𝑋 ) )
29 21 28 impbid ⊢ ( 𝑅 ∈ RingOps → ( { 𝑍 } = 𝑋 ↔ 𝑈 = 𝑍 ) )
30 9 29 syl ⊢ ( 𝑅 ∈ CRingOps → ( { 𝑍 } = 𝑋 ↔ 𝑈 = 𝑍 ) )
31 30 necon3bid ⊢ ( 𝑅 ∈ CRingOps → ( { 𝑍 } ≠ 𝑋 ↔ 𝑈 ≠ 𝑍 ) )
32 ovex ⊢ ( 𝑎 𝐻 𝑏 ) ∈ V
33 32 elsn ⊢ ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } ↔ ( 𝑎 𝐻 𝑏 ) = 𝑍 )
34 velsn ⊢ ( 𝑎 ∈ { 𝑍 } ↔ 𝑎 = 𝑍 )
35 velsn ⊢ ( 𝑏 ∈ { 𝑍 } ↔ 𝑏 = 𝑍 )
36 34 35 orbi12i ⊢ ( ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ↔ ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) )
37 33 36 imbi12i ⊢ ( ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ↔ ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) )
38 37 a1i ⊢ ( 𝑅 ∈ CRingOps → ( ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ↔ ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )
39 38 2ralbidv ⊢ ( 𝑅 ∈ CRingOps → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )
40 31 39 anbi12d ⊢ ( 𝑅 ∈ CRingOps → ( ( { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
41 14 40 bitr3d ⊢ ( 𝑅 ∈ CRingOps → ( ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ ( { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ) ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
42 11 41 bitrid ⊢ ( 𝑅 ∈ CRingOps → ( ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ { 𝑍 } → ( 𝑎 ∈ { 𝑍 } ∨ 𝑏 ∈ { 𝑍 } ) ) ) ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
43 8 10 42 3bitr3d ⊢ ( 𝑅 ∈ CRingOps → ( ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
44 7 43 bitrid ⊢ ( 𝑅 ∈ CRingOps → ( 𝑅 ∈ PrRing ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
45 44 pm5.32i ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑅 ∈ PrRing ) ↔ ( 𝑅 ∈ CRingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
46 ancom ⊢ ( ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) ↔ ( 𝑅 ∈ CRingOps ∧ 𝑅 ∈ PrRing ) )
47 3anass ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ↔ ( 𝑅 ∈ CRingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) ) )
48 45 46 47 3bitr4i ⊢ ( ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) ↔ ( 𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )
49 6 48 bitri ⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) = 𝑍 → ( 𝑎 = 𝑍 ∨ 𝑏 = 𝑍 ) ) ) )