Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β π
β RingOps) |
2 | | smprngpr.1 |
. . . . 5
β’ πΊ = (1st βπ
) |
3 | | smprngpr.4 |
. . . . 5
β’ π = (GIdβπΊ) |
4 | 2, 3 | 0idl 36487 |
. . . 4
β’ (π
β RingOps β {π} β (Idlβπ
)) |
5 | 4 | 3ad2ant1 1134 |
. . 3
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β {π} β (Idlβπ
)) |
6 | | smprngpr.2 |
. . . . . . . 8
β’ π» = (2nd βπ
) |
7 | | smprngpr.3 |
. . . . . . . 8
β’ π = ran πΊ |
8 | | smprngpr.5 |
. . . . . . . 8
β’ π = (GIdβπ») |
9 | 2, 6, 7, 3, 8 | 0rngo 36489 |
. . . . . . 7
β’ (π
β RingOps β (π = π β π = {π})) |
10 | | eqcom 2744 |
. . . . . . 7
β’ (π = π β π = π) |
11 | | eqcom 2744 |
. . . . . . 7
β’ ({π} = π β π = {π}) |
12 | 9, 10, 11 | 3bitr4g 314 |
. . . . . 6
β’ (π
β RingOps β (π = π β {π} = π)) |
13 | 12 | necon3bid 2989 |
. . . . 5
β’ (π
β RingOps β (π β π β {π} β π)) |
14 | 13 | biimpa 478 |
. . . 4
β’ ((π
β RingOps β§ π β π) β {π} β π) |
15 | 14 | 3adant3 1133 |
. . 3
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β {π} β π) |
16 | | df-pr 4590 |
. . . . . . . 8
β’ {{π}, π} = ({{π}} βͺ {π}) |
17 | 16 | eqeq2i 2750 |
. . . . . . 7
β’
((Idlβπ
) =
{{π}, π} β (Idlβπ
) = ({{π}} βͺ {π})) |
18 | | eleq2 2827 |
. . . . . . . . 9
β’
((Idlβπ
) =
({{π}} βͺ {π}) β (π β (Idlβπ
) β π β ({{π}} βͺ {π}))) |
19 | | eleq2 2827 |
. . . . . . . . 9
β’
((Idlβπ
) =
({{π}} βͺ {π}) β (π β (Idlβπ
) β π β ({{π}} βͺ {π}))) |
20 | 18, 19 | anbi12d 632 |
. . . . . . . 8
β’
((Idlβπ
) =
({{π}} βͺ {π}) β ((π β (Idlβπ
) β§ π β (Idlβπ
)) β (π β ({{π}} βͺ {π}) β§ π β ({{π}} βͺ {π})))) |
21 | | elun 4109 |
. . . . . . . . . 10
β’ (π β ({{π}} βͺ {π}) β (π β {{π}} β¨ π β {π})) |
22 | | velsn 4603 |
. . . . . . . . . . 11
β’ (π β {{π}} β π = {π}) |
23 | | velsn 4603 |
. . . . . . . . . . 11
β’ (π β {π} β π = π) |
24 | 22, 23 | orbi12i 914 |
. . . . . . . . . 10
β’ ((π β {{π}} β¨ π β {π}) β (π = {π} β¨ π = π)) |
25 | 21, 24 | bitri 275 |
. . . . . . . . 9
β’ (π β ({{π}} βͺ {π}) β (π = {π} β¨ π = π)) |
26 | | elun 4109 |
. . . . . . . . . 10
β’ (π β ({{π}} βͺ {π}) β (π β {{π}} β¨ π β {π})) |
27 | | velsn 4603 |
. . . . . . . . . . 11
β’ (π β {{π}} β π = {π}) |
28 | | velsn 4603 |
. . . . . . . . . . 11
β’ (π β {π} β π = π) |
29 | 27, 28 | orbi12i 914 |
. . . . . . . . . 10
β’ ((π β {{π}} β¨ π β {π}) β (π = {π} β¨ π = π)) |
30 | 26, 29 | bitri 275 |
. . . . . . . . 9
β’ (π β ({{π}} βͺ {π}) β (π = {π} β¨ π = π)) |
31 | 25, 30 | anbi12i 628 |
. . . . . . . 8
β’ ((π β ({{π}} βͺ {π}) β§ π β ({{π}} βͺ {π})) β ((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π))) |
32 | 20, 31 | bitrdi 287 |
. . . . . . 7
β’
((Idlβπ
) =
({{π}} βͺ {π}) β ((π β (Idlβπ
) β§ π β (Idlβπ
)) β ((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π)))) |
33 | 17, 32 | sylbi 216 |
. . . . . 6
β’
((Idlβπ
) =
{{π}, π} β ((π β (Idlβπ
) β§ π β (Idlβπ
)) β ((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π)))) |
34 | 33 | 3ad2ant3 1136 |
. . . . 5
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β ((π β (Idlβπ
) β§ π β (Idlβπ
)) β ((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π)))) |
35 | | eqimss 4001 |
. . . . . . . . . . 11
β’ (π = {π} β π β {π}) |
36 | 35 | orcd 872 |
. . . . . . . . . 10
β’ (π = {π} β (π β {π} β¨ π β {π})) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’ ((π = {π} β§ π = {π}) β (π β {π} β¨ π β {π})) |
38 | 37 | a1d 25 |
. . . . . . . 8
β’ ((π = {π} β§ π = {π}) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))) |
39 | 38 | a1i 11 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β ((π = {π} β§ π = {π}) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
40 | | eqimss 4001 |
. . . . . . . . . . 11
β’ (π = {π} β π β {π}) |
41 | 40 | olcd 873 |
. . . . . . . . . 10
β’ (π = {π} β (π β {π} β¨ π β {π})) |
42 | 41 | adantl 483 |
. . . . . . . . 9
β’ ((π = π β§ π = {π}) β (π β {π} β¨ π β {π})) |
43 | 42 | a1d 25 |
. . . . . . . 8
β’ ((π = π β§ π = {π}) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))) |
44 | 43 | a1i 11 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β ((π = π β§ π = {π}) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
45 | 36 | adantr 482 |
. . . . . . . . 9
β’ ((π = {π} β§ π = π) β (π β {π} β¨ π β {π})) |
46 | 45 | a1d 25 |
. . . . . . . 8
β’ ((π = {π} β§ π = π) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))) |
47 | 46 | a1i 11 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β ((π = {π} β§ π = π) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
48 | 2 | rneqi 5893 |
. . . . . . . . . . . . . 14
β’ ran πΊ = ran (1st
βπ
) |
49 | 7, 48 | eqtri 2765 |
. . . . . . . . . . . . 13
β’ π = ran (1st
βπ
) |
50 | 49, 6, 8 | rngo1cl 36401 |
. . . . . . . . . . . 12
β’ (π
β RingOps β π β π) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ π β π) β π β π) |
52 | 6, 49, 8 | rngolidm 36399 |
. . . . . . . . . . . . . . . 16
β’ ((π
β RingOps β§ π β π) β (ππ»π) = π) |
53 | 50, 52 | mpdan 686 |
. . . . . . . . . . . . . . 15
β’ (π
β RingOps β (ππ»π) = π) |
54 | 53 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π
β RingOps β ((ππ»π) β {π} β π β {π})) |
55 | 8 | fvexi 6857 |
. . . . . . . . . . . . . . 15
β’ π β V |
56 | 55 | elsn 4602 |
. . . . . . . . . . . . . 14
β’ (π β {π} β π = π) |
57 | 54, 56 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β ((ππ»π) β {π} β π = π)) |
58 | 57 | necon3bbid 2982 |
. . . . . . . . . . . 12
β’ (π
β RingOps β (Β¬
(ππ»π) β {π} β π β π)) |
59 | 58 | biimpar 479 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ π β π) β Β¬ (ππ»π) β {π}) |
60 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯π»π¦) = (ππ»π¦)) |
61 | 60 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯π»π¦) β {π} β (ππ»π¦) β {π})) |
62 | 61 | notbid 318 |
. . . . . . . . . . . 12
β’ (π₯ = π β (Β¬ (π₯π»π¦) β {π} β Β¬ (ππ»π¦) β {π})) |
63 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (ππ»π¦) = (ππ»π)) |
64 | 63 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((ππ»π¦) β {π} β (ππ»π) β {π})) |
65 | 64 | notbid 318 |
. . . . . . . . . . . 12
β’ (π¦ = π β (Β¬ (ππ»π¦) β {π} β Β¬ (ππ»π) β {π})) |
66 | 62, 65 | rspc2ev 3593 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π β§ Β¬ (ππ»π) β {π}) β βπ₯ β π βπ¦ β π Β¬ (π₯π»π¦) β {π}) |
67 | 51, 51, 59, 66 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π
β RingOps β§ π β π) β βπ₯ β π βπ¦ β π Β¬ (π₯π»π¦) β {π}) |
68 | | rexnal2 3133 |
. . . . . . . . . 10
β’
(βπ₯ β
π βπ¦ β π Β¬ (π₯π»π¦) β {π} β Β¬ βπ₯ β π βπ¦ β π (π₯π»π¦) β {π}) |
69 | 67, 68 | sylib 217 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π β π) β Β¬ βπ₯ β π βπ¦ β π (π₯π»π¦) β {π}) |
70 | 69 | pm2.21d 121 |
. . . . . . . 8
β’ ((π
β RingOps β§ π β π) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))) |
71 | | raleq 3310 |
. . . . . . . . . 10
β’ (π = π β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β βπ₯ β π βπ¦ β π (π₯π»π¦) β {π})) |
72 | | raleq 3310 |
. . . . . . . . . . 11
β’ (π = π β (βπ¦ β π (π₯π»π¦) β {π} β βπ¦ β π (π₯π»π¦) β {π})) |
73 | 72 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π = π β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β βπ₯ β π βπ¦ β π (π₯π»π¦) β {π})) |
74 | 71, 73 | sylan9bb 511 |
. . . . . . . . 9
β’ ((π = π β§ π = π) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β βπ₯ β π βπ¦ β π (π₯π»π¦) β {π})) |
75 | 74 | imbi1d 342 |
. . . . . . . 8
β’ ((π = π β§ π = π) β ((βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
76 | 70, 75 | syl5ibrcom 247 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β ((π = π β§ π = π) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
77 | 39, 44, 47, 76 | ccased 1038 |
. . . . . 6
β’ ((π
β RingOps β§ π β π) β (((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π)) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
78 | 77 | 3adant3 1133 |
. . . . 5
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β (((π = {π} β¨ π = π) β§ (π = {π} β¨ π = π)) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
79 | 34, 78 | sylbid 239 |
. . . 4
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β ((π β (Idlβπ
) β§ π β (Idlβπ
)) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π})))) |
80 | 79 | ralrimivv 3196 |
. . 3
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))) |
81 | 2, 6, 7 | ispridl 36496 |
. . . 4
β’ (π
β RingOps β ({π} β (PrIdlβπ
) β ({π} β (Idlβπ
) β§ {π} β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))))) |
82 | 81 | 3ad2ant1 1134 |
. . 3
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β ({π} β (PrIdlβπ
) β ({π} β (Idlβπ
) β§ {π} β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β {π} β (π β {π} β¨ π β {π}))))) |
83 | 5, 15, 80, 82 | mpbir3and 1343 |
. 2
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β {π} β (PrIdlβπ
)) |
84 | 2, 3 | isprrngo 36512 |
. 2
β’ (π
β PrRing β (π
β RingOps β§ {π} β (PrIdlβπ
))) |
85 | 1, 83, 84 | sylanbrc 584 |
1
β’ ((π
β RingOps β§ π β π β§ (Idlβπ
) = {{π}, π}) β π
β PrRing) |