Theorem ressply1add

Description: A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	ressply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
	ressply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressply1.b	$$⊢B={\mathrm{Base}}_U$$
	ressply1.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressply1.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
Assertion	ressply1add	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{+}_{U}Y=X{+}_{P}Y$$

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		ressply1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressply1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressply1.b	$$⊢B={\mathrm{Base}}_U$$
5		ressply1.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		ressply1.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
8		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
9		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
10	3 9 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
11		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
12	11	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
13		eqid	$$⊢\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B=\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B$$
14	7 2 8 10 12 5 13	ressmpladd	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{+}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}Y=X{+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}Y$$
15		eqid	$$⊢{+}_U={+}_U$$
16	3 8 15	ply1plusg	$$⊢{+}_U={+}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
17	16	oveqi	$$⊢X{+}_{U}Y=X{+}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}Y$$
18		eqid	$$⊢{+}_S={+}_S$$
19	1 7 18	ply1plusg	$$⊢{+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	4	fvexi	$$⊢B\in \mathrm{V}$$
21	6 18	ressplusg	$$⊢B\in \mathrm{V}\to {+}_S={+}_P$$
22	20 21	ax-mp	$$⊢{+}_S={+}_P$$
23		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
24	13 23	ressplusg	$$⊢B\in \mathrm{V}\to {+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
25	20 24	ax-mp	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
26	19 22 25	3eqtr3i	$$⊢{+}_P={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
27	26	oveqi	$$⊢X{+}_{P}Y=X{+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}Y$$
28	14 17 27	3eqtr4g	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{+}_{U}Y=X{+}_{P}Y$$