Step | Hyp | Ref
| Expression |
1 | | crngring 20062 |
. . . 4
β’ (π
β CRing β π
β Ring) |
2 | | zartop.1 |
. . . . 5
β’ π = (Specβπ
) |
3 | | zartop.2 |
. . . . 5
β’ π½ = (TopOpenβπ) |
4 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
5 | 2, 3, 4 | zar0ring 32847 |
. . . 4
β’ ((π
β Ring β§
(β―β(Baseβπ
)) = 1) β π½ = {β
}) |
6 | 1, 5 | sylan 581 |
. . 3
β’ ((π
β CRing β§
(β―β(Baseβπ
)) = 1) β π½ = {β
}) |
7 | | 0cmp 22890 |
. . 3
β’ {β
}
β Comp |
8 | 6, 7 | eqeltrdi 2842 |
. 2
β’ ((π
β CRing β§
(β―β(Baseβπ
)) = 1) β π½ β Comp) |
9 | 2, 3 | zartop 32845 |
. . 3
β’ (π
β CRing β π½ β Top) |
10 | | zarcmplem.1 |
. . . . . . . . . . . . . . 15
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
11 | | fvex 6902 |
. . . . . . . . . . . . . . . 16
β’
(LIdealβπ
)
β V |
12 | 11 | mptex 7222 |
. . . . . . . . . . . . . . 15
β’ (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) β V |
13 | 10, 12 | eqeltri 2830 |
. . . . . . . . . . . . . 14
β’ π β V |
14 | | imaexg 7903 |
. . . . . . . . . . . . . 14
β’ (π β V β (π β (π supp (0gβπ
))) β V) |
15 | 13, 14 | mp1i 13 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β V) |
16 | | suppssdm 8159 |
. . . . . . . . . . . . . . 15
β’ (π supp (0gβπ
)) β dom π |
17 | | imass2 6099 |
. . . . . . . . . . . . . . 15
β’ ((π supp (0gβπ
)) β dom π β (π β (π supp (0gβπ
))) β (π β dom π)) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β (π β dom π)) |
19 | 10 | funmpt2 6585 |
. . . . . . . . . . . . . . 15
β’ Fun π |
20 | | ssidd 4005 |
. . . . . . . . . . . . . . . 16
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β dom π β dom π) |
21 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β π β ((Baseβπ
) βm (β‘π β π₯))) |
22 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β (Baseβπ
) β V) |
23 | 13 | cnvex 7913 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ β‘π β V |
24 | 23 | imaex 7904 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β‘π β π₯) β V |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β (β‘π β π₯) β V) |
26 | 22, 25 | elmapd 8831 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β (π β ((Baseβπ
) βm (β‘π β π₯)) β π:(β‘π β π₯)βΆ(Baseβπ
))) |
27 | 21, 26 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β π:(β‘π β π₯)βΆ(Baseβπ
)) |
28 | 27 | fdmd 6726 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β dom π = (β‘π β π₯)) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β dom π = (β‘π β π₯)) |
30 | 20, 29 | sseqtrd 4022 |
. . . . . . . . . . . . . . 15
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β dom π β (β‘π β π₯)) |
31 | | funimass2 6629 |
. . . . . . . . . . . . . . 15
β’ ((Fun
π β§ dom π β (β‘π β π₯)) β (π β dom π) β π₯) |
32 | 19, 30, 31 | sylancr 588 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β dom π) β π₯) |
33 | 18, 32 | sstrd 3992 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β π₯) |
34 | 15, 33 | elpwd 4608 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β π« π₯) |
35 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β π finSupp (0gβπ
)) |
36 | 35 | fsuppimpd 9366 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β Fin) |
37 | | imafi 9172 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ (π supp (0gβπ
)) β Fin) β (π β (π supp (0gβπ
))) β Fin) |
38 | 19, 36, 37 | sylancr 588 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β Fin) |
39 | 34, 38 | elind 4194 |
. . . . . . . . . . 11
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
))) β (π« π₯ β© Fin)) |
40 | | inteq 4953 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β (π supp (0gβπ
))) β β©
π¦ = β© (π
β (π supp
(0gβπ
)))) |
41 | 40 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π¦ = (π β (π supp (0gβπ
))) β (β
= β© π¦
β β
= β© (π β (π supp (0gβπ
))))) |
42 | 41 | adantl 483 |
. . . . . . . . . . 11
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π¦ = (π β (π supp (0gβπ
)))) β (β
= β© π¦
β β
= β© (π β (π supp (0gβπ
))))) |
43 | 16, 29 | sseqtrid 4034 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β (β‘π β π₯)) |
44 | | cnvimass 6078 |
. . . . . . . . . . . . . 14
β’ (β‘π β π₯) β dom π |
45 | 43, 44 | sstrdi 3994 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β dom π) |
46 | | intimafv 31920 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ (π supp (0gβπ
)) β dom π) β β© (π β (π supp (0gβπ
))) = β©
π β (π supp (0gβπ
))(πβπ)) |
47 | 19, 45, 46 | sylancr 588 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β β© (π β (π supp (0gβπ
))) = β©
π β (π supp (0gβπ
))(πβπ)) |
48 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π
β
CRing) |
49 | 48 | crngringd 20063 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π
β
Ring) |
50 | 49 | ad4antr 731 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β π
β Ring) |
51 | | fvex 6902 |
. . . . . . . . . . . . . . . 16
β’
(PrmIdealβπ
)
β V |
52 | 51 | rabex 5332 |
. . . . . . . . . . . . . . 15
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
53 | 52, 10 | dmmpti 6692 |
. . . . . . . . . . . . . 14
β’ dom π = (LIdealβπ
) |
54 | 45, 53 | sseqtrdi 4032 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β (LIdealβπ
)) |
55 | | simp-7r 789 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (β―β(Baseβπ
)) β 1) |
56 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β
(1rβπ
) =
(π
Ξ£g π)) |
57 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’
(0gβπ
) = (0gβπ
) |
58 | | ringcmn 20093 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π
β Ring β π
β CMnd) |
59 | 1, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β CRing β π
β CMnd) |
60 | 59 | ad8antr 739 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β π
β CMnd) |
61 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (β‘π β π₯) β V) |
62 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β π:(β‘π β π₯)βΆ(Baseβπ
)) |
63 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (π supp (0gβπ
)) = β
) |
64 | | ssidd 4005 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β β
β
β
) |
65 | 63, 64 | eqsstrd 4020 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (π supp (0gβπ
)) β β
) |
66 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β π finSupp (0gβπ
)) |
67 | 4, 57, 60, 61, 62, 65, 66 | gsumres 19776 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (π
Ξ£g (π βΎ β
)) = (π
Ξ£g
π)) |
68 | | res0 5984 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π βΎ β
) =
β
|
69 | 68 | oveq2i 7417 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
Ξ£g
(π βΎ β
)) =
(π
Ξ£g β
) |
70 | 57 | gsum0 18600 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
Ξ£g
β
) = (0gβπ
) |
71 | 69, 70 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
Ξ£g
(π βΎ β
)) =
(0gβπ
) |
72 | 67, 71 | eqtr3di 2788 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (π
Ξ£g π) = (0gβπ
)) |
73 | 56, 72 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . 17
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β
(0gβπ
) =
(1rβπ
)) |
74 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(1rβπ
) = (1rβπ
) |
75 | 4, 57, 74 | 01eq0ring 20298 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§
(0gβπ
) =
(1rβπ
))
β (Baseβπ
) =
{(0gβπ
)}) |
76 | 50, 73, 75 | syl2an2r 684 |
. . . . . . . . . . . . . . . 16
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β (Baseβπ
) = {(0gβπ
)}) |
77 | 76 | fveq2d 6893 |
. . . . . . . . . . . . . . 15
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β
(β―β(Baseβπ
)) =
(β―β{(0gβπ
)})) |
78 | | fvex 6902 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) β V |
79 | | hashsng 14326 |
. . . . . . . . . . . . . . . 16
β’
((0gβπ
) β V β
(β―β{(0gβπ
)}) = 1) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(β―β{(0gβπ
)}) = 1 |
81 | 77, 80 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ (π supp (0gβπ
)) = β
) β
(β―β(Baseβπ
)) = 1) |
82 | 55, 81 | mteqand 3034 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β β
) |
83 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(RSpanβπ
) =
(RSpanβπ
) |
84 | 10, 83 | zarclsiin 32840 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (π supp (0gβπ
)) β (LIdealβπ
) β§ (π supp (0gβπ
)) β β
) β β© π β (π supp (0gβπ
))(πβπ) = (πβ((RSpanβπ
)ββͺ (π supp (0gβπ
))))) |
85 | 50, 54, 82, 84 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β β©
π β (π supp (0gβπ
))(πβπ) = (πβ((RSpanβπ
)ββͺ (π supp (0gβπ
))))) |
86 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) |
87 | | nfra1 3282 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²πβπ β (β‘π β π₯)(πβπ) β π |
88 | 86, 87 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) |
89 | 54 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β π β (LIdealβπ
)) |
90 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(LIdealβπ
) =
(LIdealβπ
) |
91 | 4, 90 | lidlss 20826 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β π β (Baseβπ
)) |
93 | 92 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π β (π supp (0gβπ
)) β π β (Baseβπ
))) |
94 | 88, 93 | ralrimi 3255 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β βπ β (π supp (0gβπ
))π β (Baseβπ
)) |
95 | | unissb 4943 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ (π
supp (0gβπ
)) β (Baseβπ
) β βπ β (π supp (0gβπ
))π β (Baseβπ
)) |
96 | 94, 95 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β βͺ (π supp (0gβπ
)) β (Baseβπ
)) |
97 | 83, 4, 90 | rspcl 20840 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§ βͺ (π
supp (0gβπ
)) β (Baseβπ
)) β ((RSpanβπ
)ββͺ (π supp (0gβπ
))) β (LIdealβπ
)) |
98 | 50, 96, 97 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((RSpanβπ
)ββͺ (π supp (0gβπ
))) β (LIdealβπ
)) |
99 | 4, 90 | lidlss 20826 |
. . . . . . . . . . . . . . . 16
β’
(((RSpanβπ
)ββͺ (π supp (0gβπ
))) β (LIdealβπ
) β ((RSpanβπ
)ββͺ (π
supp (0gβπ
))) β (Baseβπ
)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((RSpanβπ
)ββͺ (π supp (0gβπ
))) β (Baseβπ
)) |
101 | 83, 4, 74 | rsp1 20842 |
. . . . . . . . . . . . . . . . 17
β’ (π
β Ring β
((RSpanβπ
)β{(1rβπ
)}) = (Baseβπ
)) |
102 | 50, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((RSpanβπ
)β{(1rβπ
)}) = (Baseβπ
)) |
103 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β π:(β‘π β π₯)βΆ(Baseβπ
)) |
104 | 103, 43 | fssresd 6756 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π βΎ (π supp (0gβπ
))):(π supp (0gβπ
))βΆ(Baseβπ
)) |
105 | | fvex 6902 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(Baseβπ
)
β V |
106 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π supp (0gβπ
)) β V |
107 | 105, 106 | elmap 8862 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΎ (π supp (0gβπ
))) β ((Baseβπ
) βm (π supp (0gβπ
))) β (π βΎ (π supp (0gβπ
))):(π supp (0gβπ
))βΆ(Baseβπ
)) |
108 | 104, 107 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π βΎ (π supp (0gβπ
))) β ((Baseβπ
) βm (π supp (0gβπ
)))) |
109 | | breq1 5151 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βΎ (π supp (0gβπ
))) β (π finSupp (0gβπ
) β (π βΎ (π supp (0gβπ
))) finSupp (0gβπ
))) |
110 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π βΎ (π supp (0gβπ
))) β (π
Ξ£g π) = (π
Ξ£g (π βΎ (π supp (0gβπ
))))) |
111 | 110 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βΎ (π supp (0gβπ
))) β ((1rβπ
) = (π
Ξ£g π) β
(1rβπ
) =
(π
Ξ£g (π βΎ (π supp (0gβπ
)))))) |
112 | | fveq1 6888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π βΎ (π supp (0gβπ
))) β (πβπ) = ((π βΎ (π supp (0gβπ
)))βπ)) |
113 | 112 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π βΎ (π supp (0gβπ
))) β ((πβπ) β π β ((π βΎ (π supp (0gβπ
)))βπ) β π)) |
114 | 113 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βΎ (π supp (0gβπ
))) β (βπ β (π supp (0gβπ
))(πβπ) β π β βπ β (π supp (0gβπ
))((π βΎ (π supp (0gβπ
)))βπ) β π)) |
115 | 109, 111,
114 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π βΎ (π supp (0gβπ
))) β ((π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (π supp (0gβπ
))(πβπ) β π) β ((π βΎ (π supp (0gβπ
))) finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g (π βΎ (π supp (0gβπ
)))) β§ βπ β (π supp (0gβπ
))((π βΎ (π supp (0gβπ
)))βπ) β π))) |
116 | 115 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π = (π βΎ (π supp (0gβπ
)))) β ((π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (π supp (0gβπ
))(πβπ) β π) β ((π βΎ (π supp (0gβπ
))) finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g (π βΎ (π supp (0gβπ
)))) β§ βπ β (π supp (0gβπ
))((π βΎ (π supp (0gβπ
)))βπ) β π))) |
117 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (0gβπ
) β V) |
118 | 35, 117 | fsuppres 9385 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π βΎ (π supp (0gβπ
))) finSupp (0gβπ
)) |
119 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (1rβπ
) = (π
Ξ£g π)) |
120 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β π
β CMnd) |
121 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (β‘π β π₯) β V) |
122 | | ssidd 4005 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π supp (0gβπ
)) β (π supp (0gβπ
))) |
123 | 4, 57, 120, 121, 103, 122, 35 | gsumres 19776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (π
Ξ£g (π βΎ (π supp (0gβπ
)))) = (π
Ξ£g π)) |
124 | 119, 123 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (1rβπ
) = (π
Ξ£g (π βΎ (π supp (0gβπ
))))) |
125 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β π β (π supp (0gβπ
))) |
126 | 125 | fvresd 6909 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β ((π βΎ (π supp (0gβπ
)))βπ) = (πβπ)) |
127 | 16, 28 | sseqtrid 4034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β (π supp (0gβπ
)) β (β‘π β π₯)) |
128 | 127 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ π β (π supp (0gβπ
))) β π β (β‘π β π₯)) |
129 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β (πβπ) = (πβπ)) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β π = π) |
131 | 129, 130 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ π β (π supp (0gβπ
))) β§ π = π) β ((πβπ) β π β (πβπ) β π)) |
133 | 128, 132 | rspcdv 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ π β (π supp (0gβπ
))) β (βπ β (β‘π β π₯)(πβπ) β π β (πβπ) β π)) |
134 | 133 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ π β (π supp (0gβπ
))) β§ βπ β (β‘π β π₯)(πβπ) β π) β (πβπ) β π) |
135 | 134 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β (πβπ) β π) |
136 | 126, 135 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β§ π β (π supp (0gβπ
))) β ((π βΎ (π supp (0gβπ
)))βπ) β π) |
137 | 136 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β βπ β (π supp (0gβπ
))((π βΎ (π supp (0gβπ
)))βπ) β π) |
138 | 118, 124,
137 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((π βΎ (π supp (0gβπ
))) finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g (π βΎ (π supp (0gβπ
)))) β§ βπ β (π supp (0gβπ
))((π βΎ (π supp (0gβπ
)))βπ) β π)) |
139 | 108, 116,
138 | rspcedvd 3615 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β βπ β ((Baseβπ
) βm (π supp (0gβπ
)))(π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (π supp (0gβπ
))(πβπ) β π)) |
140 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’
(.rβπ
) = (.rβπ
) |
141 | 83, 4, 57, 140, 50, 54 | elrspunidl 32535 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((1rβπ
) β ((RSpanβπ
)ββͺ (π
supp (0gβπ
))) β βπ β ((Baseβπ
) βm (π supp (0gβπ
)))(π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (π supp (0gβπ
))(πβπ) β π))) |
142 | 139, 141 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (1rβπ
) β ((RSpanβπ
)ββͺ (π
supp (0gβπ
)))) |
143 | 142 | snssd 4812 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β {(1rβπ
)} β ((RSpanβπ
)ββͺ (π
supp (0gβπ
)))) |
144 | 83, 90 | rspssp 20844 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§
((RSpanβπ
)ββͺ (π supp (0gβπ
))) β (LIdealβπ
) β§
{(1rβπ
)}
β ((RSpanβπ
)ββͺ (π supp (0gβπ
)))) β ((RSpanβπ
)β{(1rβπ
)}) β ((RSpanβπ
)ββͺ (π
supp (0gβπ
)))) |
145 | 50, 98, 143, 144 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((RSpanβπ
)β{(1rβπ
)}) β ((RSpanβπ
)ββͺ (π
supp (0gβπ
)))) |
146 | 102, 145 | eqsstrrd 4021 |
. . . . . . . . . . . . . . 15
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (Baseβπ
) β ((RSpanβπ
)ββͺ (π supp (0gβπ
)))) |
147 | 100, 146 | eqssd 3999 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β ((RSpanβπ
)ββͺ (π supp (0gβπ
))) = (Baseβπ
)) |
148 | 147 | fveq2d 6893 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (πβ((RSpanβπ
)ββͺ (π supp (0gβπ
)))) = (πβ(Baseβπ
))) |
149 | 90, 4 | lidl1 20838 |
. . . . . . . . . . . . . . . . 17
β’ (π
β Ring β
(Baseβπ
) β
(LIdealβπ
)) |
150 | 1, 149 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π
β CRing β
(Baseβπ
) β
(LIdealβπ
)) |
151 | 10, 4 | zarcls1 32838 |
. . . . . . . . . . . . . . . 16
β’ ((π
β CRing β§
(Baseβπ
) β
(LIdealβπ
)) β
((πβ(Baseβπ
)) = β
β
(Baseβπ
) =
(Baseβπ
))) |
152 | 150, 151 | mpdan 686 |
. . . . . . . . . . . . . . 15
β’ (π
β CRing β ((πβ(Baseβπ
)) = β
β
(Baseβπ
) =
(Baseβπ
))) |
153 | 4, 152 | mpbiri 258 |
. . . . . . . . . . . . . 14
β’ (π
β CRing β (πβ(Baseβπ
)) = β
) |
154 | 153 | ad7antr 737 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (πβ(Baseβπ
)) = β
) |
155 | 148, 154 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β (πβ((RSpanβπ
)ββͺ (π supp (0gβπ
)))) = β
) |
156 | 47, 85, 155 | 3eqtrrd 2778 |
. . . . . . . . . . 11
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β β
= β© (π
β (π supp
(0gβπ
)))) |
157 | 39, 42, 156 | rspcedvd 3615 |
. . . . . . . . . 10
β’
((((((((π
β
CRing β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ π finSupp (0gβπ
)) β§
(1rβπ
) =
(π
Ξ£g π)) β§ βπ β (β‘π β π₯)(πβπ) β π) β βπ¦ β (π« π₯ β© Fin)β
= β© π¦) |
158 | 157 | exp41 436 |
. . . . . . . . 9
β’
(((((π
β CRing
β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β (π finSupp (0gβπ
) β
((1rβπ
) =
(π
Ξ£g π) β (βπ β (β‘π β π₯)(πβπ) β π β βπ¦ β (π« π₯ β© Fin)β
= β© π¦)))) |
159 | 158 | 3imp2 1350 |
. . . . . . . 8
β’
((((((π
β CRing
β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
((Baseβπ
)
βm (β‘π β π₯))) β§ (π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (β‘π β π₯)(πβπ) β π)) β βπ¦ β (π« π₯ β© Fin)β
= β© π¦) |
160 | 4, 74 | ringidcl 20077 |
. . . . . . . . . . 11
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
161 | 49, 160 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (1rβπ
) β (Baseβπ
)) |
162 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π₯ β
π« (Clsdβπ½)) |
163 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(PrmIdealβπ
) =
(PrmIdealβπ
) |
164 | 2, 3, 163, 10 | zartopn 32844 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β CRing β (π½ β
(TopOnβ(PrmIdealβπ
)) β§ ran π = (Clsdβπ½))) |
165 | 164 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ (π
β CRing β ran π = (Clsdβπ½)) |
166 | 48, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β ran π =
(Clsdβπ½)) |
167 | 166 | pweqd 4619 |
. . . . . . . . . . . . . . 15
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π« ran π = π« (Clsdβπ½)) |
168 | 162, 167 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π₯ β
π« ran π) |
169 | 168 | elpwid 4611 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π₯ β
ran π) |
170 | | intimafv 31920 |
. . . . . . . . . . . . . . 15
β’ ((Fun
π β§ (β‘π β π₯) β dom π) β β© (π β (β‘π β π₯)) = β©
π β (β‘π β π₯)(πβπ)) |
171 | 19, 44, 170 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ β© (π
β (β‘π β π₯)) = β©
π β (β‘π β π₯)(πβπ) |
172 | | funimacnv 6627 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
π β (π β (β‘π β π₯)) = (π₯ β© ran π)) |
173 | 19, 172 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (π β (β‘π β π₯)) = (π₯ β© ran π) |
174 | | df-ss 3965 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ran π β (π₯ β© ran π) = π₯) |
175 | 174 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ran π β (π₯ β© ran π) = π₯) |
176 | 173, 175 | eqtrid 2785 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ran π β (π β (β‘π β π₯)) = π₯) |
177 | 176 | inteqd 4955 |
. . . . . . . . . . . . . 14
β’ (π₯ β ran π β β© (π β (β‘π β π₯)) = β© π₯) |
178 | 171, 177 | eqtr3id 2787 |
. . . . . . . . . . . . 13
β’ (π₯ β ran π β β©
π β (β‘π β π₯)(πβπ) = β© π₯) |
179 | 169, 178 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β β© π β (β‘π β π₯)(πβπ) = β© π₯) |
180 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (β‘π β π₯) β dom π) |
181 | 180, 53 | sseqtrdi 4032 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (β‘π β π₯) β (LIdealβπ
)) |
182 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β Fun π) |
183 | | inteq 4953 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β
β β© π₯ =
β© β
) |
184 | | int0 4966 |
. . . . . . . . . . . . . . . . . 18
β’ β© β
= V |
185 | 183, 184 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β
β β© π₯ =
V) |
186 | | vn0 4338 |
. . . . . . . . . . . . . . . . . 18
β’ V β
β
|
187 | | neeq1 3004 |
. . . . . . . . . . . . . . . . . 18
β’ (β© π₯ =
V β (β© π₯ β β
β V β
β
)) |
188 | 186, 187 | mpbiri 258 |
. . . . . . . . . . . . . . . . 17
β’ (β© π₯ =
V β β© π₯ β β
) |
189 | 185, 188 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β
β β© π₯
β β
) |
190 | 189 | necon2i 2976 |
. . . . . . . . . . . . . . 15
β’ (β© π₯ =
β
β π₯ β
β
) |
191 | 190 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β π₯ β
β
) |
192 | | preiman0 31919 |
. . . . . . . . . . . . . 14
β’ ((Fun
π β§ π₯ β ran π β§ π₯ β β
) β (β‘π β π₯) β β
) |
193 | 182, 169,
191, 192 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (β‘π β π₯) β β
) |
194 | 10, 83 | zarclsiin 32840 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (β‘π β π₯) β (LIdealβπ
) β§ (β‘π β π₯) β β
) β β© π β (β‘π β π₯)(πβπ) = (πβ((RSpanβπ
)ββͺ (β‘π β π₯)))) |
195 | 49, 181, 193, 194 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β β© π β (β‘π β π₯)(πβπ) = (πβ((RSpanβπ
)ββͺ (β‘π β π₯)))) |
196 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β β© π₯ = β
) |
197 | 179, 195,
196 | 3eqtr3d 2781 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (πβ((RSpanβπ
)ββͺ (β‘π β π₯))) = β
) |
198 | 181 | sselda 3982 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
(β‘π β π₯)) β π β (LIdealβπ
)) |
199 | 198, 91 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ (β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β§ π β
(β‘π β π₯)) β π β (Baseβπ
)) |
200 | 199 | ralrimiva 3147 |
. . . . . . . . . . . . . 14
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β βπ
β (β‘π β π₯)π β (Baseβπ
)) |
201 | | unissb 4943 |
. . . . . . . . . . . . . 14
β’ (βͺ (β‘π β π₯) β (Baseβπ
) β βπ β (β‘π β π₯)π β (Baseβπ
)) |
202 | 200, 201 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β βͺ (β‘π β π₯) β (Baseβπ
)) |
203 | 83, 4, 90 | rspcl 20840 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ βͺ (β‘π β π₯) β (Baseβπ
)) β ((RSpanβπ
)ββͺ (β‘π β π₯)) β (LIdealβπ
)) |
204 | 49, 202, 203 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β ((RSpanβπ
)ββͺ (β‘π β π₯)) β (LIdealβπ
)) |
205 | 10, 4 | zarcls1 32838 |
. . . . . . . . . . . 12
β’ ((π
β CRing β§
((RSpanβπ
)ββͺ (β‘π β π₯)) β (LIdealβπ
)) β ((πβ((RSpanβπ
)ββͺ (β‘π β π₯))) = β
β ((RSpanβπ
)ββͺ (β‘π β π₯)) = (Baseβπ
))) |
206 | 48, 204, 205 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β ((πβ((RSpanβπ
)ββͺ (β‘π β π₯))) = β
β ((RSpanβπ
)ββͺ (β‘π β π₯)) = (Baseβπ
))) |
207 | 197, 206 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β ((RSpanβπ
)ββͺ (β‘π β π₯)) = (Baseβπ
)) |
208 | 161, 207 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β (1rβπ
) β ((RSpanβπ
)ββͺ (β‘π β π₯))) |
209 | 83, 4, 57, 140, 49, 181 | elrspunidl 32535 |
. . . . . . . . 9
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β ((1rβπ
) β ((RSpanβπ
)ββͺ (β‘π β π₯)) β βπ β ((Baseβπ
) βm (β‘π β π₯))(π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (β‘π β π₯)(πβπ) β π))) |
210 | 208, 209 | mpbid 231 |
. . . . . . . 8
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β βπ
β ((Baseβπ
)
βm (β‘π β π₯))(π finSupp (0gβπ
) β§
(1rβπ
) =
(π
Ξ£g π) β§ βπ β (β‘π β π₯)(πβπ) β π)) |
211 | 159, 210 | r19.29a 3163 |
. . . . . . 7
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β βπ¦
β (π« π₯ β©
Fin)β
= β© π¦) |
212 | | 0ex 5307 |
. . . . . . . 8
β’ β
β V |
213 | | vex 3479 |
. . . . . . . 8
β’ π₯ β V |
214 | | elfi 9405 |
. . . . . . . 8
β’ ((β
β V β§ π₯ β V)
β (β
β (fiβπ₯) β βπ¦ β (π« π₯ β© Fin)β
= β© π¦)) |
215 | 212, 213,
214 | mp2an 691 |
. . . . . . 7
β’ (β
β (fiβπ₯) β
βπ¦ β (π«
π₯ β© Fin)β
= β© π¦) |
216 | 211, 215 | sylibr 233 |
. . . . . 6
β’ ((((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β§ β© π₯ =
β
) β β
β (fiβπ₯)) |
217 | 216 | ex 414 |
. . . . 5
β’ (((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β (β© π₯ =
β
β β
β (fiβπ₯))) |
218 | 217 | necon3bd 2955 |
. . . 4
β’ (((π
β CRing β§
(β―β(Baseβπ
)) β 1) β§ π₯ β π« (Clsdβπ½)) β (Β¬ β
β
(fiβπ₯) β β© π₯
β β
)) |
219 | 218 | ralrimiva 3147 |
. . 3
β’ ((π
β CRing β§
(β―β(Baseβπ
)) β 1) β βπ₯ β π« (Clsdβπ½)(Β¬ β
β
(fiβπ₯) β β© π₯
β β
)) |
220 | | cmpfi 22904 |
. . . 4
β’ (π½ β Top β (π½ β Comp β
βπ₯ β π«
(Clsdβπ½)(Β¬
β
β (fiβπ₯)
β β© π₯ β β
))) |
221 | 220 | biimpar 479 |
. . 3
β’ ((π½ β Top β§ βπ₯ β π«
(Clsdβπ½)(Β¬
β
β (fiβπ₯)
β β© π₯ β β
)) β π½ β Comp) |
222 | 9, 219, 221 | syl2an2r 684 |
. 2
β’ ((π
β CRing β§
(β―β(Baseβπ
)) β 1) β π½ β Comp) |
223 | 8, 222 | pm2.61dane 3030 |
1
β’ (π
β CRing β π½ β Comp) |