Step | Hyp | Ref
| Expression |
1 | | zartop.1 |
. . . 4
β’ π = (Specβπ
) |
2 | | zartop.2 |
. . . 4
β’ π½ = (TopOpenβπ) |
3 | 1, 2 | zartop 32851 |
. . 3
β’ (π
β CRing β π½ β Top) |
4 | | zarmxt1.1 |
. . . 4
β’ π = (MaxIdealβπ
) |
5 | 4 | fvexi 6905 |
. . 3
β’ π β V |
6 | | zarmxt1.2 |
. . . 4
β’ π = (π½ βΎt π) |
7 | | resttop 22663 |
. . . 4
β’ ((π½ β Top β§ π β V) β (π½ βΎt π) β Top) |
8 | 6, 7 | eqeltrid 2837 |
. . 3
β’ ((π½ β Top β§ π β V) β π β Top) |
9 | 3, 5, 8 | sylancl 586 |
. 2
β’ (π
β CRing β π β Top) |
10 | | eqid 2732 |
. . . . . . . . . . 11
β’
(LSSumβ(mulGrpβπ
)) = (LSSumβ(mulGrpβπ
)) |
11 | 10 | mxidlprm 32581 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π β (PrmIdealβπ
)) |
12 | 11 | ex 413 |
. . . . . . . . 9
β’ (π
β CRing β (π β (MaxIdealβπ
) β π β (PrmIdealβπ
))) |
13 | 12 | ssrdv 3988 |
. . . . . . . 8
β’ (π
β CRing β
(MaxIdealβπ
) β
(PrmIdealβπ
)) |
14 | 13 | adantr 481 |
. . . . . . 7
β’ ((π
β CRing β§ π β βͺ π)
β (MaxIdealβπ
)
β (PrmIdealβπ
)) |
15 | | eqid 2732 |
. . . . . . 7
β’
(PrmIdealβπ
) =
(PrmIdealβπ
) |
16 | 14, 4, 15 | 3sstr4g 4027 |
. . . . . 6
β’ ((π
β CRing β§ π β βͺ π)
β π β
(PrmIdealβπ
)) |
17 | | sseq2 4008 |
. . . . . . . . . . . . 13
β’ (π = π β (π β π β π β π)) |
18 | 17 | cbvrabv 3442 |
. . . . . . . . . . . 12
β’ {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π} |
19 | | sseq1 4007 |
. . . . . . . . . . . . 13
β’ (π = π β (π β π β π β π)) |
20 | 19 | rabbidv 3440 |
. . . . . . . . . . . 12
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
21 | 18, 20 | eqtrid 2784 |
. . . . . . . . . . 11
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
22 | 21 | cbvmptv 5261 |
. . . . . . . . . 10
β’ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
23 | 1, 2, 15, 22 | zartopn 32850 |
. . . . . . . . 9
β’ (π
β CRing β (π½ β
(TopOnβ(PrmIdealβπ
)) β§ ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (Clsdβπ½))) |
24 | 23 | adantr 481 |
. . . . . . . 8
β’ ((π
β CRing β§ π β βͺ π)
β (π½ β
(TopOnβ(PrmIdealβπ
)) β§ ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (Clsdβπ½))) |
25 | 24 | simpld 495 |
. . . . . . 7
β’ ((π
β CRing β§ π β βͺ π)
β π½ β
(TopOnβ(PrmIdealβπ
))) |
26 | | toponuni 22415 |
. . . . . . 7
β’ (π½ β
(TopOnβ(PrmIdealβπ
)) β (PrmIdealβπ
) = βͺ π½) |
27 | 25, 26 | syl 17 |
. . . . . 6
β’ ((π
β CRing β§ π β βͺ π)
β (PrmIdealβπ
) =
βͺ π½) |
28 | 16, 27 | sseqtrd 4022 |
. . . . 5
β’ ((π
β CRing β§ π β βͺ π)
β π β βͺ π½) |
29 | | simpl 483 |
. . . . . . . 8
β’ ((π
β CRing β§ π β βͺ π)
β π
β
CRing) |
30 | 29 | crngringd 20068 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β βͺ π)
β π
β
Ring) |
31 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π
β CRing β§ π β βͺ π)
β π β βͺ π) |
32 | 6 | unieqi 4921 |
. . . . . . . . . . . 12
β’ βͺ π =
βͺ (π½ βΎt π) |
33 | 31, 32 | eleqtrdi 2843 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π β βͺ π)
β π β βͺ (π½
βΎt π)) |
34 | 3 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π
β CRing β§ π β βͺ π)
β π½ β
Top) |
35 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
36 | 35 | restuni 22665 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π β βͺ π½)
β π = βͺ (π½
βΎt π)) |
37 | 34, 28, 36 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π β βͺ π)
β π = βͺ (π½
βΎt π)) |
38 | 33, 37 | eleqtrrd 2836 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π β βͺ π)
β π β π) |
39 | 38, 4 | eleqtrdi 2843 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β βͺ π)
β π β
(MaxIdealβπ
)) |
40 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
41 | 40 | mxidlidl 32574 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β π β (LIdealβπ
)) |
42 | 30, 39, 41 | syl2anc 584 |
. . . . . . . 8
β’ ((π
β CRing β§ π β βͺ π)
β π β
(LIdealβπ
)) |
43 | | eqid 2732 |
. . . . . . . . . 10
β’
(LIdealβπ
) =
(LIdealβπ
) |
44 | 22, 43 | zarclssn 32848 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β (LIdealβπ
)) β ({π} = ((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})βπ) β π β (MaxIdealβπ
))) |
45 | 44 | biimpar 478 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (MaxIdealβπ
)) β {π} = ((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})βπ)) |
46 | 29, 42, 39, 45 | syl21anc 836 |
. . . . . . 7
β’ ((π
β CRing β§ π β βͺ π)
β {π} = ((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})βπ)) |
47 | 22 | funmpt2 6587 |
. . . . . . . 8
β’ Fun
(π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π}) |
48 | | fvex 6904 |
. . . . . . . . . . 11
β’
(PrmIdealβπ
)
β V |
49 | 48 | rabex 5332 |
. . . . . . . . . 10
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
50 | 49, 22 | dmmpti 6694 |
. . . . . . . . 9
β’ dom
(π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π}) = (LIdealβπ
) |
51 | 42, 50 | eleqtrrdi 2844 |
. . . . . . . 8
β’ ((π
β CRing β§ π β βͺ π)
β π β dom (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
52 | | fvelrn 7078 |
. . . . . . . 8
β’ ((Fun
(π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π}) β§ π β dom (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) β ((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})βπ) β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
53 | 47, 51, 52 | sylancr 587 |
. . . . . . 7
β’ ((π
β CRing β§ π β βͺ π)
β ((π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π})βπ) β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
54 | 46, 53 | eqeltrd 2833 |
. . . . . 6
β’ ((π
β CRing β§ π β βͺ π)
β {π} β ran
(π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π})) |
55 | 24 | simprd 496 |
. . . . . 6
β’ ((π
β CRing β§ π β βͺ π)
β ran (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
π β π}) = (Clsdβπ½)) |
56 | 54, 55 | eleqtrd 2835 |
. . . . 5
β’ ((π
β CRing β§ π β βͺ π)
β {π} β
(Clsdβπ½)) |
57 | 38 | snssd 4812 |
. . . . 5
β’ ((π
β CRing β§ π β βͺ π)
β {π} β π) |
58 | 35 | restcldi 22676 |
. . . . 5
β’ ((π β βͺ π½
β§ {π} β
(Clsdβπ½) β§ {π} β π) β {π} β (Clsdβ(π½ βΎt π))) |
59 | 28, 56, 57, 58 | syl3anc 1371 |
. . . 4
β’ ((π
β CRing β§ π β βͺ π)
β {π} β
(Clsdβ(π½
βΎt π))) |
60 | 6 | fveq2i 6894 |
. . . 4
β’
(Clsdβπ) =
(Clsdβ(π½
βΎt π)) |
61 | 59, 60 | eleqtrrdi 2844 |
. . 3
β’ ((π
β CRing β§ π β βͺ π)
β {π} β
(Clsdβπ)) |
62 | 61 | ralrimiva 3146 |
. 2
β’ (π
β CRing β
βπ β βͺ π{π} β (Clsdβπ)) |
63 | | eqid 2732 |
. . 3
β’ βͺ π =
βͺ π |
64 | 63 | ist1 22824 |
. 2
β’ (π β Fre β (π β Top β§ βπ β βͺ π{π} β (Clsdβπ))) |
65 | 9, 62, 64 | sylanbrc 583 |
1
β’ (π
β CRing β π β Fre) |