Theorem sdrgbas

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

	Ref	Expression
Hypothesis	sdrgbas.b	$$⊢S=R{\upharpoonright }_{𝑠}A$$
Assertion	sdrgbas	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to A={\mathrm{Base}}_S$$

Proof

Step	Hyp	Ref	Expression
1		sdrgbas.b	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3	2	sdrgss	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to A\subseteq {\mathrm{Base}}_R$$
4	1 2	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_R\to A={\mathrm{Base}}_S$$
5	3 4	syl	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to A={\mathrm{Base}}_S$$