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	No typesetting found for |- S = ( Spec ` R ) with typecode |-
Assertion	rspectps	$$⊢R\in \mathrm{CRing}\to S\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		rspectps.1	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2		eqid	$$⊢\mathrm{TopOpen}\left(S\right)=\mathrm{TopOpen}\left(S\right)$$
3		eqid	Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
4	1 2 3	zartopon	Could not format ( R e. CRing -> ( TopOpen ` S ) e. ( TopOn ` ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. CRing -> ( TopOpen ` S ) e. ( TopOn ` ( PrmIdeal ` R ) ) ) with typecode |-
5		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
6	1	rspecbas	Could not format ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) ) with typecode |-
7	6	fveq2d	Could not format ( R e. Ring -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) ) : No typesetting found for |- ( R e. Ring -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) ) with typecode |-
8	5 7	syl	Could not format ( R e. CRing -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) ) : No typesetting found for |- ( R e. CRing -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) ) with typecode |-
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}$$