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	⊢ 𝑆 = ( Spec ‘ 𝑅 )
Assertion	rspecbas	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		prmidlssidl	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
3		eqid	⊢ ( IDLsrg ‘ 𝑅 ) = ( IDLsrg ‘ 𝑅 )
4		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5	3 4	idlsrgbas	⊢ ( 𝑅 ∈ Ring → ( LIdeal ‘ 𝑅 ) = ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
6	2 5	sseqtrd	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) ⊆ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
7		eqid	⊢ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) )
8		eqid	⊢ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) = ( Base ‘ ( IDLsrg ‘ 𝑅 ) )
9	7 8	ressbas2	⊢ ( ( PrmIdeal ‘ 𝑅 ) ⊆ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) → ( PrmIdeal ‘ 𝑅 ) = ( Base ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ) )
10	6 9	syl	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) = ( Base ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ) )
11		rspecval	⊢ ( 𝑅 ∈ Ring → ( Spec ‘ 𝑅 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
12	1 11	syl5eq	⊢ ( 𝑅 ∈ Ring → 𝑆 = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
13	12	fveq2d	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑆 ) = ( Base ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ) )
14	10 13	eqtr4d	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )