Step | Hyp | Ref
| Expression |
1 | | ssrab2 4041 |
. . . . . . . 8
β’ {π β π β£ π β π} β π |
2 | | zarcls.1 |
. . . . . . . . . 10
β’ π = (PrmIdealβπ
) |
3 | 2 | fvexi 6860 |
. . . . . . . . 9
β’ π β V |
4 | 3 | elpw2 5306 |
. . . . . . . 8
β’ ({π β π β£ π β π} β π« π β {π β π β£ π β π} β π) |
5 | 1, 4 | mpbir 230 |
. . . . . . 7
β’ {π β π β£ π β π} β π« π |
6 | 5 | rgenw 3065 |
. . . . . 6
β’
βπ β
(LIdealβπ
){π β π β£ π β π} β π« π |
7 | | zarcls.2 |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β π β£ π β π}) |
8 | 7 | rnmptss 7074 |
. . . . . 6
β’
(βπ β
(LIdealβπ
){π β π β£ π β π} β π« π β ran π β π« π) |
9 | 6, 8 | ax-mp 5 |
. . . . 5
β’ ran π β π« π |
10 | 9 | a1i 11 |
. . . 4
β’ (π
β CRing β ran π β π« π) |
11 | | crngring 19984 |
. . . . 5
β’ (π
β CRing β π
β Ring) |
12 | 2 | rabeqi 3419 |
. . . . . . . . 9
β’ {π β π β£ π β π} = {π β (PrmIdealβπ
) β£ π β π} |
13 | 12 | mpteq2i 5214 |
. . . . . . . 8
β’ (π β (LIdealβπ
) β¦ {π β π β£ π β π}) = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
14 | 7, 13 | eqtri 2761 |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
15 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
16 | 14, 2, 15 | zarcls0 32513 |
. . . . . 6
β’ (π
β Ring β (πβ{(0gβπ
)}) = π) |
17 | 7 | funmpt2 6544 |
. . . . . . 7
β’ Fun π |
18 | | eqid 2733 |
. . . . . . . . 9
β’
(LIdealβπ
) =
(LIdealβπ
) |
19 | 18, 15 | lidl0 20734 |
. . . . . . . 8
β’ (π
β Ring β
{(0gβπ
)}
β (LIdealβπ
)) |
20 | 3 | rabex 5293 |
. . . . . . . . 9
β’ {π β π β£ π β π} β V |
21 | 20, 7 | dmmpti 6649 |
. . . . . . . 8
β’ dom π = (LIdealβπ
) |
22 | 19, 21 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π
β Ring β
{(0gβπ
)}
β dom π) |
23 | | fvelrn 7031 |
. . . . . . 7
β’ ((Fun
π β§
{(0gβπ
)}
β dom π) β (πβ{(0gβπ
)}) β ran π) |
24 | 17, 22, 23 | sylancr 588 |
. . . . . 6
β’ (π
β Ring β (πβ{(0gβπ
)}) β ran π) |
25 | 16, 24 | eqeltrrd 2835 |
. . . . 5
β’ (π
β Ring β π β ran π) |
26 | 11, 25 | syl 17 |
. . . 4
β’ (π
β CRing β π β ran π) |
27 | 14 | zarclsint 32517 |
. . . 4
β’ ((π
β CRing β§ π§ β ran π β§ π§ β β
) β β© π§
β ran π) |
28 | 10, 26, 27 | ismred 17490 |
. . 3
β’ (π
β CRing β ran π β (Mooreβπ)) |
29 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
30 | 21, 29 | lidl1 20735 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) β dom
π) |
31 | 11, 30 | syl 17 |
. . . . . 6
β’ (π
β CRing β
(Baseβπ
) β dom
π) |
32 | 31, 21 | eleqtrdi 2844 |
. . . . 5
β’ (π
β CRing β
(Baseβπ
) β
(LIdealβπ
)) |
33 | 14, 29 | zarcls1 32514 |
. . . . . 6
β’ ((π
β CRing β§
(Baseβπ
) β
(LIdealβπ
)) β
((πβ(Baseβπ
)) = β
β
(Baseβπ
) =
(Baseβπ
))) |
34 | 29, 33 | mpbiri 258 |
. . . . 5
β’ ((π
β CRing β§
(Baseβπ
) β
(LIdealβπ
)) β
(πβ(Baseβπ
)) = β
) |
35 | 32, 34 | mpdan 686 |
. . . 4
β’ (π
β CRing β (πβ(Baseβπ
)) = β
) |
36 | 17 | a1i 11 |
. . . . 5
β’ (π
β CRing β Fun π) |
37 | | fvelrn 7031 |
. . . . 5
β’ ((Fun
π β§ (Baseβπ
) β dom π) β (πβ(Baseβπ
)) β ran π) |
38 | 36, 31, 37 | syl2anc 585 |
. . . 4
β’ (π
β CRing β (πβ(Baseβπ
)) β ran π) |
39 | 35, 38 | eqeltrrd 2835 |
. . 3
β’ (π
β CRing β β
β ran π) |
40 | 14 | zarclsun 32515 |
. . 3
β’ ((π
β CRing β§ π₯ β ran π β§ π¦ β ran π) β (π₯ βͺ π¦) β ran π) |
41 | | eqid 2733 |
. . 3
β’ {π β π« π β£ (π β π ) β ran π} = {π β π« π β£ (π β π ) β ran π} |
42 | 28, 39, 40, 41 | mretopd 22466 |
. 2
β’ (π
β CRing β ({π β π« π β£ (π β π ) β ran π} β (TopOnβπ) β§ ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π}))) |
43 | | zartop.1 |
. . . . . 6
β’ π = (Specβπ
) |
44 | | zartop.2 |
. . . . . 6
β’ π½ = (TopOpenβπ) |
45 | 43, 44, 2, 7 | zarcls 32519 |
. . . . 5
β’ (π
β Ring β π½ = {π β π« π β£ (π β π ) β ran π}) |
46 | 11, 45 | syl 17 |
. . . 4
β’ (π
β CRing β π½ = {π β π« π β£ (π β π ) β ran π}) |
47 | 46 | eleq1d 2819 |
. . 3
β’ (π
β CRing β (π½ β (TopOnβπ) β {π β π« π β£ (π β π ) β ran π} β (TopOnβπ))) |
48 | 46 | fveq2d 6850 |
. . . 4
β’ (π
β CRing β
(Clsdβπ½) =
(Clsdβ{π β
π« π β£ (π β π ) β ran π})) |
49 | 48 | eqeq2d 2744 |
. . 3
β’ (π
β CRing β (ran π = (Clsdβπ½) β ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π}))) |
50 | 47, 49 | anbi12d 632 |
. 2
β’ (π
β CRing β ((π½ β (TopOnβπ) β§ ran π = (Clsdβπ½)) β ({π β π« π β£ (π β π ) β ran π} β (TopOnβπ) β§ ran π = (Clsdβ{π β π« π β£ (π β π ) β ran π})))) |
51 | 42, 50 | mpbird 257 |
1
β’ (π
β CRing β (π½ β (TopOnβπ) β§ ran π = (Clsdβπ½))) |