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	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		cidlsrg	Could not format IDLsrg : No typesetting found for class IDLsrg with typecode class
4	1	cv	$$setvarr$$
5	4 3	cfv	Could not format ( IDLsrg ` r ) : No typesetting found for class ( IDLsrg ` r ) with typecode class
6		cress	$$class{\upharpoonright }_{𝑠}$$
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