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	⊢ ( 𝑅 ∈ Ring → ( Spec ‘ 𝑅 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑟 = 𝑅 → ( IDLsrg ‘ 𝑟 ) = ( IDLsrg ‘ 𝑅 ) )
2		fveq2	⊢ ( 𝑟 = 𝑅 → ( PrmIdeal ‘ 𝑟 ) = ( PrmIdeal ‘ 𝑅 ) )
3	1 2	oveq12d	⊢ ( 𝑟 = 𝑅 → ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
4		df-rspec	⊢ Spec = ( 𝑟 ∈ Ring ↦ ( ( IDLsrg ‘ 𝑟 ) ↾s ( PrmIdeal ‘ 𝑟 ) ) )
5		ovex	⊢ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑅 ∈ Ring → ( Spec ‘ 𝑅 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )