Theorem sdrgbas

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

	Ref	Expression
Hypothesis	sdrgbas.b	|- S = ( R |`s A )
Assertion	sdrgbas	|- ( A e. ( SubDRing ` R ) -> A = ( Base ` S ) )

Proof

Step	Hyp	Ref	Expression
1		sdrgbas.b	|- S = ( R |`s A )
2		eqid	|- ( Base ` R ) = ( Base ` R )
3	2	sdrgss	|- ( A e. ( SubDRing ` R ) -> A C_ ( Base ` R ) )
4	1 2	ressbas2	|- ( A C_ ( Base ` R ) -> A = ( Base ` S ) )
5	3 4	syl	|- ( A e. ( SubDRing ` R ) -> A = ( Base ` S ) )