Theorem rspecval

Description: Value of the spectrum of the ring R . Notation 1.1.1 of EGA p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024)

	Ref	Expression
Assertion	rspecval	$$⊢R\in \mathrm{Ring}\to \mathrm{Spec}\left(R\right)=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢r=R\to \mathrm{IDLsrg}\left(r\right)=\mathrm{IDLsrg}\left(R\right)$$
2		fveq2	$$⊢r=R\to \mathrm{PrmIdeal}\left(r\right)=\mathrm{PrmIdeal}\left(R\right)$$
3	1 2	oveq12d	$$⊢r=R\to \mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$
4		df-rspec	$$⊢\mathrm{Spec}=\left(r\in \mathrm{Ring}⟼\mathrm{IDLsrg}\left(r\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(r\right)\right)$$
5		ovex	$$⊢\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢R\in \mathrm{Ring}\to \mathrm{Spec}\left(R\right)=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$