Theorem ply1baspropd

Description: Property deduction for univariate polynomial base set. (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	ply1baspropd	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\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	mplbaspropd	$$⊢\phi \to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
5		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
6		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
8	5 6 7	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
10		eqid	$$⊢{\mathrm{PwSer}}_1\left(S\right)={\mathrm{PwSer}}_1\left(S\right)$$
11		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
12	9 10 11	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
13	4 8 12	3eqtr4g	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$