Step | Hyp | Ref
| Expression |
1 | | zartop.2 |
. . 3
β’ π½ = (TopOpenβπ) |
2 | | zartop.1 |
. . . 4
β’ π = (Specβπ
) |
3 | | eqid 2733 |
. . . 4
β’
(LIdealβπ
) =
(LIdealβπ
) |
4 | | zarcls.1 |
. . . 4
β’ π = (PrmIdealβπ
) |
5 | | eqid 2733 |
. . . 4
β’ ran
(π β
(LIdealβπ
) β¦
{π β π β£ Β¬ π β π}) = ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) |
6 | 2, 3, 4, 5 | rspectopn 32512 |
. . 3
β’ (π
β Ring β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) = (TopOpenβπ)) |
7 | 1, 6 | eqtr4id 2792 |
. 2
β’ (π
β Ring β π½ = ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π})) |
8 | | nfv 1918 |
. . 3
β’
β²π π
β Ring |
9 | | nfcv 2904 |
. . 3
β’
β²π ran
(π β
(LIdealβπ
) β¦
{π β π β£ Β¬ π β π}) |
10 | | nfrab1 3425 |
. . 3
β’
β²π {π β π« π β£ (π β π ) β ran π} |
11 | | notrab 4275 |
. . . . . . . . . 10
β’ (π β {π β π β£ π β π}) = {π β π β£ Β¬ π β π} |
12 | 11 | eqeq2i 2746 |
. . . . . . . . 9
β’ (π = (π β {π β π β£ π β π}) β π = {π β π β£ Β¬ π β π}) |
13 | | ssrab2 4041 |
. . . . . . . . . . . 12
β’ {π β π β£ π β π} β π |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (π β π« π β {π β π β£ π β π} β π) |
15 | | elpwi 4571 |
. . . . . . . . . . 11
β’ (π β π« π β π β π) |
16 | | ssdifsym 4227 |
. . . . . . . . . . 11
β’ (({π β π β£ π β π} β π β§ π β π) β (π = (π β {π β π β£ π β π}) β {π β π β£ π β π} = (π β π ))) |
17 | 14, 15, 16 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π« π β (π = (π β {π β π β£ π β π}) β {π β π β£ π β π} = (π β π ))) |
18 | | eqcom 2740 |
. . . . . . . . . 10
β’ ({π β π β£ π β π} = (π β π ) β (π β π ) = {π β π β£ π β π}) |
19 | 17, 18 | bitrdi 287 |
. . . . . . . . 9
β’ (π β π« π β (π = (π β {π β π β£ π β π}) β (π β π ) = {π β π β£ π β π})) |
20 | 12, 19 | bitr3id 285 |
. . . . . . . 8
β’ (π β π« π β (π = {π β π β£ Β¬ π β π} β (π β π ) = {π β π β£ π β π})) |
21 | 20 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β Ring β§ π β π« π) β§ π β (LIdealβπ
)) β (π = {π β π β£ Β¬ π β π} β (π β π ) = {π β π β£ π β π})) |
22 | 21 | rexbidva 3170 |
. . . . . 6
β’ ((π
β Ring β§ π β π« π) β (βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π} β βπ β (LIdealβπ
)(π β π ) = {π β π β£ π β π})) |
23 | | zarcls.2 |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β π β£ π β π}) |
24 | 4 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
25 | 24 | rabex 5293 |
. . . . . . 7
β’ {π β π β£ π β π} β V |
26 | 23, 25 | elrnmpti 5919 |
. . . . . 6
β’ ((π β π ) β ran π β βπ β (LIdealβπ
)(π β π ) = {π β π β£ π β π}) |
27 | 22, 26 | bitr4di 289 |
. . . . 5
β’ ((π
β Ring β§ π β π« π) β (βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π} β (π β π ) β ran π)) |
28 | 27 | pm5.32da 580 |
. . . 4
β’ (π
β Ring β ((π β π« π β§ βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π}) β (π β π« π β§ (π β π ) β ran π))) |
29 | | ssrab2 4041 |
. . . . . . . . . 10
β’ {π β π β£ Β¬ π β π} β π |
30 | 24 | elpw2 5306 |
. . . . . . . . . 10
β’ ({π β π β£ Β¬ π β π} β π« π β {π β π β£ Β¬ π β π} β π) |
31 | 29, 30 | mpbir 230 |
. . . . . . . . 9
β’ {π β π β£ Β¬ π β π} β π« π |
32 | 31 | rgenw 3065 |
. . . . . . . 8
β’
βπ β
(LIdealβπ
){π β π β£ Β¬ π β π} β π« π |
33 | | eqid 2733 |
. . . . . . . . 9
β’ (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) = (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) |
34 | 33 | rnmptss 7074 |
. . . . . . . 8
β’
(βπ β
(LIdealβπ
){π β π β£ Β¬ π β π} β π« π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β π« π) |
35 | 32, 34 | ax-mp 5 |
. . . . . . 7
β’ ran
(π β
(LIdealβπ
) β¦
{π β π β£ Β¬ π β π}) β π« π |
36 | 35 | sseli 3944 |
. . . . . 6
β’ (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β π β π« π) |
37 | 36 | pm4.71ri 562 |
. . . . 5
β’ (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β (π β π« π β§ π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}))) |
38 | | vex 3451 |
. . . . . . 7
β’ π β V |
39 | 33 | elrnmpt 5915 |
. . . . . . 7
β’ (π β V β (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π})) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
β’ (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π}) |
41 | 40 | anbi2i 624 |
. . . . 5
β’ ((π β π« π β§ π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π})) β (π β π« π β§ βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π})) |
42 | 37, 41 | bitri 275 |
. . . 4
β’ (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β (π β π« π β§ βπ β (LIdealβπ
)π = {π β π β£ Β¬ π β π})) |
43 | | rabid 3426 |
. . . 4
β’ (π β {π β π« π β£ (π β π ) β ran π} β (π β π« π β§ (π β π ) β ran π)) |
44 | 28, 42, 43 | 3bitr4g 314 |
. . 3
β’ (π
β Ring β (π β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) β π β {π β π« π β£ (π β π ) β ran π})) |
45 | 8, 9, 10, 44 | eqrd 3967 |
. 2
β’ (π
β Ring β ran (π β (LIdealβπ
) β¦ {π β π β£ Β¬ π β π}) = {π β π« π β£ (π β π ) β ran π}) |
46 | 7, 45 | eqtrd 2773 |
1
β’ (π
β Ring β π½ = {π β π« π β£ (π β π ) β ran π}) |