Theorem ressply1mul

Description: A restricted polynomial algebra has the same multiplication 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	ressply1mul	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{\cdot }_{U}Y=X{\cdot }_{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	ressmplmul	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}H\right)}Y=X{\cdot }_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}Y$$
15		eqid	$$⊢{\cdot }_U={\cdot }_U$$
16	3 8 15	ply1mulr	$$⊢{\cdot }_U={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
17	16	oveqi	$$⊢X{\cdot }_{U}Y=X{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}H\right)}Y$$
18		eqid	$$⊢{\cdot }_S={\cdot }_S$$
19	1 7 18	ply1mulr	$$⊢{\cdot }_S={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	4	fvexi	$$⊢B\in \mathrm{V}$$
21	6 18	ressmulr	$$⊢B\in \mathrm{V}\to {\cdot }_S={\cdot }_P$$
22	20 21	ax-mp	$$⊢{\cdot }_S={\cdot }_P$$
23		eqid	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
24	13 23	ressmulr	$$⊢B\in \mathrm{V}\to {\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\cdot }_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
25	20 24	ax-mp	$$⊢{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\cdot }_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
26	19 22 25	3eqtr3i	$$⊢{\cdot }_P={\cdot }_{\left(\left(1_{𝑜}\mathrm{mPoly}R\right){\upharpoonright }_{𝑠}B\right)}$$
27	26	oveqi	$$⊢X{\cdot }_{P}Y=X{\cdot }_{\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{\cdot }_{U}Y=X{\cdot }_{P}Y$$