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	$$⊢S=\mathrm{Spec}\left(R\right)$$
Assertion	rspectps	$$⊢R\in \mathrm{CRing}\to S\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		rspectps.1	$$⊢S=\mathrm{Spec}\left(R\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left(S\right)=\mathrm{TopOpen}\left(S\right)$$
3		eqid	$$⊢\mathrm{PrmIdeal}\left(R\right)=\mathrm{PrmIdeal}\left(R\right)$$
4	1 2 3	zartopon	$$⊢R\in \mathrm{CRing}\to \mathrm{TopOpen}\left(S\right)\in \mathrm{TopOn}\left(\mathrm{PrmIdeal}\left(R\right)\right)$$
5		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
6	1	rspecbas	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)={\mathrm{Base}}_S$$
7	6	fveq2d	$$⊢R\in \mathrm{Ring}\to \mathrm{TopOn}\left(\mathrm{PrmIdeal}\left(R\right)\right)=\mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
8	5 7	syl	$$⊢R\in \mathrm{CRing}\to \mathrm{TopOn}\left(\mathrm{PrmIdeal}\left(R\right)\right)=\mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
9	4 8	eleqtrd	$$⊢R\in \mathrm{CRing}\to \mathrm{TopOpen}\left(S\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
10		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
11	10 2	istps	$$⊢S\in \mathrm{TopSp}\leftrightarrow \mathrm{TopOpen}\left(S\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
12	9 11	sylibr	$$⊢R\in \mathrm{CRing}\to S\in \mathrm{TopSp}$$