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{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
7	5 6	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8		eqid	$$⊢{\mathrm{Poly}}_1\left(S\right)={\mathrm{Poly}}_1\left(S\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$
10	8 9	ply1bas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
11	4 7 10	3eqtr4g	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(S\right)}$$