Theorem zarcls0

Description: The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
	zarcls0.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
	zarcls0.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	zarcls0	⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ { 0 } ) = 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
2		zarcls0.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
3		zarcls0.2	⊢ 0 = ( 0g ‘ 𝑅 )
4	1	a1i	⊢ ( 𝑅 ∈ Ring → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
5		simplr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 = { 0 } )
6		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
7		prmidlidl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
8	6 7	sylancom	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
9		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
10	9 3	lidl0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑗 )
11	6 8 10	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑗 )
12	11	snssd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 0 } ⊆ 𝑗 )
13	5 12	eqsstrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ⊆ 𝑗 )
14	13	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) → ∀ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) 𝑖 ⊆ 𝑗 )
15		rabid2	⊢ ( ( PrmIdeal ‘ 𝑅 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ↔ ∀ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) 𝑖 ⊆ 𝑗 )
16	14 15	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) → ( PrmIdeal ‘ 𝑅 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
17	2 16	eqtr2id	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 = { 0 } ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = 𝑃 )
18	9 3	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
19	2	fvexi	⊢ 𝑃 ∈ V
20	19	a1i	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ V )
21	4 17 18 20	fvmptd	⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ { 0 } ) = 𝑃 )