Metamath Proof Explorer

Definition df-rspec

Description: Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Assertion df-rspec 
|- Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crspec 
 |-  Spec
1 vr 
 |-  r
2 crg 
 |-  Ring
3 cidlsrg 
 |-  IDLsrg
4 1 cv 
 |-  r
5 4 3 cfv 
 |-  ( IDLsrg ` r )
6 cress 
 |-  |`s
7 cprmidl 
 |-  PrmIdeal
8 4 7 cfv 
 |-  ( PrmIdeal ` r )
9 5 8 6 co 
 |-  ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) )
10 1 2 9 cmpt 
 |-  ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) )
11 0 10 wceq 
 |-  Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) )