Theorem evlsvvvallem

Description: Lemma for evlsvvval akin to psrbagev2 . (Contributed by SN, 6-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvvallem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsvvvallem.k	$$⊢K={\mathrm{Base}}_S$$
	evlsvvvallem.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evlsvvvallem.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsvvvallem.i	$$⊢\phi \to I\in V$$
	evlsvvvallem.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsvvvallem.a	$$⊢\phi \to A\in \left(K^I\right)$$
	evlsvvvallem.b	$$⊢\phi \to B\in D$$
Assertion	evlsvvvallem	$$⊢\phi \to \underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		evlsvvvallem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		evlsvvvallem.k	$$⊢K={\mathrm{Base}}_S$$
3		evlsvvvallem.m	$$⊢M={\mathrm{mulGrp}}_S$$
4		evlsvvvallem.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
5		evlsvvvallem.i	$$⊢\phi \to I\in V$$
6		evlsvvvallem.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evlsvvvallem.a	$$⊢\phi \to A\in \left(K^I\right)$$
8		evlsvvvallem.b	$$⊢\phi \to B\in D$$
9	3 2	mgpbas	$$⊢K={\mathrm{Base}}_M$$
10		eqid	$$⊢1_S=1_S$$
11	3 10	ringidval	$$⊢1_S=0_M$$
12	3	crngmgp	$$⊢S\in \mathrm{CRing}\to M\in \mathrm{CMnd}$$
13	6 12	syl	$$⊢\phi \to M\in \mathrm{CMnd}$$
14	6	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
15	3	ringmgp	$$⊢S\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
16	14 15	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
17	16	adantr	$$⊢\left(\phi \wedge v\in I\right)\to M\in \mathrm{Mnd}$$
18	1	psrbagf	$$⊢B\in D\to B:I⟶{\mathbb{N}}_0$$
19	8 18	syl	$$⊢\phi \to B:I⟶{\mathbb{N}}_0$$
20	19	ffvelcdmda	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right)\in {\mathbb{N}}_0$$
21		elmapi	$$⊢A\in \left(K^I\right)\to A:I⟶K$$
22	7 21	syl	$$⊢\phi \to A:I⟶K$$
23	22	ffvelcdmda	$$⊢\left(\phi \wedge v\in I\right)\to A\left(v\right)\in K$$
24	9 4 17 20 23	mulgnn0cld	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\in K$$
25	24	fmpttd	$$⊢\phi \to \left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right):I⟶K$$
26	5	mptexd	$$⊢\phi \to \left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in \mathrm{V}$$
27		fvexd	$$⊢\phi \to 1_S\in \mathrm{V}$$
28	25	ffund	$$⊢\phi \to \mathrm{Fun}\left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)$$
29	1	psrbagfsupp	$$⊢B\in D\to {finSupp}_0\left(B\right)$$
30	8 29	syl	$$⊢\phi \to {finSupp}_0\left(B\right)$$
31		ssidd	$$⊢\phi \to B\mathrm{supp}0\subseteq B\mathrm{supp}0$$
32		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
33	19 31 5 32	suppssr	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to B\left(v\right)=0$$
34	33	oveq1d	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)=0\underset{\dot{}}{\times }A\left(v\right)$$
35		eldifi	$$⊢v\in \left(I\setminus {supp}_0\left(B\right)\right)\to v\in I$$
36	35 23	sylan2	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to A\left(v\right)\in K$$
37	9 11 4	mulg0	$$⊢A\left(v\right)\in K\to 0\underset{\dot{}}{\times }A\left(v\right)=1_S$$
38	36 37	syl	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to 0\underset{\dot{}}{\times }A\left(v\right)=1_S$$
39	34 38	eqtrd	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)=1_S$$
40	39 5	suppss2	$$⊢\phi \to \left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\mathrm{supp}{1}_S\subseteq B\mathrm{supp}0$$
41	26 27 28 30 40	fsuppsssuppgd	$$⊢\phi \to {finSupp}_{1_S}\left(\left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)$$
42	9 11 13 5 25 41	gsumcl	$$⊢\phi \to \underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in K$$