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	$$⊢S=\mathrm{Spec}\left(R\right)$$
Assertion	rspecbas	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)={\mathrm{Base}}_S$$

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	$$⊢S=\mathrm{Spec}\left(R\right)$$
2		prmidlssidl	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)\subseteq \mathrm{LIdeal}\left(R\right)$$
3		eqid	$$⊢\mathrm{IDLsrg}\left(R\right)=\mathrm{IDLsrg}\left(R\right)$$
4		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
5	3 4	idlsrgbas	$$⊢R\in \mathrm{Ring}\to \mathrm{LIdeal}\left(R\right)={\mathrm{Base}}_{\mathrm{IDLsrg}\left(R\right)}$$
6	2 5	sseqtrd	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)\subseteq {\mathrm{Base}}_{\mathrm{IDLsrg}\left(R\right)}$$
7		eqid	$$⊢\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$
8		eqid	$$⊢{\mathrm{Base}}_{\mathrm{IDLsrg}\left(R\right)}={\mathrm{Base}}_{\mathrm{IDLsrg}\left(R\right)}$$
9	7 8	ressbas2	$$⊢\mathrm{PrmIdeal}\left(R\right)\subseteq {\mathrm{Base}}_{\mathrm{IDLsrg}\left(R\right)}\to \mathrm{PrmIdeal}\left(R\right)={\mathrm{Base}}_{\left(\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)\right)}$$
10	6 9	syl	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)={\mathrm{Base}}_{\left(\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)\right)}$$
11		rspecval	$$⊢R\in \mathrm{Ring}\to \mathrm{Spec}\left(R\right)=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$
12	1 11	eqtrid	$$⊢R\in \mathrm{Ring}\to S=\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)$$
13	12	fveq2d	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_S={\mathrm{Base}}_{\left(\mathrm{IDLsrg}\left(R\right){\upharpoonright }_{𝑠}\mathrm{PrmIdeal}\left(R\right)\right)}$$
14	10 13	eqtr4d	$$⊢R\in \mathrm{Ring}\to \mathrm{PrmIdeal}\left(R\right)={\mathrm{Base}}_S$$