Theorem sdrgbas

Description: Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025)

	Ref	Expression
Hypothesis	sdrgbas.b	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
Assertion	sdrgbas	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		sdrgbas.b	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3	2	sdrgss	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
4	1 2	ressbas2	⊢ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
5	3 4	syl	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )