Step | Hyp | Ref
| Expression |
1 | | rhmpreimacn.s |
. . 3
β’ (π β π β CRing) |
2 | | rhmpreimacn.u |
. . . 4
β’ π = (Specβπ) |
3 | | rhmpreimacn.k |
. . . 4
β’ πΎ = (TopOpenβπ) |
4 | | rhmpreimacn.b |
. . . 4
β’ π΅ = (PrmIdealβπ) |
5 | 2, 3, 4 | zartopon 32498 |
. . 3
β’ (π β CRing β πΎ β (TopOnβπ΅)) |
6 | 1, 5 | syl 17 |
. 2
β’ (π β πΎ β (TopOnβπ΅)) |
7 | | rhmpreimacn.r |
. . 3
β’ (π β π
β CRing) |
8 | | rhmpreimacn.t |
. . . 4
β’ π = (Specβπ
) |
9 | | rhmpreimacn.j |
. . . 4
β’ π½ = (TopOpenβπ) |
10 | | rhmpreimacn.a |
. . . 4
β’ π΄ = (PrmIdealβπ
) |
11 | 8, 9, 10 | zartopon 32498 |
. . 3
β’ (π
β CRing β π½ β (TopOnβπ΄)) |
12 | 7, 11 | syl 17 |
. 2
β’ (π β π½ β (TopOnβπ΄)) |
13 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π β π΅) β π β CRing) |
14 | | rhmpreimacn.f |
. . . . 5
β’ (π β πΉ β (π
RingHom π)) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π β π΅) β πΉ β (π
RingHom π)) |
16 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π΅) β π β π΅) |
17 | 16, 4 | eleqtrdi 2848 |
. . . 4
β’ ((π β§ π β π΅) β π β (PrmIdealβπ)) |
18 | 10 | rhmpreimaprmidl 32264 |
. . . 4
β’ (((π β CRing β§ πΉ β (π
RingHom π)) β§ π β (PrmIdealβπ)) β (β‘πΉ β π) β π΄) |
19 | 13, 15, 17, 18 | syl21anc 837 |
. . 3
β’ ((π β§ π β π΅) β (β‘πΉ β π) β π΄) |
20 | | rhmpreimacn.g |
. . 3
β’ πΊ = (π β π΅ β¦ (β‘πΉ β π)) |
21 | 19, 20 | fmptd 7067 |
. 2
β’ (π β πΊ:π΅βΆπ΄) |
22 | 4 | fvexi 6861 |
. . . . . . 7
β’ π΅ β V |
23 | 22 | rabex 5294 |
. . . . . 6
β’ {π β π΅ β£ π β π} β V |
24 | | sseq1 3974 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
25 | 24 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π β π΅ β£ π β π} = {π β π΅ β£ π β π}) |
26 | 25 | cbvmptv 5223 |
. . . . . 6
β’ (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) = (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) |
27 | 23, 26 | fnmpti 6649 |
. . . . 5
β’ (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) Fn (LIdealβπ) |
28 | 14 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β πΉ β (π
RingHom π)) |
29 | | rhmpreimacn.1 |
. . . . . . . . 9
β’ (π β ran πΉ = (Baseβπ)) |
30 | 29 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β ran πΉ = (Baseβπ)) |
31 | | simplr 768 |
. . . . . . . 8
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β π β (LIdealβπ
)) |
32 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
33 | | eqid 2737 |
. . . . . . . . 9
β’
(LIdealβπ
) =
(LIdealβπ
) |
34 | | eqid 2737 |
. . . . . . . . 9
β’
(LIdealβπ) =
(LIdealβπ) |
35 | 32, 33, 34 | rhmimaidl 32246 |
. . . . . . . 8
β’ ((πΉ β (π
RingHom π) β§ ran πΉ = (Baseβπ) β§ π β (LIdealβπ
)) β (πΉ β π) β (LIdealβπ)) |
36 | 28, 30, 31, 35 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β (πΉ β π) β (LIdealβπ)) |
37 | | fveqeq2 6856 |
. . . . . . . 8
β’ (π = (πΉ β π) β (((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯) β ((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})β(πΉ β π)) = (β‘πΊ β π₯))) |
38 | 37 | adantl 483 |
. . . . . . 7
β’
(((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β§ π = (πΉ β π)) β (((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯) β ((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})β(πΉ β π)) = (β‘πΊ β π₯))) |
39 | 7 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β π
β CRing) |
40 | 1 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β π β CRing) |
41 | 24 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = π β {π β π΄ β£ π β π} = {π β π΄ β£ π β π}) |
42 | 41 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) = (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) |
43 | 8, 2, 10, 4, 9, 3,
20, 39, 40, 28, 30, 31, 42, 26 | rhmpreimacnlem 32505 |
. . . . . . . 8
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β ((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})β(πΉ β π)) = (β‘πΊ β ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ))) |
44 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) |
45 | 44 | imaeq2d 6018 |
. . . . . . . 8
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β (β‘πΊ β ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ)) = (β‘πΊ β π₯)) |
46 | 43, 45 | eqtrd 2777 |
. . . . . . 7
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β ((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})β(πΉ β π)) = (β‘πΊ β π₯)) |
47 | 36, 38, 46 | rspcedvd 3586 |
. . . . . 6
β’ ((((π β§ π₯ β (Clsdβπ½)) β§ π β (LIdealβπ
)) β§ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) β βπ β (LIdealβπ)((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯)) |
48 | 10 | fvexi 6861 |
. . . . . . . . 9
β’ π΄ β V |
49 | 48 | rabex 5294 |
. . . . . . . 8
β’ {π β π΄ β£ π β π} β V |
50 | 49, 42 | fnmpti 6649 |
. . . . . . 7
β’ (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) Fn (LIdealβπ
) |
51 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β (Clsdβπ½)) β π₯ β (Clsdβπ½)) |
52 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Clsdβπ½)) β π
β CRing) |
53 | 8, 9, 10, 42 | zartopn 32496 |
. . . . . . . . . 10
β’ (π
β CRing β (π½ β (TopOnβπ΄) β§ ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) = (Clsdβπ½))) |
54 | 53 | simprd 497 |
. . . . . . . . 9
β’ (π
β CRing β ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) = (Clsdβπ½)) |
55 | 52, 54 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β (Clsdβπ½)) β ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) = (Clsdβπ½)) |
56 | 51, 55 | eleqtrrd 2841 |
. . . . . . 7
β’ ((π β§ π₯ β (Clsdβπ½)) β π₯ β ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})) |
57 | | fvelrnb 6908 |
. . . . . . . 8
β’ ((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) Fn (LIdealβπ
) β (π₯ β ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) β βπ β (LIdealβπ
)((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯)) |
58 | 57 | biimpa 478 |
. . . . . . 7
β’ (((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) Fn (LIdealβπ
) β§ π₯ β ran (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})) β βπ β (LIdealβπ
)((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) |
59 | 50, 56, 58 | sylancr 588 |
. . . . . 6
β’ ((π β§ π₯ β (Clsdβπ½)) β βπ β (LIdealβπ
)((π β (LIdealβπ
) β¦ {π β π΄ β£ π β π})βπ) = π₯) |
60 | 47, 59 | r19.29a 3160 |
. . . . 5
β’ ((π β§ π₯ β (Clsdβπ½)) β βπ β (LIdealβπ)((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯)) |
61 | | fvelrnb 6908 |
. . . . . 6
β’ ((π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) Fn (LIdealβπ) β ((β‘πΊ β π₯) β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) β βπ β (LIdealβπ)((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯))) |
62 | 61 | biimpar 479 |
. . . . 5
β’ (((π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) Fn (LIdealβπ) β§ βπ β (LIdealβπ)((π β (LIdealβπ) β¦ {π β π΅ β£ π β π})βπ) = (β‘πΊ β π₯)) β (β‘πΊ β π₯) β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π})) |
63 | 27, 60, 62 | sylancr 588 |
. . . 4
β’ ((π β§ π₯ β (Clsdβπ½)) β (β‘πΊ β π₯) β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π})) |
64 | 2, 3, 4, 26 | zartopn 32496 |
. . . . . . 7
β’ (π β CRing β (πΎ β (TopOnβπ΅) β§ ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) = (ClsdβπΎ))) |
65 | 64 | simprd 497 |
. . . . . 6
β’ (π β CRing β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) = (ClsdβπΎ)) |
66 | 1, 65 | syl 17 |
. . . . 5
β’ (π β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) = (ClsdβπΎ)) |
67 | 66 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (Clsdβπ½)) β ran (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) = (ClsdβπΎ)) |
68 | 63, 67 | eleqtrd 2840 |
. . 3
β’ ((π β§ π₯ β (Clsdβπ½)) β (β‘πΊ β π₯) β (ClsdβπΎ)) |
69 | 68 | ralrimiva 3144 |
. 2
β’ (π β βπ₯ β (Clsdβπ½)(β‘πΊ β π₯) β (ClsdβπΎ)) |
70 | | iscncl 22636 |
. . 3
β’ ((πΎ β (TopOnβπ΅) β§ π½ β (TopOnβπ΄)) β (πΊ β (πΎ Cn π½) β (πΊ:π΅βΆπ΄ β§ βπ₯ β (Clsdβπ½)(β‘πΊ β π₯) β (ClsdβπΎ)))) |
71 | 70 | biimpar 479 |
. 2
β’ (((πΎ β (TopOnβπ΅) β§ π½ β (TopOnβπ΄)) β§ (πΊ:π΅βΆπ΄ β§ βπ₯ β (Clsdβπ½)(β‘πΊ β π₯) β (ClsdβπΎ))) β πΊ β (πΎ Cn π½)) |
72 | 6, 12, 21, 69, 71 | syl22anc 838 |
1
β’ (π β πΊ β (πΎ Cn π½)) |