Definition df-rspec

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

	Ref	Expression
Assertion	df-rspec	⊢ Spec = ( 𝑟 ∈ Ring ↦ ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crspec	⊢ Spec
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		cidlsrg	⊢ IDLsrg
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( IDLsrg ‘ 𝑟 )
6		cress	⊢ ↾s
7		cprmidl	⊢ PrmIdeal
8	4 7	cfv	⊢ ( PrmIdeal ‘ 𝑟 )
9	5 8 6	co	⊢ ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) )
10	1 2 9	cmpt	⊢ ( 𝑟 ∈ Ring ↦ ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) ) )
11	0 10	wceq	⊢ Spec = ( 𝑟 ∈ Ring ↦ ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) ) )