Theorem subrgply1

Description: A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	subrgply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
	subrgply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	subrgply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	subrgply1.b	$$⊢B={\mathrm{Base}}_U$$
Assertion	subrgply1	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		subrgply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		subrgply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		subrgply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		subrgply1.b	$$⊢B={\mathrm{Base}}_U$$
5		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
8	3 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
9	6 2 7 8	subrgmpl	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge T\in \mathrm{SubRing}\left(R\right)\right)\to B\in \mathrm{SubRing}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
10	5 9	mpan	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
11		eqidd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
12		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
13	1 12	ply1bas	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
14	13	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_S={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
15		eqid	$$⊢{+}_S={+}_S$$
16	1 6 15	ply1plusg	$$⊢{+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17	16	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	17	oveqdr	$$⊢\left(T\in \mathrm{SubRing}\left(R\right)\wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x{+}_{S}y=x{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
19		eqid	$$⊢{\cdot }_S={\cdot }_S$$
20	1 6 19	ply1mulr	$$⊢{\cdot }_S={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
21	20	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\cdot }_S={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
22	21	oveqdr	$$⊢\left(T\in \mathrm{SubRing}\left(R\right)\wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x{\cdot }_{S}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
23	11 14 18 22	subrgpropd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to \mathrm{SubRing}\left(S\right)=\mathrm{SubRing}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
24	10 23	eleqtrrd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(S\right)$$