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	3 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11	10	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
12		eqid	$$⊢\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B=\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B$$
13	7 2 8 9 11 5 12	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$$
14		eqid	$$⊢{+}_U={+}_U$$
15	3 8 14	ply1plusg	$$⊢{+}_U={+}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
16	15	oveqi	$$⊢X{+}_{U}Y=X{+}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}Y$$
17		eqid	$$⊢{+}_S={+}_S$$
18	1 7 17	ply1plusg	$$⊢{+}_S={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	4	fvexi	$$⊢B\in \mathrm{V}$$
20	6 17	ressplusg	$$⊢B\in \mathrm{V}\to {+}_S={+}_P$$
21	19 20	ax-mp	$$⊢{+}_S={+}_P$$
22		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
23	12 22	ressplusg	$$⊢B\in \mathrm{V}\to {+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
24	19 23	ax-mp	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
25	18 21 24	3eqtr3i	$$⊢{+}_P={+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
26	25	oveqi	$$⊢X{+}_{P}Y=X{+}_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}Y$$
27	13 16 26	3eqtr4g	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{+}_{U}Y=X{+}_{P}Y$$