Theorem evlsvvvallem2

Description: Lemma for theorems using evlsvvval . (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvvallem2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsvvvallem2.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsvvvallem2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsvvvallem2.b	$$⊢B={\mathrm{Base}}_P$$
	evlsvvvallem2.k	$$⊢K={\mathrm{Base}}_S$$
	evlsvvvallem2.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evlsvvvallem2.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsvvvallem2.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlsvvvallem2.i	$$⊢\phi \to I\in V$$
	evlsvvvallem2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsvvvallem2.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsvvvallem2.f	$$⊢\phi \to F\in B$$
	evlsvvvallem2.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	evlsvvvallem2	$$⊢\phi \to {finSupp}_{0_S}\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		evlsvvvallem2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		evlsvvvallem2.p	$$⊢P=I\mathrm{mPoly}U$$
3		evlsvvvallem2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evlsvvvallem2.b	$$⊢B={\mathrm{Base}}_P$$
5		evlsvvvallem2.k	$$⊢K={\mathrm{Base}}_S$$
6		evlsvvvallem2.m	$$⊢M={\mathrm{mulGrp}}_S$$
7		evlsvvvallem2.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
8		evlsvvvallem2.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
9		evlsvvvallem2.i	$$⊢\phi \to I\in V$$
10		evlsvvvallem2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
11		evlsvvvallem2.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
12		evlsvvvallem2.f	$$⊢\phi \to F\in B$$
13		evlsvvvallem2.a	$$⊢\phi \to A\in \left(K^I\right)$$
14		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
15	1 14	rabex2	$$⊢D\in \mathrm{V}$$
16	15	mptex	$$⊢\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)\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \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)\in \mathrm{V}$$
18		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
19		funmpt	$$⊢\mathrm{Fun}\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)$$
20	19	a1i	$$⊢\phi \to \mathrm{Fun}\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)$$
21		eqid	$$⊢0_U=0_U$$
22	2 4 21 12	mplelsfi	$$⊢\phi \to {finSupp}_{0_U}\left(F\right)$$
23		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
24	2 23 4 1 12	mplelf	$$⊢\phi \to F:D⟶{\mathrm{Base}}_U$$
25		ssidd	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq F\mathrm{supp}{0}_U$$
26		fvexd	$$⊢\phi \to 0_U\in \mathrm{V}$$
27	24 25 12 26	suppssrg	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to F\left(b\right)=0_U$$
28		eqid	$$⊢0_S=0_S$$
29	3 28	subrg0	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 0_S=0_U$$
30	11 29	syl	$$⊢\phi \to 0_S=0_U$$
31	30	eqcomd	$$⊢\phi \to 0_U=0_S$$
32	31	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to 0_U=0_S$$
33	27 32	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to F\left(b\right)=0_S$$
34	33	oveq1d	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to 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)=0_S\underset{\dot{}}{·}\left(\underset{v\in I}{{\sum }_M},\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)$$
35	10	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
36	35	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to S\in \mathrm{Ring}$$
37		eldifi	$$⊢b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\to b\in D$$
38	9	adantr	$$⊢\left(\phi \wedge b\in D\right)\to I\in V$$
39	10	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{CRing}$$
40	13	adantr	$$⊢\left(\phi \wedge b\in D\right)\to A\in \left(K^I\right)$$
41		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
42	1 5 6 7 38 39 40 41	evlsvvvallem	$$⊢\left(\phi \wedge b\in D\right)\to \underset{v\in I}{{\sum }_M}\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in K$$
43	37 42	sylan2	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to \underset{v\in I}{{\sum }_M}\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in K$$
44	5 8 28 36 43	ringlzd	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to 0_S\underset{\dot{}}{·}\left(\underset{v\in I}{{\sum }_M},\left(b\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)=0_S$$
45	34 44	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to 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)=0_S$$
46	15	a1i	$$⊢\phi \to D\in \mathrm{V}$$
47	45 46	suppss2	$$⊢\phi \to \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)\mathrm{supp}{0}_S\subseteq F\mathrm{supp}{0}_U$$
48	17 18 20 22 47	fsuppsssuppgd	$$⊢\phi \to {finSupp}_{0_S}\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)$$