Step | Hyp | Ref
| Expression |
1 | | rspecval 32509 |
. . . . 5
β’ (π
β Ring β
(Specβπ
) =
((IDLsrgβπ
)
βΎs (PrmIdealβπ
))) |
2 | | rspecbas.1 |
. . . . 5
β’ π = (Specβπ
) |
3 | | rspectopn.2 |
. . . . . 6
β’ π = (PrmIdealβπ
) |
4 | 3 | oveq2i 7372 |
. . . . 5
β’
((IDLsrgβπ
)
βΎs π) =
((IDLsrgβπ
)
βΎs (PrmIdealβπ
)) |
5 | 1, 2, 4 | 3eqtr4g 2798 |
. . . 4
β’ (π
β Ring β π = ((IDLsrgβπ
) βΎs π)) |
6 | 5 | fveq2d 6850 |
. . 3
β’ (π
β Ring β
(TopOpenβπ) =
(TopOpenβ((IDLsrgβπ
) βΎs π))) |
7 | | eqid 2733 |
. . . 4
β’
((IDLsrgβπ
)
βΎs π) =
((IDLsrgβπ
)
βΎs π) |
8 | | eqid 2733 |
. . . 4
β’
(TopOpenβ(IDLsrgβπ
)) = (TopOpenβ(IDLsrgβπ
)) |
9 | 7, 8 | resstopn 22560 |
. . 3
β’
((TopOpenβ(IDLsrgβπ
)) βΎt π) = (TopOpenβ((IDLsrgβπ
) βΎs π)) |
10 | 6, 9 | eqtr4di 2791 |
. 2
β’ (π
β Ring β
(TopOpenβπ) =
((TopOpenβ(IDLsrgβπ
)) βΎt π)) |
11 | | eqid 2733 |
. . . . 5
β’
(IDLsrgβπ
) =
(IDLsrgβπ
) |
12 | | rspectopn.1 |
. . . . 5
β’ πΌ = (LIdealβπ
) |
13 | | eqid 2733 |
. . . . 5
β’ ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) |
14 | 11, 12, 13 | idlsrgtset 32305 |
. . . 4
β’ (π
β Ring β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) = (TopSetβ(IDLsrgβπ
))) |
15 | 12 | fvexi 6860 |
. . . . . . . . . . 11
β’ πΌ β V |
16 | 15 | rabex 5293 |
. . . . . . . . . 10
β’ {π β πΌ β£ Β¬ π β π} β V |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β πΌ) β {π β πΌ β£ Β¬ π β π} β V) |
18 | | simp2 1138 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ π β πΌ) β§ π β πΌ β§ Β¬ π β π) β π β πΌ) |
19 | 11, 12 | idlsrgbas 32301 |
. . . . . . . . . . . . 13
β’ (π
β Ring β πΌ =
(Baseβ(IDLsrgβπ
))) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β πΌ) β πΌ = (Baseβ(IDLsrgβπ
))) |
21 | 20 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ π β πΌ) β§ π β πΌ β§ Β¬ π β π) β πΌ = (Baseβ(IDLsrgβπ
))) |
22 | 18, 21 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β πΌ) β§ π β πΌ β§ Β¬ π β π) β π β (Baseβ(IDLsrgβπ
))) |
23 | 22 | rabssdv 4036 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β πΌ) β {π β πΌ β£ Β¬ π β π} β (Baseβ(IDLsrgβπ
))) |
24 | 17, 23 | elpwd 4570 |
. . . . . . . 8
β’ ((π
β Ring β§ π β πΌ) β {π β πΌ β£ Β¬ π β π} β π«
(Baseβ(IDLsrgβπ
))) |
25 | 24 | ralrimiva 3140 |
. . . . . . 7
β’ (π
β Ring β
βπ β πΌ {π β πΌ β£ Β¬ π β π} β π«
(Baseβ(IDLsrgβπ
))) |
26 | | eqid 2733 |
. . . . . . . 8
β’ (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) = (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) |
27 | 26 | rnmptss 7074 |
. . . . . . 7
β’
(βπ β
πΌ {π β πΌ β£ Β¬ π β π} β π«
(Baseβ(IDLsrgβπ
)) β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β π«
(Baseβ(IDLsrgβπ
))) |
28 | 25, 27 | syl 17 |
. . . . . 6
β’ (π
β Ring β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β π«
(Baseβ(IDLsrgβπ
))) |
29 | 14, 28 | eqsstrrd 3987 |
. . . . 5
β’ (π
β Ring β
(TopSetβ(IDLsrgβπ
)) β π«
(Baseβ(IDLsrgβπ
))) |
30 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(IDLsrgβπ
)) = (Baseβ(IDLsrgβπ
)) |
31 | | eqid 2733 |
. . . . . 6
β’
(TopSetβ(IDLsrgβπ
)) = (TopSetβ(IDLsrgβπ
)) |
32 | 30, 31 | topnid 17325 |
. . . . 5
β’
((TopSetβ(IDLsrgβπ
)) β π«
(Baseβ(IDLsrgβπ
)) β (TopSetβ(IDLsrgβπ
)) =
(TopOpenβ(IDLsrgβπ
))) |
33 | 29, 32 | syl 17 |
. . . 4
β’ (π
β Ring β
(TopSetβ(IDLsrgβπ
)) = (TopOpenβ(IDLsrgβπ
))) |
34 | 14, 33 | eqtrd 2773 |
. . 3
β’ (π
β Ring β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) = (TopOpenβ(IDLsrgβπ
))) |
35 | 34 | oveq1d 7376 |
. 2
β’ (π
β Ring β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) = ((TopOpenβ(IDLsrgβπ
)) βΎt π)) |
36 | 15 | mptex 7177 |
. . . . . . 7
β’ (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β V |
37 | 36 | rnex 7853 |
. . . . . 6
β’ ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β V |
38 | 3 | fvexi 6860 |
. . . . . 6
β’ π β V |
39 | | elrest 17317 |
. . . . . 6
β’ ((ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β V β§ π β V) β (π₯ β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) β βπ¦ β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})π₯ = (π¦ β© π))) |
40 | 37, 38, 39 | mp2an 691 |
. . . . 5
β’ (π₯ β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) β βπ¦ β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})π₯ = (π¦ β© π)) |
41 | 16 | rgenw 3065 |
. . . . . . 7
β’
βπ β
πΌ {π β πΌ β£ Β¬ π β π} β V |
42 | | ineq1 4169 |
. . . . . . . . 9
β’ (π¦ = {π β πΌ β£ Β¬ π β π} β (π¦ β© π) = ({π β πΌ β£ Β¬ π β π} β© π)) |
43 | 42 | eqeq2d 2744 |
. . . . . . . 8
β’ (π¦ = {π β πΌ β£ Β¬ π β π} β (π₯ = (π¦ β© π) β π₯ = ({π β πΌ β£ Β¬ π β π} β© π))) |
44 | 26, 43 | rexrnmptw 7049 |
. . . . . . 7
β’
(βπ β
πΌ {π β πΌ β£ Β¬ π β π} β V β (βπ¦ β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})π₯ = (π¦ β© π) β βπ β πΌ π₯ = ({π β πΌ β£ Β¬ π β π} β© π))) |
45 | 41, 44 | ax-mp 5 |
. . . . . 6
β’
(βπ¦ β ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π})π₯ = (π¦ β© π) β βπ β πΌ π₯ = ({π β πΌ β£ Β¬ π β π} β© π)) |
46 | | inrab2 4271 |
. . . . . . . . 9
β’ ({π β πΌ β£ Β¬ π β π} β© π) = {π β (πΌ β© π) β£ Β¬ π β π} |
47 | | prmidlssidl 32272 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(PrmIdealβπ
) β
(LIdealβπ
)) |
48 | 47, 3, 12 | 3sstr4g 3993 |
. . . . . . . . . . 11
β’ (π
β Ring β π β πΌ) |
49 | | sseqin2 4179 |
. . . . . . . . . . 11
β’ (π β πΌ β (πΌ β© π) = π) |
50 | 48, 49 | sylib 217 |
. . . . . . . . . 10
β’ (π
β Ring β (πΌ β© π) = π) |
51 | 50 | rabeqdv 3421 |
. . . . . . . . 9
β’ (π
β Ring β {π β (πΌ β© π) β£ Β¬ π β π} = {π β π β£ Β¬ π β π}) |
52 | 46, 51 | eqtrid 2785 |
. . . . . . . 8
β’ (π
β Ring β ({π β πΌ β£ Β¬ π β π} β© π) = {π β π β£ Β¬ π β π}) |
53 | 52 | eqeq2d 2744 |
. . . . . . 7
β’ (π
β Ring β (π₯ = ({π β πΌ β£ Β¬ π β π} β© π) β π₯ = {π β π β£ Β¬ π β π})) |
54 | 53 | rexbidv 3172 |
. . . . . 6
β’ (π
β Ring β
(βπ β πΌ π₯ = ({π β πΌ β£ Β¬ π β π} β© π) β βπ β πΌ π₯ = {π β π β£ Β¬ π β π})) |
55 | 45, 54 | bitrid 283 |
. . . . 5
β’ (π
β Ring β
(βπ¦ β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})π₯ = (π¦ β© π) β βπ β πΌ π₯ = {π β π β£ Β¬ π β π})) |
56 | 40, 55 | bitrid 283 |
. . . 4
β’ (π
β Ring β (π₯ β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) β βπ β πΌ π₯ = {π β π β£ Β¬ π β π})) |
57 | | rspectopn.3 |
. . . . . 6
β’ π½ = ran (π β πΌ β¦ {π β π β£ Β¬ π β π}) |
58 | 57 | eleq2i 2826 |
. . . . 5
β’ (π₯ β π½ β π₯ β ran (π β πΌ β¦ {π β π β£ Β¬ π β π})) |
59 | | eqid 2733 |
. . . . . 6
β’ (π β πΌ β¦ {π β π β£ Β¬ π β π}) = (π β πΌ β¦ {π β π β£ Β¬ π β π}) |
60 | 38 | rabex 5293 |
. . . . . 6
β’ {π β π β£ Β¬ π β π} β V |
61 | 59, 60 | elrnmpti 5919 |
. . . . 5
β’ (π₯ β ran (π β πΌ β¦ {π β π β£ Β¬ π β π}) β βπ β πΌ π₯ = {π β π β£ Β¬ π β π}) |
62 | 58, 61 | bitri 275 |
. . . 4
β’ (π₯ β π½ β βπ β πΌ π₯ = {π β π β£ Β¬ π β π}) |
63 | 56, 62 | bitr4di 289 |
. . 3
β’ (π
β Ring β (π₯ β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) β π₯ β π½)) |
64 | 63 | eqrdv 2731 |
. 2
β’ (π
β Ring β (ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) βΎt π) = π½) |
65 | 10, 35, 64 | 3eqtr2rd 2780 |
1
β’ (π
β Ring β π½ = (TopOpenβπ)) |