Theorem rspecbas

Description: The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024)

	Ref	Expression
Hypothesis	rspecbas.1	No typesetting found for |- S = ( Spec ` R ) with typecode |-
Assertion	rspecbas	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2		prmidlssidl	Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
3		eqid	Could not format ( IDLsrg ` R ) = ( IDLsrg ` R ) : No typesetting found for |- ( IDLsrg ` R ) = ( IDLsrg ` R ) with typecode |-
4		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
5	3 4	idlsrgbas	Could not format ( R e. Ring -> ( LIdeal ` R ) = ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( LIdeal ` R ) = ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
6	2 5	sseqtrd	Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
7		eqid	Could not format ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) with typecode |-
8		eqid	Could not format ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) ) : No typesetting found for |- ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) ) with typecode |-
9	7 8	ressbas2	Could not format ( ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) : No typesetting found for |- ( ( PrmIdeal ` R ) C_ ( Base ` ( IDLsrg ` R ) ) -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) with typecode |-
10	6 9	syl	Could not format ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) with typecode |-
11		rspecval	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 |-
12	1 11	syl5eq	Could not format ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) with typecode |-
13	12	fveq2d	Could not format ( R e. Ring -> ( Base ` S ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( Base ` S ) = ( Base ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) ) with typecode |-
14	10 13	eqtr4d	Could not format ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = ( Base ` S ) ) with typecode |-