Theorem zartopn

Description: The Zariski topology is a topology, and its closed sets are images by V of the ideals of R . (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
	zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
	zarcls.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
	zarcls.2	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
Assertion	zartopn	⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ 𝑃 ) ∧ ran 𝑉 = ( Clsd ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3		zarcls.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
4		zarcls.2	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
5		ssrab2	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ⊆ 𝑃
6	3	fvexi	⊢ 𝑃 ∈ V
7	6	elpw2	⊢ ( { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃 ↔ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ⊆ 𝑃 )
8	5 7	mpbir	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃
9	8	rgenw	⊢ ∀ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃
10	4	rnmptss	⊢ ( ∀ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃 → ran 𝑉 ⊆ 𝒫 𝑃 )
11	9 10	ax-mp	⊢ ran 𝑉 ⊆ 𝒫 𝑃
12	11	a1i	⊢ ( 𝑅 ∈ CRing → ran 𝑉 ⊆ 𝒫 𝑃 )
13		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14	3	rabeqi	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 }
15	14	mpteq2i	⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
16	4 15	eqtri	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18	16 3 17	zarcls0	⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ { ( 0g ‘ 𝑅 ) } ) = 𝑃 )
19	4	funmpt2	⊢ Fun 𝑉
20		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
21	20 17	lidl0	⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
22	6	rabex	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ V
23	22 4	dmmpti	⊢ dom 𝑉 = ( LIdeal ‘ 𝑅 )
24	21 23	eleqtrrdi	⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ dom 𝑉 )
25		fvelrn	⊢ ( ( Fun 𝑉 ∧ { ( 0g ‘ 𝑅 ) } ∈ dom 𝑉 ) → ( 𝑉 ‘ { ( 0g ‘ 𝑅 ) } ) ∈ ran 𝑉 )
26	19 24 25	sylancr	⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ { ( 0g ‘ 𝑅 ) } ) ∈ ran 𝑉 )
27	18 26	eqeltrrd	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ ran 𝑉 )
28	13 27	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ ran 𝑉 )
29	16	zarclsint	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑧 ⊆ ran 𝑉 ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ∈ ran 𝑉 )
30	12 28 29	ismred	⊢ ( 𝑅 ∈ CRing → ran 𝑉 ∈ ( Moore ‘ 𝑃 ) )
31		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32	23 31	lidl1	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ dom 𝑉 )
33	13 32	syl	⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) ∈ dom 𝑉 )
34	33 23	eleqtrdi	⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) )
35	16 31	zarcls1	⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ ↔ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) )
36	31 35	mpbiri	⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ )
37	34 36	mpdan	⊢ ( 𝑅 ∈ CRing → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ )
38	19	a1i	⊢ ( 𝑅 ∈ CRing → Fun 𝑉 )
39		fvelrn	⊢ ( ( Fun 𝑉 ∧ ( Base ‘ 𝑅 ) ∈ dom 𝑉 ) → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) ∈ ran 𝑉 )
40	38 33 39	syl2anc	⊢ ( 𝑅 ∈ CRing → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) ∈ ran 𝑉 )
41	37 40	eqeltrrd	⊢ ( 𝑅 ∈ CRing → ∅ ∈ ran 𝑉 )
42	16	zarclsun	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ran 𝑉 ∧ 𝑦 ∈ ran 𝑉 ) → ( 𝑥 ∪ 𝑦 ) ∈ ran 𝑉 )
43		eqid	⊢ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 }
44	30 41 42 43	mretopd	⊢ ( 𝑅 ∈ CRing → ( { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ∈ ( TopOn ‘ 𝑃 ) ∧ ran 𝑉 = ( Clsd ‘ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ) ) )
45	1 2 3 4	zarcls	⊢ ( 𝑅 ∈ Ring → 𝐽 = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } )
46	13 45	syl	⊢ ( 𝑅 ∈ CRing → 𝐽 = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } )
47	46	eleq1d	⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ 𝑃 ) ↔ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ∈ ( TopOn ‘ 𝑃 ) ) )
48	46	fveq2d	⊢ ( 𝑅 ∈ CRing → ( Clsd ‘ 𝐽 ) = ( Clsd ‘ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ) )
49	48	eqeq2d	⊢ ( 𝑅 ∈ CRing → ( ran 𝑉 = ( Clsd ‘ 𝐽 ) ↔ ran 𝑉 = ( Clsd ‘ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ) ) )
50	47 49	anbi12d	⊢ ( 𝑅 ∈ CRing → ( ( 𝐽 ∈ ( TopOn ‘ 𝑃 ) ∧ ran 𝑉 = ( Clsd ‘ 𝐽 ) ) ↔ ( { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ∈ ( TopOn ‘ 𝑃 ) ∧ ran 𝑉 = ( Clsd ‘ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ) ) ) )
51	44 50	mpbird	⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ 𝑃 ) ∧ ran 𝑉 = ( Clsd ‘ 𝐽 ) ) )