Definition df-rspec

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

	Ref	Expression
Assertion	df-rspec	$$⊢\mathrm{Spec}=\left(r\in \mathrm{Ring}⟼\mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crspec	$$class\mathrm{Spec}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		cidlsrg	$$class\mathrm{IDLsrg}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class\mathrm{IDLsrg}\left(r\right)$$
6		cress	$$class{\upharpoonright }_{𝑠}$$
7		cprmidl	$$class\mathrm{PrmIdeal}$$
8	4 7	cfv	$$class\mathrm{PrmIdeal}\left(r\right)$$
9	5 8 6	co	$$class\left(\mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)\right)$$
10	1 2 9	cmpt	$$class\left(r\in \mathrm{Ring}⟼\mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)\right)$$
11	0 10	wceq	$$wff\mathrm{Spec}=\left(r\in \mathrm{Ring}⟼\mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)\right)$$