Metamath Proof Explorer

Theorem rspecbas

Description: The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024)

Ref Expression
Hypothesis rspecbas.1 
|- S = ( Spec ` R )
Assertion rspecbas 
|- ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) )

Proof

Step Hyp Ref Expression
1 rspecbas.1 
 |-  S = ( Spec ` R )
2 prmidlssidl 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
3 eqid 
 |-  ( IDLsrg ` R ) = ( IDLsrg ` R )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 3 4 idlsrgbas 
 |-  ( R e. Ring -> ( LIdeal ` R ) = ( Base ` ( IDLsrg ` R ) ) )
6 2 5 sseqtrd 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) )
7 eqid 
 |-  ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) )
8 eqid 
 |-  ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) )
9 7 8 ressbas2 
 |-  ( ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) )
10 6 9 syl 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) )
11 rspecval 
 |-  ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
12 1 11 syl5eq 
 |-  ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
13 12 fveq2d 
 |-  ( R e. Ring -> ( Base ` S ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) )
14 10 13 eqtr4d 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) )