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	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fveq2	Could not format ( r = R -> ( IDLsrg ` r ) = ( IDLsrg ` R ) ) : No typesetting found for |- ( r = R -> ( IDLsrg ` r ) = ( IDLsrg ` R ) ) with typecode |-
2		fveq2	Could not format ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) : No typesetting found for |- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) with typecode |-
3	1 2	oveq12d	Could not format ( r = R -> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( r = R -> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) with typecode |-
4		df-rspec	Could not format Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) : No typesetting found for |- Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r ) ) ) with typecode |-
5		ovex	Could not format ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) e. _V : No typesetting found for |- ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) e. _V with typecode |-
6	3 4 5	fvmpt	Could not format ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) with typecode |-