Theorem ressmplmul

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

	Ref	Expression
Hypotheses	ressmpl.s	$$⊢S=I\mathrm{mPoly}R$$
	ressmpl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressmpl.u	$$⊢U=I\mathrm{mPoly}H$$
	ressmpl.b	$$⊢B={\mathrm{Base}}_U$$
	ressmpl.1	$$⊢\phi \to I\in V$$
	ressmpl.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressmpl.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
Assertion	ressmplmul	$$⊢\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		ressmpl.s	$$⊢S=I\mathrm{mPoly}R$$
2		ressmpl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressmpl.u	$$⊢U=I\mathrm{mPoly}H$$
4		ressmpl.b	$$⊢B={\mathrm{Base}}_U$$
5		ressmpl.1	$$⊢\phi \to I\in V$$
6		ressmpl.2	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
7		ressmpl.p	$$⊢P=S{\upharpoonright }_{𝑠}B$$
8		eqid	$$⊢I\mathrm{mPwSer}H=I\mathrm{mPwSer}H$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
10	3 8 4 9	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
11	10	sseli	$$⊢X\in B\to X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
12	10	sseli	$$⊢Y\in B\to Y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
13	11 12	anim12i	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\wedge Y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)$$
14		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
15		eqid	$$⊢\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
16	14 2 8 9 15 6	resspsrmul	$$⊢\left(\phi \wedge \left(X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\wedge Y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)\right)\to X{\cdot }_{\left(I\mathrm{mPwSer}H\right)}Y=X{\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}Y$$
17	13 16	sylan2	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{\cdot }_{\left(I\mathrm{mPwSer}H\right)}Y=X{\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}Y$$
18	4	fvexi	$$⊢B\in \mathrm{V}$$
19	3 8 4	mplval2	$$⊢U=\left(I\mathrm{mPwSer}H\right){\upharpoonright }_{𝑠}B$$
20		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_{\left(I\mathrm{mPwSer}H\right)}$$
21	19 20	ressmulr	$$⊢B\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_U$$
22	18 21	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_U$$
23	22	oveqi	$$⊢X{\cdot }_{\left(I\mathrm{mPwSer}H\right)}Y=X{\cdot }_{U}Y$$
24		fvex	$$⊢{\mathrm{Base}}_S\in \mathrm{V}$$
25		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
26	1 14 25	mplval2	$$⊢S=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_S$$
27		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
28	26 27	ressmulr	$$⊢{\mathrm{Base}}_S\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_S$$
29	24 28	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_S$$
30		fvex	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\in \mathrm{V}$$
31	15 27	ressmulr	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}$$
32	30 31	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}$$
33		eqid	$$⊢{\cdot }_S={\cdot }_S$$
34	7 33	ressmulr	$$⊢B\in \mathrm{V}\to {\cdot }_S={\cdot }_P$$
35	18 34	ax-mp	$$⊢{\cdot }_S={\cdot }_P$$
36	29 32 35	3eqtr3i	$$⊢{\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}={\cdot }_P$$
37	36	oveqi	$$⊢X{\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}Y=X{\cdot }_{P}Y$$
38	17 23 37	3eqtr3g	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X{\cdot }_{U}Y=X{\cdot }_{P}Y$$