Metamath Proof Explorer

Theorem zarmxt1

Description: The Zariski topology restricted to maximal ideals is T_1 . (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
zarmxt1.1 ⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
zarmxt1.2 ⊢ 𝑇 = ( 𝐽 ↾t 𝑀 )
Assertion zarmxt1 ( 𝑅 ∈ CRing → 𝑇 ∈ Fre )

Proof

Step Hyp Ref Expression
1 zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
2 zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3 zarmxt1.1 ⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
4 zarmxt1.2 ⊢ 𝑇 = ( 𝐽 ↾t 𝑀 )
5 1 2 zartop ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Top )
6 3 fvexi ⊢ 𝑀 ∈ V
7 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ V ) → ( 𝐽 ↾t 𝑀 ) ∈ Top )
8 4 7 eqeltrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ V ) → 𝑇 ∈ Top )
9 5 6 8 sylancl ⊢ ( 𝑅 ∈ CRing → 𝑇 ∈ Top )
10 eqid ⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
11 10 mxidlprm ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) )
12 11 ex ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
13 12 ssrdv ⊢ ( 𝑅 ∈ CRing → ( MaxIdeal ‘ 𝑅 ) ⊆ ( PrmIdeal ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → ( MaxIdeal ‘ 𝑅 ) ⊆ ( PrmIdeal ‘ 𝑅 ) )
15 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
16 14 3 15 3sstr4g ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑀 ⊆ ( PrmIdeal ‘ 𝑅 ) )
17 sseq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑖 ⊆ 𝑗 ↔ 𝑖 ⊆ 𝑙 ) )
18 17 cbvrabv ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑙 }
19 sseq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ⊆ 𝑙 ↔ 𝑘 ⊆ 𝑙 ) )
20 19 rabbidv ⊢ ( 𝑖 = 𝑘 → { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑙 } = { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } )
21 18 20 syl5eq ⊢ ( 𝑖 = 𝑘 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } )
22 21 cbvmptv ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } )
23 1 2 15 22 zartopn ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) ∧ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) ) )
24 23 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) ∧ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) ) )
25 24 simpld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) )
26 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) → ( PrmIdeal ‘ 𝑅 ) = ∪ 𝐽 )
27 25 26 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → ( PrmIdeal ‘ 𝑅 ) = ∪ 𝐽 )
28 16 27 sseqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑀 ⊆ ∪ 𝐽 )
29 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑅 ∈ CRing )
30 29 crngringd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑅 ∈ Ring )
31 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ ∪ 𝑇 )
32 4 unieqi ⊢ ∪ 𝑇 = ∪ ( 𝐽 ↾t 𝑀 )
33 31 32 eleqtrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ ∪ ( 𝐽 ↾t 𝑀 ) )
34 5 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝐽 ∈ Top )
35 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
36 35 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ⊆ ∪ 𝐽 ) → 𝑀 = ∪ ( 𝐽 ↾t 𝑀 ) )
37 34 28 36 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑀 = ∪ ( 𝐽 ↾t 𝑀 ) )
38 33 37 eleqtrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ 𝑀 )
39 38 3 eleqtrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
40 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
41 40 mxidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
42 30 39 41 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
43 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
44 22 43 zarclssn ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ) → ( { 𝑚 } = ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ‘ 𝑚 ) ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) )
45 44 biimpar ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → { 𝑚 } = ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ‘ 𝑚 ) )
46 29 42 39 45 syl21anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } = ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ‘ 𝑚 ) )
47 22 funmpt2 ⊢ Fun ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
48 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
49 48 rabex ⊢ { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } ∈ V
50 49 22 dmmpti ⊢ dom ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( LIdeal ‘ 𝑅 )
51 42 50 eleqtrrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → 𝑚 ∈ dom ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
52 fvelrn ⊢ ( ( Fun ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ∧ 𝑚 ∈ dom ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ) → ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ‘ 𝑚 ) ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
53 47 51 52 sylancr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ‘ 𝑚 ) ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
54 46 53 eqeltrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
55 24 simprd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) )
56 54 55 eleqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } ∈ ( Clsd ‘ 𝐽 ) )
57 38 snssd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } ⊆ 𝑀 )
58 35 restcldi ⊢ ( ( 𝑀 ⊆ ∪ 𝐽 ∧ { 𝑚 } ∈ ( Clsd ‘ 𝐽 ) ∧ { 𝑚 } ⊆ 𝑀 ) → { 𝑚 } ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑀 ) ) )
59 28 56 57 58 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑀 ) ) )
60 4 fveq2i ⊢ ( Clsd ‘ 𝑇 ) = ( Clsd ‘ ( 𝐽 ↾t 𝑀 ) )
61 59 60 eleqtrrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇 ) → { 𝑚 } ∈ ( Clsd ‘ 𝑇 ) )
62 61 ralrimiva ⊢ ( 𝑅 ∈ CRing → ∀ 𝑚 ∈ ∪ 𝑇 { 𝑚 } ∈ ( Clsd ‘ 𝑇 ) )
63 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
64 63 ist1 ⊢ ( 𝑇 ∈ Fre ↔ ( 𝑇 ∈ Top ∧ ∀ 𝑚 ∈ ∪ 𝑇 { 𝑚 } ∈ ( Clsd ‘ 𝑇 ) ) )
65 9 62 64 sylanbrc ⊢ ( 𝑅 ∈ CRing → 𝑇 ∈ Fre )