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		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
9	3 8 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
10	6 2 7 9	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)$$
11	5 10	mpan	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
12		eqidd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
13		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
14		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
15	1 13 14	ply1bas	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	15	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_S={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17		eqid	$$⊢{+}_S={+}_S$$
18	1 6 17	ply1plusg	$$⊢{+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	18	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	19	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$$
21		eqid	$$⊢{\cdot }_S={\cdot }_S$$
22	1 6 21	ply1mulr	$$⊢{\cdot }_S={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
23	22	a1i	$$⊢T\in \mathrm{SubRing}\left(R\right)\to {\cdot }_S={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
24	23	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$$
25	12 16 20 24	subrgpropd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to \mathrm{SubRing}\left(S\right)=\mathrm{SubRing}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
26	11 25	eleqtrrd	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(S\right)$$