Theorem rspectps

Description: The spectrum of a ring R is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypothesis	rspectps.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
Assertion	rspectps	⊢ ( 𝑅 ∈ CRing → 𝑆 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		rspectps.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		eqid	⊢ ( TopOpen ‘ 𝑆 ) = ( TopOpen ‘ 𝑆 )
3		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
4	1 2 3	zartopon	⊢ ( 𝑅 ∈ CRing → ( TopOpen ‘ 𝑆 ) ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) )
5		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6	1	rspecbas	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
7	6	fveq2d	⊢ ( 𝑅 ∈ Ring → ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) = ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
8	5 7	syl	⊢ ( 𝑅 ∈ CRing → ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) = ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
9	4 8	eleqtrd	⊢ ( 𝑅 ∈ CRing → ( TopOpen ‘ 𝑆 ) ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11	10 2	istps	⊢ ( 𝑆 ∈ TopSp ↔ ( TopOpen ‘ 𝑆 ) ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
12	9 11	sylibr	⊢ ( 𝑅 ∈ CRing → 𝑆 ∈ TopSp )