Theorem ressmplvsca

Description: A restricted power series algebra has the same scalar 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	ressmplvsca	$$⊢\left(\phi \wedge \left(X\in T\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	$$⊢Y\in B\to Y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
12		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
13		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)}$$
14	12 2 8 9 13 6	resspsrvsca	$$⊢\left(\phi \wedge \left(X\in T\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$$
15	11 14	sylanr2	$$⊢\left(\phi \wedge \left(X\in T\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$$
16	4	fvexi	$$⊢B\in \mathrm{V}$$
17	3 8 4	mplval2	$$⊢U=\left(I\mathrm{mPwSer}H\right){\upharpoonright }_{𝑠}B$$
18		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_{\left(I\mathrm{mPwSer}H\right)}$$
19	17 18	ressvsca	$$⊢B\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_U$$
20	16 19	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}H\right)}={\cdot }_U$$
21	20	oveqi	$$⊢X{\cdot }_{\left(I\mathrm{mPwSer}H\right)}Y=X{\cdot }_{U}Y$$
22		fvex	$$⊢{\mathrm{Base}}_S\in \mathrm{V}$$
23		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
24	1 12 23	mplval2	$$⊢S=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_S$$
25		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
26	24 25	ressvsca	$$⊢{\mathrm{Base}}_S\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_S$$
27	22 26	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_S$$
28		fvex	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\in \mathrm{V}$$
29	13 25	ressvsca	$$⊢{\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)}$$
30	28 29	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)}$$
31		eqid	$$⊢{\cdot }_S={\cdot }_S$$
32	7 31	ressvsca	$$⊢B\in \mathrm{V}\to {\cdot }_S={\cdot }_P$$
33	16 32	ax-mp	$$⊢{\cdot }_S={\cdot }_P$$
34	27 30 33	3eqtr3i	$$⊢{\cdot }_{\left(\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}\right)}={\cdot }_P$$
35	34	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$$
36	15 21 35	3eqtr3g	$$⊢\left(\phi \wedge \left(X\in T\wedge Y\in B\right)\right)\to X{\cdot }_{U}Y=X{\cdot }_{P}Y$$