Theorem subrgbas

Description: Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		subrgbas.b	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		subrgsubg	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A\in \mathrm{SubGrp}\left(R\right)$$
3	1	subgbas	$$⊢A\in \mathrm{SubGrp}\left(R\right)\to A={\mathrm{Base}}_S$$
4	2 3	syl	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A={\mathrm{Base}}_S$$