Theorem ply1plusgpropd

Description: Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1baspropd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
	ply1baspropd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
	ply1baspropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
Assertion	ply1plusgpropd	$$⊢\phi \to {+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left(S\right)}$$

Proof

Step	Hyp	Ref	Expression
1		ply1baspropd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		ply1baspropd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
3		ply1baspropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
4	1 2 3	psrplusgpropd	$$⊢\phi \to {+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
7		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	5 6 7	mplplusg	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
10		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}S=1_{𝑜}\mathrm{mPwSer}S$$
11		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
12	9 10 11	mplplusg	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}S\right)}$$
13	4 8 12	3eqtr4g	$$⊢\phi \to {+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
14		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
15		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left(R\right)}$$
16	14 5 15	ply1plusg	$$⊢{+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
18		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(S\right)}={+}_{{\mathrm{Poly}}_1\left(S\right)}$$
19	17 9 18	ply1plusg	$$⊢{+}_{{\mathrm{Poly}}_1\left(S\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
20	13 16 19	3eqtr4g	$$⊢\phi \to {+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left(S\right)}$$