Step | Hyp | Ref
| Expression |
1 | | zartop.1 |
. . . 4
β’ π = (Specβπ
) |
2 | | zartop.2 |
. . . 4
β’ π½ = (TopOpenβπ) |
3 | 1, 2 | zartop 32497 |
. . 3
β’ (π
β CRing β π½ β Top) |
4 | | sseq2 3975 |
. . . . . . . . . . 11
β’ (π = π₯ β (π₯ β π β π₯ β π₯)) |
5 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π₯ β (PrmIdealβπ
)) β π₯ β (PrmIdealβπ
)) |
6 | | ssidd 3972 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π₯ β (PrmIdealβπ
)) β π₯ β π₯) |
7 | 4, 5, 6 | elrabd 3652 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π₯ β (PrmIdealβπ
)) β π₯ β {π β (PrmIdealβπ
) β£ π₯ β π}) |
8 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π₯ β {π β (PrmIdealβπ
) β£ π₯ β π}) |
9 | | sseq1 3974 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
10 | 9 | rabbidv 3418 |
. . . . . . . . . . . . 13
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
11 | 10 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
12 | | crngring 19983 |
. . . . . . . . . . . . . 14
β’ (π
β CRing β π
β Ring) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β π
β Ring) |
14 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β π₯ β (PrmIdealβπ
)) |
15 | | prmidlidl 32256 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π₯ β (PrmIdealβπ
)) β π₯ β (LIdealβπ
)) |
16 | 13, 14, 15 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β π₯ β (LIdealβπ
)) |
17 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’
(PrmIdealβπ
)
β V |
18 | 17 | rabex 5294 |
. . . . . . . . . . . . 13
β’ {π β (PrmIdealβπ
) β£ π₯ β π} β V |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β {π β (PrmIdealβπ
) β£ π₯ β π} β V) |
20 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π β π β π₯ β π)) |
21 | 20 | rabbidv 3418 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π₯ β π}) |
22 | 21 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π = π₯ β {π β (PrmIdealβπ
) β£ π₯ β π} = {π β (PrmIdealβπ
) β£ π β π}) |
23 | 22 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = π₯) β {π β (PrmIdealβπ
) β£ π₯ β π} = {π β (PrmIdealβπ
) β£ π β π}) |
24 | 11, 16, 19, 23 | elrnmptdv 5922 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β {π β (PrmIdealβπ
) β£ π₯ β π} β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
25 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π₯ β π}) β π = {π β (PrmIdealβπ
) β£ π₯ β π}) |
26 | 25 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π₯ β π}) β (π₯ β π β π₯ β {π β (PrmIdealβπ
) β£ π₯ β π})) |
27 | 25 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π₯ β π}) β (π¦ β π β π¦ β {π β (PrmIdealβπ
) β£ π₯ β π})) |
28 | 26, 27 | bibi12d 346 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π₯ β π}) β ((π₯ β π β π¦ β π) β (π₯ β {π β (PrmIdealβπ
) β£ π₯ β π} β π¦ β {π β (PrmIdealβπ
) β£ π₯ β π}))) |
29 | 24, 28 | rspcdv 3576 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β (βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β (π₯ β {π β (PrmIdealβπ
) β£ π₯ β π} β π¦ β {π β (PrmIdealβπ
) β£ π₯ β π}))) |
30 | 29 | imp 408 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β (π₯ β {π β (PrmIdealβπ
) β£ π₯ β π} β π¦ β {π β (PrmIdealβπ
) β£ π₯ β π})) |
31 | 8, 30 | mpbid 231 |
. . . . . . . 8
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π¦ β {π β (PrmIdealβπ
) β£ π₯ β π}) |
32 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π = π¦ β (π₯ β π β π₯ β π¦)) |
33 | 32 | elrab 3650 |
. . . . . . . . 9
β’ (π¦ β {π β (PrmIdealβπ
) β£ π₯ β π} β (π¦ β (PrmIdealβπ
) β§ π₯ β π¦)) |
34 | 33 | simprbi 498 |
. . . . . . . 8
β’ (π¦ β {π β (PrmIdealβπ
) β£ π₯ β π} β π₯ β π¦) |
35 | 31, 34 | syl 17 |
. . . . . . 7
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π₯ β π¦) |
36 | | sseq2 3975 |
. . . . . . . . . . 11
β’ (π = π¦ β (π¦ β π β π¦ β π¦)) |
37 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π¦ β (PrmIdealβπ
)) β π¦ β (PrmIdealβπ
)) |
38 | | ssidd 3972 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π¦ β (PrmIdealβπ
)) β π¦ β π¦) |
39 | 36, 37, 38 | elrabd 3652 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π¦ β (PrmIdealβπ
)) β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π}) |
40 | 39 | ad4ant13 750 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π}) |
41 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β π¦ β (PrmIdealβπ
)) |
42 | | prmidlidl 32256 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β (PrmIdealβπ
)) β π¦ β (LIdealβπ
)) |
43 | 13, 41, 42 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β π¦ β (LIdealβπ
)) |
44 | 17 | rabex 5294 |
. . . . . . . . . . . . 13
β’ {π β (PrmIdealβπ
) β£ π¦ β π} β V |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β {π β (PrmIdealβπ
) β£ π¦ β π} β V) |
46 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π = π¦ β (π β π β π¦ β π)) |
47 | 46 | rabbidv 3418 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π¦ β π}) |
48 | 47 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π = π¦ β {π β (PrmIdealβπ
) β£ π¦ β π} = {π β (PrmIdealβπ
) β£ π β π}) |
49 | 48 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = π¦) β {π β (PrmIdealβπ
) β£ π¦ β π} = {π β (PrmIdealβπ
) β£ π β π}) |
50 | 11, 43, 45, 49 | elrnmptdv 5922 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β {π β (PrmIdealβπ
) β£ π¦ β π} β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
51 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π¦ β π}) β π = {π β (PrmIdealβπ
) β£ π¦ β π}) |
52 | 51 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π¦ β π}) β (π₯ β π β π₯ β {π β (PrmIdealβπ
) β£ π¦ β π})) |
53 | 51 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π¦ β π}) β (π¦ β π β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π})) |
54 | 52, 53 | bibi12d 346 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π¦ β π}) β ((π₯ β π β π¦ β π) β (π₯ β {π β (PrmIdealβπ
) β£ π¦ β π} β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π}))) |
55 | 50, 54 | rspcdv 3576 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β (βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β (π₯ β {π β (PrmIdealβπ
) β£ π¦ β π} β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π}))) |
56 | 55 | imp 408 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β (π₯ β {π β (PrmIdealβπ
) β£ π¦ β π} β π¦ β {π β (PrmIdealβπ
) β£ π¦ β π})) |
57 | 40, 56 | mpbird 257 |
. . . . . . . 8
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π₯ β {π β (PrmIdealβπ
) β£ π¦ β π}) |
58 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π = π₯ β (π¦ β π β π¦ β π₯)) |
59 | 58 | elrab 3650 |
. . . . . . . . 9
β’ (π₯ β {π β (PrmIdealβπ
) β£ π¦ β π} β (π₯ β (PrmIdealβπ
) β§ π¦ β π₯)) |
60 | 59 | simprbi 498 |
. . . . . . . 8
β’ (π₯ β {π β (PrmIdealβπ
) β£ π¦ β π} β π¦ β π₯) |
61 | 57, 60 | syl 17 |
. . . . . . 7
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π¦ β π₯) |
62 | 35, 61 | eqssd 3966 |
. . . . . 6
β’ ((((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β§ βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π)) β π₯ = π¦) |
63 | 62 | ex 414 |
. . . . 5
β’ (((π
β CRing β§ π₯ β (PrmIdealβπ
)) β§ π¦ β (PrmIdealβπ
)) β (βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β π₯ = π¦)) |
64 | 63 | anasss 468 |
. . . 4
β’ ((π
β CRing β§ (π₯ β (PrmIdealβπ
) β§ π¦ β (PrmIdealβπ
))) β (βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β π₯ = π¦)) |
65 | 64 | ralrimivva 3198 |
. . 3
β’ (π
β CRing β
βπ₯ β
(PrmIdealβπ
)βπ¦ β (PrmIdealβπ
)(βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β π₯ = π¦)) |
66 | 3, 65 | jca 513 |
. 2
β’ (π
β CRing β (π½ β Top β§ βπ₯ β (PrmIdealβπ
)βπ¦ β (PrmIdealβπ
)(βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β π₯ = π¦))) |
67 | | eqid 2737 |
. . . . 5
β’
(PrmIdealβπ
) =
(PrmIdealβπ
) |
68 | 1, 2, 67 | zartopon 32498 |
. . . 4
β’ (π
β CRing β π½ β
(TopOnβ(PrmIdealβπ
))) |
69 | | toponuni 22279 |
. . . 4
β’ (π½ β
(TopOnβ(PrmIdealβπ
)) β (PrmIdealβπ
) = βͺ π½) |
70 | 68, 69 | syl 17 |
. . 3
β’ (π
β CRing β
(PrmIdealβπ
) = βͺ π½) |
71 | 1, 2, 67, 11 | zartopn 32496 |
. . . 4
β’ (π
β CRing β (π½ β
(TopOnβ(PrmIdealβπ
)) β§ ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (Clsdβπ½))) |
72 | 71 | simprd 497 |
. . 3
β’ (π
β CRing β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) = (Clsdβπ½)) |
73 | 70, 72 | ist0cld 32454 |
. 2
β’ (π
β CRing β (π½ β Kol2 β (π½ β Top β§ βπ₯ β (PrmIdealβπ
)βπ¦ β (PrmIdealβπ
)(βπ β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})(π₯ β π β π¦ β π) β π₯ = π¦)))) |
74 | 66, 73 | mpbird 257 |
1
β’ (π
β CRing β π½ β Kol2) |