evlsvvvallem

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

	Ref	Expression
Hypotheses	evlsvvvallem.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	evlsvvvallem.k	$⊢ K = {Base}_{S}$
	evlsvvvallem.m	$⊢ M = {mulGrp}_{S}$
	evlsvvvallem.w	$⊢ \underset{˙}{\times} = \cdot_{M}$
	evlsvvvallem.i	$⊢ φ \to I \in V$
	evlsvvvallem.s	$⊢ φ \to S \in CRing$
	evlsvvvallem.a	$⊢ φ \to A \in (K^{I})$
	evlsvvvallem.b	$⊢ φ \to B \in D$
Assertion	evlsvvvallem	$⊢ φ \to \underset{v \in I}{\sum_{M}} (B (v) \underset{˙}{\times} A (v)) \in K$

Proof

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

Metamath Proof Explorer

Theorem evlsvvvallem

Proof