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	3	ovexi	$$⊢U\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to U\in \mathrm{V}$$
24	2 4 21 12 23	mplelsfi	$$⊢\phi \to {finSupp}_{0_U}\left(F\right)$$
25		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
26	2 25 4 1 12	mplelf	$$⊢\phi \to F:D⟶{\mathrm{Base}}_U$$
27		ssidd	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq F\mathrm{supp}{0}_U$$
28		fvexd	$$⊢\phi \to 0_U\in \mathrm{V}$$
29	26 27 12 28	suppssrg	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to F\left(b\right)=0_U$$
30		eqid	$$⊢0_S=0_S$$
31	3 30	subrg0	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 0_S=0_U$$
32	11 31	syl	$$⊢\phi \to 0_S=0_U$$
33	32	eqcomd	$$⊢\phi \to 0_U=0_S$$
34	33	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to 0_U=0_S$$
35	29 34	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to F\left(b\right)=0_S$$
36	35	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)$$
37	10	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
38	37	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\right)\to S\in \mathrm{Ring}$$
39		eldifi	$$⊢b\in \left(D\setminus {supp}_{0_U}\left(F\right)\right)\to b\in D$$
40	9	adantr	$$⊢\left(\phi \wedge b\in D\right)\to I\in V$$
41	10	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{CRing}$$
42	13	adantr	$$⊢\left(\phi \wedge b\in D\right)\to A\in \left(K^I\right)$$
43		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
44	1 5 6 7 40 41 42 43	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$$
45	39 44	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$$
46	5 8 30 38 45	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$$
47	36 46	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$$
48	15	a1i	$$⊢\phi \to D\in \mathrm{V}$$
49	47 48	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$$
50	17 18 20 24 49	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)$$