Step | Hyp | Ref
| Expression |
1 | | isdmn2 36543 |
. 2
β’ (π
β Dmn β (π
β PrRing β§ π
β
CRingOps)) |
2 | | isdmn3.1 |
. . . . . 6
β’ πΊ = (1st βπ
) |
3 | | isdmn3.4 |
. . . . . 6
β’ π = (GIdβπΊ) |
4 | 2, 3 | isprrngo 36538 |
. . . . 5
β’ (π
β PrRing β (π
β RingOps β§ {π} β (PrIdlβπ
))) |
5 | | isdmn3.2 |
. . . . . . 7
β’ π» = (2nd βπ
) |
6 | | isdmn3.3 |
. . . . . . 7
β’ π = ran πΊ |
7 | 2, 5, 6 | ispridlc 36558 |
. . . . . 6
β’ (π
β CRingOps β ({π} β (PrIdlβπ
) β ({π} β (Idlβπ
) β§ {π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))))) |
8 | | crngorngo 36488 |
. . . . . . 7
β’ (π
β CRingOps β π
β
RingOps) |
9 | 8 | biantrurd 534 |
. . . . . 6
β’ (π
β CRingOps β ({π} β (PrIdlβπ
) β (π
β RingOps β§ {π} β (PrIdlβπ
)))) |
10 | | 3anass 1096 |
. . . . . . 7
β’ (({π} β (Idlβπ
) β§ {π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))) β ({π} β (Idlβπ
) β§ ({π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))))) |
11 | 2, 3 | 0idl 36513 |
. . . . . . . . . 10
β’ (π
β RingOps β {π} β (Idlβπ
)) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
β’ (π
β CRingOps β {π} β (Idlβπ
)) |
13 | 12 | biantrurd 534 |
. . . . . . . 8
β’ (π
β CRingOps β (({π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))) β ({π} β (Idlβπ
) β§ ({π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π})))))) |
14 | 2 | rneqi 5897 |
. . . . . . . . . . . . . . 15
β’ ran πΊ = ran (1st
βπ
) |
15 | 6, 14 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ π = ran (1st
βπ
) |
16 | | isdmn3.5 |
. . . . . . . . . . . . . 14
β’ π = (GIdβπ») |
17 | 15, 5, 16 | rngo1cl 36427 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β π β π) |
18 | | eleq2 2827 |
. . . . . . . . . . . . . 14
β’ ({π} = π β (π β {π} β π β π)) |
19 | | elsni 4608 |
. . . . . . . . . . . . . 14
β’ (π β {π} β π = π) |
20 | 18, 19 | syl6bir 254 |
. . . . . . . . . . . . 13
β’ ({π} = π β (π β π β π = π)) |
21 | 17, 20 | syl5com 31 |
. . . . . . . . . . . 12
β’ (π
β RingOps β ({π} = π β π = π)) |
22 | 2, 5, 3, 16, 6 | rngoueqz 36428 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β (π β 1o β
π = π)) |
23 | 2, 6, 3 | rngo0cl 36407 |
. . . . . . . . . . . . . 14
β’ (π
β RingOps β π β π) |
24 | | en1eqsn 9225 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β 1o) β π = {π}) |
25 | 24 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β 1o) β {π} = π) |
26 | 25 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β π β (π β 1o β {π} = π)) |
27 | 23, 26 | syl 17 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β (π β 1o β
{π} = π)) |
28 | 22, 27 | sylbird 260 |
. . . . . . . . . . . 12
β’ (π
β RingOps β (π = π β {π} = π)) |
29 | 21, 28 | impbid 211 |
. . . . . . . . . . 11
β’ (π
β RingOps β ({π} = π β π = π)) |
30 | 8, 29 | syl 17 |
. . . . . . . . . 10
β’ (π
β CRingOps β ({π} = π β π = π)) |
31 | 30 | necon3bid 2989 |
. . . . . . . . 9
β’ (π
β CRingOps β ({π} β π β π β π)) |
32 | | ovex 7395 |
. . . . . . . . . . . . 13
β’ (ππ»π) β V |
33 | 32 | elsn 4606 |
. . . . . . . . . . . 12
β’ ((ππ»π) β {π} β (ππ»π) = π) |
34 | | velsn 4607 |
. . . . . . . . . . . . 13
β’ (π β {π} β π = π) |
35 | | velsn 4607 |
. . . . . . . . . . . . 13
β’ (π β {π} β π = π) |
36 | 34, 35 | orbi12i 914 |
. . . . . . . . . . . 12
β’ ((π β {π} β¨ π β {π}) β (π = π β¨ π = π)) |
37 | 33, 36 | imbi12i 351 |
. . . . . . . . . . 11
β’ (((ππ»π) β {π} β (π β {π} β¨ π β {π})) β ((ππ»π) = π β (π = π β¨ π = π))) |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ (π
β CRingOps β (((ππ»π) β {π} β (π β {π} β¨ π β {π})) β ((ππ»π) = π β (π = π β¨ π = π)))) |
39 | 38 | 2ralbidv 3213 |
. . . . . . . . 9
β’ (π
β CRingOps β
(βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π})) β βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π)))) |
40 | 31, 39 | anbi12d 632 |
. . . . . . . 8
β’ (π
β CRingOps β (({π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))) β (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
41 | 13, 40 | bitr3d 281 |
. . . . . . 7
β’ (π
β CRingOps β (({π} β (Idlβπ
) β§ ({π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π})))) β (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
42 | 10, 41 | bitrid 283 |
. . . . . 6
β’ (π
β CRingOps β (({π} β (Idlβπ
) β§ {π} β π β§ βπ β π βπ β π ((ππ»π) β {π} β (π β {π} β¨ π β {π}))) β (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
43 | 7, 9, 42 | 3bitr3d 309 |
. . . . 5
β’ (π
β CRingOps β ((π
β RingOps β§ {π} β (PrIdlβπ
)) β (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
44 | 4, 43 | bitrid 283 |
. . . 4
β’ (π
β CRingOps β (π
β PrRing β (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
45 | 44 | pm5.32i 576 |
. . 3
β’ ((π
β CRingOps β§ π
β PrRing) β (π
β CRingOps β§ (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
46 | | ancom 462 |
. . 3
β’ ((π
β PrRing β§ π
β CRingOps) β (π
β CRingOps β§ π
β
PrRing)) |
47 | | 3anass 1096 |
. . 3
β’ ((π
β CRingOps β§ π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))) β (π
β CRingOps β§ (π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π))))) |
48 | 45, 46, 47 | 3bitr4i 303 |
. 2
β’ ((π
β PrRing β§ π
β CRingOps) β (π
β CRingOps β§ π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π)))) |
49 | 1, 48 | bitri 275 |
1
β’ (π
β Dmn β (π
β CRingOps β§ π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π)))) |