| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssrab2 4077 |
. . . . . . . 8
β’ {π β π β£ π β π} β π |
| 2 | | zarcls.1 |
. . . . . . . . . 10
β’ π = (PrmIdealβπ
) |
| 3 | 2 | fvexi 6905 |
. . . . . . . . 9
β’ π β V |
| 4 | 3 | elpw2 5345 |
. . . . . . . 8
β’ ({π β π β£ π β π} β π« π β {π β π β£ π β π} β π) |
| 5 | 1, 4 | mpbir 230 |
. . . . . . 7
β’ {π β π β£ π β π} β π« π |
| 6 | 5 | rgenw 3065 |
. . . . . 6
β’
βπ β
(LIdealβπ
){π β π β£ π β π} β π« π |
| 7 | | zarcls.2 |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β π β£ π β π}) |
| 8 | 7 | rnmptss 7121 |
. . . . . 6
β’
(βπ β
(LIdealβπ
){π β π β£ π β π} β π« π β ran π β π« π) |
| 9 | 6, 8 | ax-mp 5 |
. . . . 5
β’ ran π β π« π |
| 10 | 9 | a1i 11 |
. . . 4
β’ (π
β CRing β ran π β π« π) |
| 11 | | crngring 20067 |
. . . . 5
β’ (π
β CRing β π
β Ring) |
| 12 | 2 | rabeqi 3445 |
. . . . . . . . 9
β’ {π β π β£ π β π} = {π β (PrmIdealβπ
) β£ π β π} |
| 13 | 12 | mpteq2i 5253 |
. . . . . . . 8
β’ (π β (LIdealβπ
) β¦ {π β π β£ π β π}) = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
| 14 | 7, 13 | eqtri 2760 |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
| 15 | | eqid 2732 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
| 16 | 14, 2, 15 | zarcls0 32843 |
. . . . . 6
β’ (π
β Ring β (πβ{(0gβπ
)}) = π) |
| 17 | 7 | funmpt2 6587 |
. . . . . . 7
β’ Fun π |
| 18 | | eqid 2732 |
. . . . . . . . 9
β’
(LIdealβπ
) =
(LIdealβπ
) |
| 19 | 18, 15 | lidl0 20843 |
. . . . . . . 8
β’ (π
β Ring β
{(0gβπ
)}
β (LIdealβπ
)) |
| 20 | 3 | rabex 5332 |
. . . . . . . . 9
β’ {π β π β£ π β π} β V |
| 21 | 20, 7 | dmmpti 6694 |
. . . . . . . 8
β’ dom π = (LIdealβπ
) |
| 22 | 19, 21 | eleqtrrdi 2844 |
. . . . . . 7
β’ (π
β Ring β
{(0gβπ
)}
β dom π) |
| 23 | | fvelrn 7078 |
. . . . . . 7
β’ ((Fun
π β§
{(0gβπ
)}
β dom π) β (πβ{(0gβπ
)}) β ran π) |
| 24 | 17, 22, 23 | sylancr 587 |
. . . . . 6
β’ (π
β Ring β (πβ{(0gβπ
)}) β ran π) |
| 25 | 16, 24 | eqeltrrd 2834 |
. . . . 5
β’ (π
β Ring β π β ran π) |
| 26 | 11, 25 | syl 17 |
. . . 4
β’ (π
β CRing β π β ran π) |
| 27 | 14 | zarclsint 32847 |
. . . 4
β’ ((π
β CRing β§ π§ β ran π β§ π§ β β
) β β© π§
β ran π) |
| 28 | 10, 26, 27 | ismred 17545 |
. . 3
β’ (π
β CRing β ran π β (Mooreβπ)) |
| 29 | | eqid 2732 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
| 30 | 21, 29 | lidl1 20844 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) β dom
π) |
| 31 | 11, 30 | syl 17 |
. . . . . 6
β’ (π
β CRing β
(Baseβπ
) β dom
π) |
| 32 | 31, 21 | eleqtrdi 2843 |
. . . . 5
β’ (π
β CRing β
(Baseβπ
) β
(LIdealβπ
)) |
| 33 | 14, 29 | zarcls1 32844 |
. . . . . 6
β’ ((π
β CRing β§
(Baseβπ
) β
(LIdealβπ
)) β
((πβ(Baseβπ
)) = β
β
(Baseβπ
) =
(Baseβπ
))) |
| 34 | 29, 33 | mpbiri 257 |
. . . . 5
β’ ((π
β CRing β§
(Baseβπ
) β
(LIdealβπ
)) β
(πβ(Baseβπ
)) = β
) |
| 35 | 32, 34 | mpdan 685 |
. . . 4
β’ (π
β CRing β (πβ(Baseβπ
)) = β
) |
| 36 | 17 | a1i 11 |
. . . . 5
β’ (π
β CRing β Fun π) |
| 37 | | fvelrn 7078 |
. . . . 5
β’ ((Fun
π β§ (Baseβπ
) β dom π) β (πβ(Baseβπ
)) β ran π) |
| 38 | 36, 31, 37 | syl2anc 584 |
. . . 4
β’ (π
β CRing β (πβ(Baseβπ
)) β ran π) |
| 39 | 35, 38 | eqeltrrd 2834 |
. . 3
β’ (π
β CRing β β
β ran π) |
| 40 | 14 | zarclsun 32845 |
. . 3
β’ ((π
β CRing β§ π₯ β ran π β§ π¦ β ran π) β (π₯ βͺ π¦) β ran π) |
| 41 | | eqid 2732 |
. . 3
β’ {π β π« π β£ (π β π ) β ran π} = {π β π« π β£ (π β π ) β ran π} |
| 42 | 28, 39, 40, 41 | mretopd 22595 |
. 2
β’ (π
β CRing β ({π β π« π β£ (π β π ) β ran π} β (TopOnβπ) β§ ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π}))) |
| 43 | | zartop.1 |
. . . . . 6
β’ π = (Specβπ
) |
| 44 | | zartop.2 |
. . . . . 6
β’ π½ = (TopOpenβπ) |
| 45 | 43, 44, 2, 7 | zarcls 32849 |
. . . . 5
β’ (π
β Ring β π½ = {π β π« π β£ (π β π ) β ran π}) |
| 46 | 11, 45 | syl 17 |
. . . 4
β’ (π
β CRing β π½ = {π β π« π β£ (π β π ) β ran π}) |
| 47 | 46 | eleq1d 2818 |
. . 3
β’ (π
β CRing β (π½ β (TopOnβπ) β {π β π« π β£ (π β π ) β ran π} β (TopOnβπ))) |
| 48 | 46 | fveq2d 6895 |
. . . 4
β’ (π
β CRing β
(Clsdβπ½) =
(Clsdβ{π β
π« π β£ (π β π ) β ran π})) |
| 49 | 48 | eqeq2d 2743 |
. . 3
β’ (π
β CRing β (ran π = (Clsdβπ½) β ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π}))) |
| 50 | 47, 49 | anbi12d 631 |
. 2
β’ (π
β CRing β ((π½ β (TopOnβπ) β§ ran π = (Clsdβπ½)) β ({π β π« π β£ (π β π ) β ran π} β (TopOnβπ) β§ ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π})))) |
| 51 | 42, 50 | mpbird 256 |
1
β’ (π
β CRing β (π½ β (TopOnβπ) β§ ran π = (Clsdβπ½))) |
