Metamath Proof Explorer

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 = ( Spec ` R )
Assertion rspectps 
|- ( R e. CRing -> S e. TopSp )

Proof

Step Hyp Ref Expression
1 rspectps.1 
 |-  S = ( Spec ` R )
2 eqid 
 |-  ( TopOpen ` S ) = ( TopOpen ` S )
3 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
4 1 2 3 zartopon 
 |-  ( R e. CRing -> ( TopOpen ` S ) e. ( TopOn ` ( PrmIdeal ` R ) ) )
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 1 rspecbas 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) )
7 6 fveq2d 
 |-  ( R e. Ring -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) )
8 5 7 syl 
 |-  ( R e. CRing -> ( TopOn ` ( PrmIdeal ` R ) ) = ( TopOn ` ( Base ` S ) ) )
9 4 8 eleqtrd 
 |-  ( R e. CRing -> ( TopOpen ` S ) e. ( TopOn ` ( Base ` S ) ) )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 10 2 istps 
 |-  ( S e. TopSp <-> ( TopOpen ` S ) e. ( TopOn ` ( Base ` S ) ) )
12 9 11 sylibr 
 |-  ( R e. CRing -> S e. TopSp )