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 Could not format assertion : No typesetting found for |- Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 crspec Could not format Spec : No typesetting found for class Spec with typecode class
1 vr setvar r
2 crg class Ring
3 cidlsrg Could not format IDLsrg : No typesetting found for class IDLsrg with typecode class
4 1 cv setvar r
5 4 3 cfv Could not format ( IDLsrg ` r ) : No typesetting found for class ( IDLsrg ` r ) with typecode class
6 cress class 𝑠
7 cprmidl Could not format PrmIdeal : No typesetting found for class PrmIdeal with typecode class
8 4 7 cfv Could not format ( PrmIdeal ` r ) : No typesetting found for class ( PrmIdeal ` r ) with typecode class
9 5 8 6 co Could not format ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) : No typesetting found for class ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) with typecode class
10 1 2 9 cmpt Could not format ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) : No typesetting found for class ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) with typecode class
11 0 10 wceq Could not format Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) : No typesetting found for wff Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) with typecode wff