| Step | Hyp | Ref
| Expression |
|---|
| 1 | | zartop.2 |
. . 3
β’ π½ = (TopOpenβπ) |
| 2 | | zartop.1 |
. . . . 5
β’ π = (Specβπ
) |
| 3 | | eqid 2731 |
. . . . 5
β’
(LIdealβπ
) =
(LIdealβπ
) |
| 4 | | eqid 2731 |
. . . . 5
β’
(PrmIdealβπ
) =
(PrmIdealβπ
) |
| 5 | | eqid 2731 |
. . . . 5
β’ ran
(π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) = ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) |
| 6 | 2, 3, 4, 5 | rspectopn 33146 |
. . . 4
β’ (π
β Ring β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = (TopOpenβπ)) |
| 7 | 6 | adantr 480 |
. . 3
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β ran (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) = (TopOpenβπ)) |
| 8 | 1, 7 | eqtr4id 2790 |
. 2
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β π½ = ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π})) |
| 9 | | fvex 6904 |
. . . . . 6
β’
(PrmIdealβπ
)
β V |
| 10 | 9 | rabex 5332 |
. . . . 5
β’ {π β (PrmIdealβπ
) β£ Β¬ π β π} β V |
| 11 | | eqid 2731 |
. . . . 5
β’ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) |
| 12 | 10, 11 | fnmpti 6693 |
. . . 4
β’ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) Fn (LIdealβπ
) |
| 13 | 12 | a1i 11 |
. . 3
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) Fn (LIdealβπ
)) |
| 14 | | zar0ring.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
| 15 | | eqid 2731 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
| 16 | 14, 15 | 0ringidl 32814 |
. . . 4
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (LIdealβπ
) =
{{(0gβπ
)}}) |
| 17 | | snex 5431 |
. . . . . 6
β’
{(0gβπ
)} β V |
| 18 | 17 | a1i 11 |
. . . . 5
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β {(0gβπ
)} β V) |
| 19 | 18 | snn0d 4779 |
. . . 4
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β {{(0gβπ
)}} β β
) |
| 20 | 16, 19 | eqnetrd 3007 |
. . 3
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (LIdealβπ
)
β β
) |
| 21 | 14 | 0ringprmidl 32843 |
. . . . . . 7
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (PrmIdealβπ
) =
β
) |
| 22 | 21 | rabeqdv 3446 |
. . . . . 6
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β {π β
(PrmIdealβπ
) β£
Β¬ π β π} = {π β β
β£ Β¬ π β π}) |
| 23 | | rab0 4382 |
. . . . . 6
β’ {π β β
β£ Β¬
π β π} = β
|
| 24 | 22, 23 | eqtrdi 2787 |
. . . . 5
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β {π β
(PrmIdealβπ
) β£
Β¬ π β π} = β
) |
| 25 | 24 | mpteq2dv 5250 |
. . . 4
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) = (π β (LIdealβπ
) β¦ β
)) |
| 26 | | fconstmpt 5738 |
. . . 4
β’
((LIdealβπ
)
Γ {β
}) = (π
β (LIdealβπ
)
β¦ β
) |
| 27 | 25, 26 | eqtr4di 2789 |
. . 3
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) = ((LIdealβπ
) Γ
{β
})) |
| 28 | | fconst5 7209 |
. . . 4
β’ (((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) Fn (LIdealβπ
) β§ (LIdealβπ
) β β
) β ((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = ((LIdealβπ
) Γ {β
}) β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = {β
})) |
| 29 | 28 | biimpa 476 |
. . 3
β’ ((((π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) Fn (LIdealβπ
) β§ (LIdealβπ
) β β
) β§ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = ((LIdealβπ
) Γ {β
})) β ran (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ Β¬ π β π}) = {β
}) |
| 30 | 13, 20, 27, 29 | syl21anc 835 |
. 2
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β ran (π β
(LIdealβπ
) β¦
{π β
(PrmIdealβπ
) β£
Β¬ π β π}) = {β
}) |
| 31 | 8, 30 | eqtrd 2771 |
1
β’ ((π
β Ring β§
(β―βπ΅) = 1)
β π½ =
{β
}) |
