Metamath Proof Explorer

Theorem rspecval

Description: Value of the spectrum of the ring R . Notation 1.1.1 of EGA p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024)

Ref Expression
Assertion rspecval 
|- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( r = R -> ( IDLsrg ` r ) = ( IDLsrg ` R ) )
2 fveq2 
 |-  ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) )
3 1 2 oveq12d 
 |-  ( r = R -> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
4 df-rspec 
 |-  Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) )
5 ovex 
 |-  ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) e. _V
6 3 4 5 fvmpt 
 |-  ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )