Proof of Theorem isdmn3
Step | Hyp | Ref
| Expression |
1 | | isdmn2 35858 |
. 2
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈
CRingOps)) |
2 | | isdmn3.1 |
. . . . . 6
⊢ 𝐺 = (1st ‘𝑅) |
3 | | isdmn3.4 |
. . . . . 6
⊢ 𝑍 = (GId‘𝐺) |
4 | 2, 3 | isprrngo 35853 |
. . . . 5
⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) |
5 | | isdmn3.2 |
. . . . . . 7
⊢ 𝐻 = (2nd ‘𝑅) |
6 | | isdmn3.3 |
. . . . . . 7
⊢ 𝑋 = ran 𝐺 |
7 | 2, 5, 6 | ispridlc 35873 |
. . . . . 6
⊢ (𝑅 ∈ CRingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))))) |
8 | | crngorngo 35803 |
. . . . . . 7
⊢ (𝑅 ∈ CRingOps → 𝑅 ∈
RingOps) |
9 | 8 | biantrurd 536 |
. . . . . 6
⊢ (𝑅 ∈ CRingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))) |
10 | | 3anass 1096 |
. . . . . . 7
⊢ (({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ ({𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))))) |
11 | 2, 3 | 0idl 35828 |
. . . . . . . . . 10
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRingOps → {𝑍} ∈ (Idl‘𝑅)) |
13 | 12 | biantrurd 536 |
. . . . . . . 8
⊢ (𝑅 ∈ CRingOps → (({𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ ({𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍})))))) |
14 | 2 | rneqi 5780 |
. . . . . . . . . . . . . . 15
⊢ ran 𝐺 = ran (1st
‘𝑅) |
15 | 6, 14 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ran (1st
‘𝑅) |
16 | | isdmn3.5 |
. . . . . . . . . . . . . 14
⊢ 𝑈 = (GId‘𝐻) |
17 | 15, 5, 16 | rngo1cl 35742 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) |
18 | | eleq2 2821 |
. . . . . . . . . . . . . 14
⊢ ({𝑍} = 𝑋 → (𝑈 ∈ {𝑍} ↔ 𝑈 ∈ 𝑋)) |
19 | | elsni 4533 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ {𝑍} → 𝑈 = 𝑍) |
20 | 18, 19 | syl6bir 257 |
. . . . . . . . . . . . 13
⊢ ({𝑍} = 𝑋 → (𝑈 ∈ 𝑋 → 𝑈 = 𝑍)) |
21 | 17, 20 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → ({𝑍} = 𝑋 → 𝑈 = 𝑍)) |
22 | 2, 5, 3, 16, 6 | rngoueqz 35743 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔
𝑈 = 𝑍)) |
23 | 2, 6, 3 | rngo0cl 35722 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) |
24 | | en1eqsn 8827 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → 𝑋 = {𝑍}) |
25 | 24 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → {𝑍} = 𝑋) |
26 | 25 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝑋 → (𝑋 ≈ 1o → {𝑍} = 𝑋)) |
27 | 23, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o →
{𝑍} = 𝑋)) |
28 | 22, 27 | sylbird 263 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 → {𝑍} = 𝑋)) |
29 | 21, 28 | impbid 215 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ RingOps → ({𝑍} = 𝑋 ↔ 𝑈 = 𝑍)) |
30 | 8, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRingOps → ({𝑍} = 𝑋 ↔ 𝑈 = 𝑍)) |
31 | 30 | necon3bid 2978 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRingOps → ({𝑍} ≠ 𝑋 ↔ 𝑈 ≠ 𝑍)) |
32 | | ovex 7205 |
. . . . . . . . . . . . 13
⊢ (𝑎𝐻𝑏) ∈ V |
33 | 32 | elsn 4531 |
. . . . . . . . . . . 12
⊢ ((𝑎𝐻𝑏) ∈ {𝑍} ↔ (𝑎𝐻𝑏) = 𝑍) |
34 | | velsn 4532 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑍} ↔ 𝑎 = 𝑍) |
35 | | velsn 4532 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ {𝑍} ↔ 𝑏 = 𝑍) |
36 | 34, 35 | orbi12i 914 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}) ↔ (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)) |
37 | 33, 36 | imbi12i 354 |
. . . . . . . . . . 11
⊢ (((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍})) ↔ ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))) |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRingOps → (((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍})) ↔ ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) |
39 | 38 | 2ralbidv 3111 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRingOps →
(∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍})) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) |
40 | 31, 39 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑅 ∈ CRingOps → (({𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
41 | 13, 40 | bitr3d 284 |
. . . . . . 7
⊢ (𝑅 ∈ CRingOps → (({𝑍} ∈ (Idl‘𝑅) ∧ ({𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍})))) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
42 | 10, 41 | syl5bb 286 |
. . . . . 6
⊢ (𝑅 ∈ CRingOps → (({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ {𝑍} → (𝑎 ∈ {𝑍} ∨ 𝑏 ∈ {𝑍}))) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
43 | 7, 9, 42 | 3bitr3d 312 |
. . . . 5
⊢ (𝑅 ∈ CRingOps → ((𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
44 | 4, 43 | syl5bb 286 |
. . . 4
⊢ (𝑅 ∈ CRingOps → (𝑅 ∈ PrRing ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
45 | 44 | pm5.32i 578 |
. . 3
⊢ ((𝑅 ∈ CRingOps ∧ 𝑅 ∈ PrRing) ↔ (𝑅 ∈ CRingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
46 | | ancom 464 |
. . 3
⊢ ((𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps) ↔ (𝑅 ∈ CRingOps ∧ 𝑅 ∈
PrRing)) |
47 | | 3anass 1096 |
. . 3
⊢ ((𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))) ↔ (𝑅 ∈ CRingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))) |
48 | 45, 46, 47 | 3bitr4i 306 |
. 2
⊢ ((𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps) ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) |
49 | 1, 48 | bitri 278 |
1
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) |