Theorem evlvvvallem

Description: Lemma for theorems using evlvvval . Version of evlsvvvallem2 using df-evl . (Contributed by SN, 11-Mar-2025)

	Ref	Expression
Hypotheses	evlvvvallem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlvvvallem.p	$$⊢P=I\mathrm{mPoly}R$$
	evlvvvallem.b	$$⊢B={\mathrm{Base}}_P$$
	evlvvvallem.k	$$⊢K={\mathrm{Base}}_R$$
	evlvvvallem.m	$$⊢M={\mathrm{mulGrp}}_R$$
	evlvvvallem.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlvvvallem.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	evlvvvallem.i	$$⊢\phi \to I\in V$$
	evlvvvallem.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlvvvallem.f	$$⊢\phi \to F\in B$$
	evlvvvallem.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	evlvvvallem	$$⊢\phi \to {finSupp}_{0_R}\left(\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{v\in I}{{\sum }_M},\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlvvvallem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		evlvvvallem.p	$$⊢P=I\mathrm{mPoly}R$$
3		evlvvvallem.b	$$⊢B={\mathrm{Base}}_P$$
4		evlvvvallem.k	$$⊢K={\mathrm{Base}}_R$$
5		evlvvvallem.m	$$⊢M={\mathrm{mulGrp}}_R$$
6		evlvvvallem.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
7		evlvvvallem.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		evlvvvallem.i	$$⊢\phi \to I\in V$$
9		evlvvvallem.r	$$⊢\phi \to R\in \mathrm{CRing}$$
10		evlvvvallem.f	$$⊢\phi \to F\in B$$
11		evlvvvallem.a	$$⊢\phi \to A\in \left(K^I\right)$$
12		eqid	$$⊢I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)=I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)$$
13		eqid	$$⊢R{\upharpoonright }_{𝑠}K=R{\upharpoonright }_{𝑠}K$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)\right)}$$
15	9	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
16	4	subrgid	$$⊢R\in \mathrm{Ring}\to K\in \mathrm{SubRing}\left(R\right)$$
17	15 16	syl	$$⊢\phi \to K\in \mathrm{SubRing}\left(R\right)$$
18	4	ressid	$$⊢R\in \mathrm{CRing}\to R{\upharpoonright }_{𝑠}K=R$$
19	9 18	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}K=R$$
20	19	oveq2d	$$⊢\phi \to I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)=I\mathrm{mPoly}R$$
21	20 2	eqtr4di	$$⊢\phi \to I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)=P$$
22	21	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)\right)}={\mathrm{Base}}_P$$
23	22 3	eqtr4di	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)\right)}=B$$
24	10 23	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}K\right)\right)}$$
25	1 12 13 14 4 5 6 7 8 9 17 24 11	evlsvvvallem2	$$⊢\phi \to {finSupp}_{0_R}\left(\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{v\in I}{{\sum }_M},\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)\right)\right)$$