Theorem ply1plusg

Description: Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	ply1plusg.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	ply1plusg.s	$$⊢S=1_{𝑜}\mathrm{mPoly}R$$
	ply1plusg.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
Assertion	ply1plusg	$$⊢\underset{\dot{}}{+}={+}_S$$

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		ply1plusg.s	$$⊢S=1_{𝑜}\mathrm{mPoly}R$$
3		ply1plusg.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
5		eqid	$$⊢{+}_S={+}_S$$
6	2 4 5	mplplusg	$$⊢{+}_S={+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
7		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
8		eqid	$$⊢{+}_{{\mathrm{PwSer}}_1\left(R\right)}={+}_{{\mathrm{PwSer}}_1\left(R\right)}$$
9	7 4 8	psr1plusg	$$⊢{+}_{{\mathrm{PwSer}}_1\left(R\right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
10		fvex	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{V}$$
11	1 7	ply1val	$$⊢Y={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
12	11 8	ressplusg	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{V}\to {+}_{{\mathrm{PwSer}}_1\left(R\right)}={+}_Y$$
13	10 12	ax-mp	$$⊢{+}_{{\mathrm{PwSer}}_1\left(R\right)}={+}_Y$$
14	6 9 13	3eqtr2i	$$⊢{+}_S={+}_Y$$
15	3 14	eqtr4i	$$⊢\underset{\dot{}}{+}={+}_S$$