evlsvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. This is the sum of the evaluations for each term (corresponding to a bag of variables), that is, the coefficient times the product of each variable raised to the corresponding power. (Contributed by SN, 5-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvval.q	$⊢ Q = (I evalSub S) (R)$
	evlsvvval.p	$⊢ P = I mPoly U$
	evlsvvval.b	$⊢ B = {Base}_{P}$
	evlsvvval.u	$⊢ U = S ↾_{𝑠} R$
	evlsvvval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	evlsvvval.k	$⊢ K = {Base}_{S}$
	evlsvvval.m	$⊢ M = {mulGrp}_{S}$
	evlsvvval.w	$⊢ \underset{˙}{\times} = \cdot_{M}$
	evlsvvval.x	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evlsvvval.i	$⊢ φ \to I \in V$
	evlsvvval.s	$⊢ φ \to S \in CRing$
	evlsvvval.r	$⊢ φ \to R \in SubRing (S)$
	evlsvvval.f	$⊢ φ \to F \in B$
	evlsvvval.a	$⊢ φ \to A \in (K^{I})$
Assertion	evlsvvval	$⊢ φ \to Q (F) (A) = \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i))))$

Proof

Step	Hyp	Ref	Expression
1		evlsvvval.q	$⊢ Q = (I evalSub S) (R)$
2		evlsvvval.p	$⊢ P = I mPoly U$
3		evlsvvval.b	$⊢ B = {Base}_{P}$
4		evlsvvval.u	$⊢ U = S ↾_{𝑠} R$
5		evlsvvval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
6		evlsvvval.k	$⊢ K = {Base}_{S}$
7		evlsvvval.m	$⊢ M = {mulGrp}_{S}$
8		evlsvvval.w	$⊢ \underset{˙}{\times} = \cdot_{M}$
9		evlsvvval.x	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
10		evlsvvval.i	$⊢ φ \to I \in V$
11		evlsvvval.s	$⊢ φ \to S \in CRing$
12		evlsvvval.r	$⊢ φ \to R \in SubRing (S)$
13		evlsvvval.f	$⊢ φ \to F \in B$
14		evlsvvval.a	$⊢ φ \to A \in (K^{I})$
15		fveq1	$⊢ l = A \to l (i) = A (i)$
16	15	oveq2d	$⊢ l = A \to b (i) \underset{˙}{\times} l (i) = b (i) \underset{˙}{\times} A (i)$
17	16	mpteq2dv	$⊢ l = A \to (i \in I ⟼ b (i) \underset{˙}{\times} l (i)) = (i \in I ⟼ b (i) \underset{˙}{\times} A (i))$
18	17	oveq2d	$⊢ l = A \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i)) = \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} A (i))$
19	18	oveq2d	$⊢ l = A \to F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))) = F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i)))$
20	19	mpteq2dv	$⊢ l = A \to (b \in D ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))) = (b \in D ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i))))$
21	20	oveq2d	$⊢ l = A \to \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))) = \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i))))$
22		eqid	$⊢ S ↑_{𝑠} (K^{I}) = S ↑_{𝑠} (K^{I})$
23		eqid	$⊢ {mulGrp}_{(S ↑_{𝑠} (K^{I}))} = {mulGrp}_{(S ↑_{𝑠} (K^{I}))}$
24		eqid	$⊢ \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} = \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}$
25		eqid	$⊢ \cdot_{(S ↑_{𝑠} (K^{I}))} = \cdot_{(S ↑_{𝑠} (K^{I}))}$
26		eqid	$⊢ (x \in R ⟼ (K^{I}) \times \{x\}) = (x \in R ⟼ (K^{I}) \times \{x\})$
27		eqid	$⊢ (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) = (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))$
28	1 2 3 5 6 4 22 23 24 25 26 27 10 11 12 13	evlsvval	$⊢ φ \to Q (F) = \underset{b \in D}{\sum_{S ↑_{𝑠} (K^{I})}} ((x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) \cdot_{(S ↑_{𝑠} (K^{I}))} (\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}, (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))))))$
29		sneq	$⊢ x = F (b) \to \{x\} = \{F (b)\}$
30	29	xpeq2d	$⊢ x = F (b) \to (K^{I}) \times \{x\} = (K^{I}) \times \{F (b)\}$
31		eqid	$⊢ {Base}_{U} = {Base}_{U}$
32	2 31 3 5 13	mplelf	$⊢ φ \to F : D ⟶ {Base}_{U}$
33	4	subrgbas	$⊢ R \in SubRing (S) \to R = {Base}_{U}$
34	12 33	syl	$⊢ φ \to R = {Base}_{U}$
35	34	feq3d	$⊢ φ \to (F : D ⟶ R \leftrightarrow F : D ⟶ {Base}_{U})$
36	32 35	mpbird	$⊢ φ \to F : D ⟶ R$
37	36	ffvelcdmda	$⊢ (φ \land b \in D) \to F (b) \in R$
38		ovex	$⊢ K^{I} \in V$
39		snex	$⊢ \{F (b)\} \in V$
40	38 39	xpex	$⊢ (K^{I}) \times \{F (b)\} \in V$
41	40	a1i	$⊢ (φ \land b \in D) \to (K^{I}) \times \{F (b)\} \in V$
42	26 30 37 41	fvmptd3	$⊢ (φ \land b \in D) \to (x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) = (K^{I}) \times \{F (b)\}$
43	5	psrbagf	$⊢ b \in D \to b : I ⟶ ℕ_{0}$
44	43	adantl	$⊢ (φ \land b \in D) \to b : I ⟶ ℕ_{0}$
45	44	ffnd	$⊢ (φ \land b \in D) \to b Fn I$
46	38	mptex	$⊢ (a \in (K^{I}) ⟼ a (x)) \in V$
47	46 27	fnmpti	$⊢ (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) Fn I$
48	47	a1i	$⊢ (φ \land b \in D) \to (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) Fn I$
49	10	adantr	$⊢ (φ \land b \in D) \to I \in V$
50		inidm	$⊢ I \cap I = I$
51		eqidd	$⊢ ((φ \land b \in D) \land i \in I) \to b (i) = b (i)$
52		fveq2	$⊢ x = i \to a (x) = a (i)$
53	52	mpteq2dv	$⊢ x = i \to (a \in (K^{I}) ⟼ a (x)) = (a \in (K^{I}) ⟼ a (i))$
54		simpr	$⊢ ((φ \land b \in D) \land i \in I) \to i \in I$
55		eqid	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} (K^{I}))}$
56	11	ad2antrr	$⊢ ((φ \land b \in D) \land i \in I) \to S \in CRing$
57		ovexd	$⊢ ((φ \land b \in D) \land i \in I) \to K^{I} \in V$
58		elmapi	$⊢ a \in (K^{I}) \to a : I ⟶ K$
59	58	ffvelcdmda	$⊢ (a \in (K^{I}) \land i \in I) \to a (i) \in K$
60	59	ancoms	$⊢ (i \in I \land a \in (K^{I})) \to a (i) \in K$
61	60	adantll	$⊢ (((φ \land b \in D) \land i \in I) \land a \in (K^{I})) \to a (i) \in K$
62	61	fmpttd	$⊢ ((φ \land b \in D) \land i \in I) \to (a \in (K^{I}) ⟼ a (i)) : K^{I} ⟶ K$
63	22 6 55 56 57 62	pwselbasr	$⊢ ((φ \land b \in D) \land i \in I) \to (a \in (K^{I}) ⟼ a (i)) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
64	27 53 54 63	fvmptd3	$⊢ ((φ \land b \in D) \land i \in I) \to (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) (i) = (a \in (K^{I}) ⟼ a (i))$
65	45 48 49 49 50 51 64	offval	$⊢ (φ \land b \in D) \to b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) = (i \in I ⟼ b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i)))$
66	23 55	mgpbas	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}$
67	11	crngringd	$⊢ φ \to S \in Ring$
68		ovexd	$⊢ φ \to K^{I} \in V$
69	22	pwsring	$⊢ (S \in Ring \land K^{I} \in V) \to S ↑_{𝑠} (K^{I}) \in Ring$
70	67 68 69	syl2anc	$⊢ φ \to S ↑_{𝑠} (K^{I}) \in Ring$
71	23	ringmgp	$⊢ S ↑_{𝑠} (K^{I}) \in Ring \to {mulGrp}_{(S ↑_{𝑠} (K^{I}))} \in Mnd$
72	70 71	syl	$⊢ φ \to {mulGrp}_{(S ↑_{𝑠} (K^{I}))} \in Mnd$
73	72	ad2antrr	$⊢ ((φ \land b \in D) \land i \in I) \to {mulGrp}_{(S ↑_{𝑠} (K^{I}))} \in Mnd$
74	44	ffvelcdmda	$⊢ ((φ \land b \in D) \land i \in I) \to b (i) \in ℕ_{0}$
75	66 24 73 74 63	mulgnn0cld	$⊢ ((φ \land b \in D) \land i \in I) \to b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i)) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
76	22 6 55 56 57 75	pwselbas	$⊢ ((φ \land b \in D) \land i \in I) \to (b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i))) : K^{I} ⟶ K$
77	76	ffnd	$⊢ ((φ \land b \in D) \land i \in I) \to (b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i))) Fn (K^{I})$
78		ovex	$⊢ b (i) \underset{˙}{\times} m (i) \in V$
79		eqid	$⊢ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) = (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))$
80	78 79	fnmpti	$⊢ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) Fn (K^{I})$
81	80	a1i	$⊢ ((φ \land b \in D) \land i \in I) \to (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) Fn (K^{I})$
82		eqid	$⊢ (a \in (K^{I}) ⟼ a (i)) = (a \in (K^{I}) ⟼ a (i))$
83		fveq1	$⊢ a = p \to a (i) = p (i)$
84		simpr	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to p \in (K^{I})$
85		fvexd	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to p (i) \in V$
86	82 83 84 85	fvmptd3	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to (a \in (K^{I}) ⟼ a (i)) (p) = p (i)$
87	86	oveq2d	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to b (i) \underset{˙}{\times} (a \in (K^{I}) ⟼ a (i)) (p) = b (i) \underset{˙}{\times} p (i)$
88	67	ad3antrrr	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to S \in Ring$
89		ovexd	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to K^{I} \in V$
90	74	adantr	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to b (i) \in ℕ_{0}$
91	63	adantr	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to (a \in (K^{I}) ⟼ a (i)) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
92	22 55 23 7 24 8 88 89 90 91 84	pwsexpg	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to (b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i))) (p) = b (i) \underset{˙}{\times} (a \in (K^{I}) ⟼ a (i)) (p)$
93		fveq1	$⊢ m = p \to m (i) = p (i)$
94	93	oveq2d	$⊢ m = p \to b (i) \underset{˙}{\times} m (i) = b (i) \underset{˙}{\times} p (i)$
95		ovexd	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to b (i) \underset{˙}{\times} p (i) \in V$
96	79 94 84 95	fvmptd3	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) (p) = b (i) \underset{˙}{\times} p (i)$
97	87 92 96	3eqtr4d	$⊢ (((φ \land b \in D) \land i \in I) \land p \in (K^{I})) \to (b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i))) (p) = (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) (p)$
98	77 81 97	eqfnfvd	$⊢ ((φ \land b \in D) \land i \in I) \to b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i)) = (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))$
99	98	mpteq2dva	$⊢ (φ \land b \in D) \to (i \in I ⟼ b (i) \cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (a \in (K^{I}) ⟼ a (i))) = (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)))$
100	65 99	eqtrd	$⊢ (φ \land b \in D) \to b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))) = (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)))$
101	100	oveq2d	$⊢ (φ \land b \in D) \to \sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))) = \underset{i \in I}{\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}} (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))$
102		eqid	$⊢ 1_{(S ↑_{𝑠} (K^{I}))} = 1_{(S ↑_{𝑠} (K^{I}))}$
103		ovexd	$⊢ (φ \land b \in D) \to K^{I} \in V$
104	11	adantr	$⊢ (φ \land b \in D) \to S \in CRing$
105	7 6	mgpbas	$⊢ K = {Base}_{M}$
106	7	ringmgp	$⊢ S \in Ring \to M \in Mnd$
107	67 106	syl	$⊢ φ \to M \in Mnd$
108	107	ad2antrr	$⊢ ((φ \land b \in D) \land (m \in (K^{I}) \land i \in I)) \to M \in Mnd$
109	74	adantrl	$⊢ ((φ \land b \in D) \land (m \in (K^{I}) \land i \in I)) \to b (i) \in ℕ_{0}$
110		elmapi	$⊢ m \in (K^{I}) \to m : I ⟶ K$
111	110	ffvelcdmda	$⊢ (m \in (K^{I}) \land i \in I) \to m (i) \in K$
112	111	adantl	$⊢ ((φ \land b \in D) \land (m \in (K^{I}) \land i \in I)) \to m (i) \in K$
113	105 8 108 109 112	mulgnn0cld	$⊢ ((φ \land b \in D) \land (m \in (K^{I}) \land i \in I)) \to b (i) \underset{˙}{\times} m (i) \in K$
114	49	mptexd	$⊢ (φ \land b \in D) \to (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))) \in V$
115		fvexd	$⊢ (φ \land b \in D) \to 1_{(S ↑_{𝑠} (K^{I}))} \in V$
116		funmpt	$⊢ Fun (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)))$
117	116	a1i	$⊢ (φ \land b \in D) \to Fun (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)))$
118	5	psrbagfsupp	$⊢ b \in D \to {finSupp}_{0} (b)$
119	118	adantl	$⊢ (φ \land b \in D) \to {finSupp}_{0} (b)$
120		ssidd	$⊢ (φ \land b \in D) \to b supp 0 \subseteq b supp 0$
121		0cnd	$⊢ (φ \land b \in D) \to 0 \in ℂ$
122	44 120 49 121	suppssr	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to b (i) = 0$
123	122	oveq1d	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to b (i) \underset{˙}{\times} m (i) = 0 \underset{˙}{\times} m (i)$
124	123	adantr	$⊢ (((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \land m \in (K^{I})) \to b (i) \underset{˙}{\times} m (i) = 0 \underset{˙}{\times} m (i)$
125		eldifi	$⊢ i \in (I ∖ {supp}_{0} (b)) \to i \in I$
126	125 111	sylan2	$⊢ (m \in (K^{I}) \land i \in (I ∖ {supp}_{0} (b))) \to m (i) \in K$
127	126	ancoms	$⊢ (i \in (I ∖ {supp}_{0} (b)) \land m \in (K^{I})) \to m (i) \in K$
128	127	adantll	$⊢ (((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \land m \in (K^{I})) \to m (i) \in K$
129		eqid	$⊢ 1_{S} = 1_{S}$
130	7 129	ringidval	$⊢ 1_{S} = 0_{M}$
131	105 130 8	mulg0	$⊢ m (i) \in K \to 0 \underset{˙}{\times} m (i) = 1_{S}$
132	128 131	syl	$⊢ (((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \land m \in (K^{I})) \to 0 \underset{˙}{\times} m (i) = 1_{S}$
133	124 132	eqtrd	$⊢ (((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \land m \in (K^{I})) \to b (i) \underset{˙}{\times} m (i) = 1_{S}$
134	133	mpteq2dva	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) = (m \in (K^{I}) ⟼ 1_{S})$
135		fconstmpt	$⊢ (K^{I}) \times \{1_{S}\} = (m \in (K^{I}) ⟼ 1_{S})$
136	22 129	pws1	$⊢ (S \in Ring \land K^{I} \in V) \to (K^{I}) \times \{1_{S}\} = 1_{(S ↑_{𝑠} (K^{I}))}$
137	67 68 136	syl2anc	$⊢ φ \to (K^{I}) \times \{1_{S}\} = 1_{(S ↑_{𝑠} (K^{I}))}$
138	137	ad2antrr	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to (K^{I}) \times \{1_{S}\} = 1_{(S ↑_{𝑠} (K^{I}))}$
139	135 138	eqtr3id	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to (m \in (K^{I}) ⟼ 1_{S}) = 1_{(S ↑_{𝑠} (K^{I}))}$
140	134 139	eqtrd	$⊢ ((φ \land b \in D) \land i \in (I ∖ {supp}_{0} (b))) \to (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) = 1_{(S ↑_{𝑠} (K^{I}))}$
141	140 49	suppss2	$⊢ (φ \land b \in D) \to (i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))) supp 1_{(S ↑_{𝑠} (K^{I}))} \subseteq b supp 0$
142	114 115 117 119 141	fsuppsssuppgd	$⊢ (φ \land b \in D) \to {finSupp}_{1_{(S ↑_{𝑠} (K^{I}))}} ((i \in I ⟼ (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i))))$
143	22 6 102 23 7 103 49 104 113 142	pwsgprod	$⊢ (φ \land b \in D) \to \underset{i \in I}{\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}} (m \in (K^{I}) ⟼ b (i) \underset{˙}{\times} m (i)) = (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)))$
144	101 143	eqtrd	$⊢ (φ \land b \in D) \to \sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}} (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))) = (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)))$
145	42 144	oveq12d	$⊢ (φ \land b \in D) \to (x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) \cdot_{(S ↑_{𝑠} (K^{I}))} (\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}, (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))))) = ((K^{I}) \times \{F (b)\}) \cdot_{(S ↑_{𝑠} (K^{I}))} (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)))$
146	6	subrgss	$⊢ R \in SubRing (S) \to R \subseteq K$
147	33 146	eqsstrrd	$⊢ R \in SubRing (S) \to {Base}_{U} \subseteq K$
148	12 147	syl	$⊢ φ \to {Base}_{U} \subseteq K$
149	32 148	fssd	$⊢ φ \to F : D ⟶ K$
150	149	ffvelcdmda	$⊢ (φ \land b \in D) \to F (b) \in K$
151		fconst6g	$⊢ F (b) \in K \to ((K^{I}) \times \{F (b)\}) : K^{I} ⟶ K$
152	150 151	syl	$⊢ (φ \land b \in D) \to ((K^{I}) \times \{F (b)\}) : K^{I} ⟶ K$
153	22 6 55 104 103 152	pwselbasr	$⊢ (φ \land b \in D) \to (K^{I}) \times \{F (b)\} \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
154	10	ad2antrr	$⊢ ((φ \land b \in D) \land m \in (K^{I})) \to I \in V$
155	11	ad2antrr	$⊢ ((φ \land b \in D) \land m \in (K^{I})) \to S \in CRing$
156		simpr	$⊢ ((φ \land b \in D) \land m \in (K^{I})) \to m \in (K^{I})$
157		simplr	$⊢ ((φ \land b \in D) \land m \in (K^{I})) \to b \in D$
158	5 6 7 8 154 155 156 157	evlsvvvallem	$⊢ ((φ \land b \in D) \land m \in (K^{I})) \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)) \in K$
159	158	fmpttd	$⊢ (φ \land b \in D) \to (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) : K^{I} ⟶ K$
160	22 6 55 104 103 159	pwselbasr	$⊢ (φ \land b \in D) \to (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
161	22 55 104 103 153 160 9 25	pwsmulrval	$⊢ (φ \land b \in D) \to ((K^{I}) \times \{F (b)\}) \cdot_{(S ↑_{𝑠} (K^{I}))} (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) = ((K^{I}) \times \{F (b)\}) {\underset{˙}{\cdot}}_{f} (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)))$
162	152	ffnd	$⊢ (φ \land b \in D) \to ((K^{I}) \times \{F (b)\}) Fn (K^{I})$
163		ovex	$⊢ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)) \in V$
164		eqid	$⊢ (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) = (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)))$
165	163 164	fnmpti	$⊢ (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) Fn (K^{I})$
166	165	a1i	$⊢ (φ \land b \in D) \to (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) Fn (K^{I})$
167		inidm	$⊢ (K^{I}) \cap (K^{I}) = K^{I}$
168		fvex	$⊢ F (b) \in V$
169	168	fvconst2	$⊢ l \in (K^{I}) \to ((K^{I}) \times \{F (b)\}) (l) = F (b)$
170	169	adantl	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to ((K^{I}) \times \{F (b)\}) (l) = F (b)$
171		fveq1	$⊢ m = l \to m (i) = l (i)$
172	171	oveq2d	$⊢ m = l \to b (i) \underset{˙}{\times} m (i) = b (i) \underset{˙}{\times} l (i)$
173	172	mpteq2dv	$⊢ m = l \to (i \in I ⟼ b (i) \underset{˙}{\times} m (i)) = (i \in I ⟼ b (i) \underset{˙}{\times} l (i))$
174	173	oveq2d	$⊢ m = l \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i)) = \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i))$
175		simpr	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to l \in (K^{I})$
176	10	ad2antrr	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to I \in V$
177	11	ad2antrr	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to S \in CRing$
178		simplr	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to b \in D$
179	5 6 7 8 176 177 175 178	evlsvvvallem	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i)) \in K$
180	164 174 175 179	fvmptd3	$⊢ ((φ \land b \in D) \land l \in (K^{I})) \to (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) (l) = \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i))$
181	162 166 103 103 167 170 180	offval	$⊢ (φ \land b \in D) \to ((K^{I}) \times \{F (b)\}) {\underset{˙}{\cdot}}_{f} (m \in (K^{I}) ⟼ \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} m (i))) = (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))$
182	145 161 181	3eqtrd	$⊢ (φ \land b \in D) \to (x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) \cdot_{(S ↑_{𝑠} (K^{I}))} (\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}, (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x))))) = (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))$
183	182	mpteq2dva	$⊢ φ \to (b \in D ⟼ (x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) \cdot_{(S ↑_{𝑠} (K^{I}))} (\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}, (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))))) = (b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))))$
184	183	oveq2d	$⊢ φ \to \underset{b \in D}{\sum_{S ↑_{𝑠} (K^{I})}} ((x \in R ⟼ (K^{I}) \times \{x\}) (F (b)) \cdot_{(S ↑_{𝑠} (K^{I}))} (\sum_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}, (b {\cdot_{{mulGrp}_{(S ↑_{𝑠} (K^{I}))}}}_{f} (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))))) = \underset{b \in D}{\sum_{S ↑_{𝑠} (K^{I})}} (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))$
185		eqid	$⊢ 0_{(S ↑_{𝑠} (K^{I}))} = 0_{(S ↑_{𝑠} (K^{I}))}$
186		ovexd	$⊢ φ \to {ℕ_{0}}^{I} \in V$
187	5 186	rabexd	$⊢ φ \to D \in V$
188	67	ringcmnd	$⊢ φ \to S \in CMnd$
189	67	adantr	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to S \in Ring$
190	150	adantrl	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to F (b) \in K$
191		simpl	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to φ$
192		simprr	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to b \in D$
193		simprl	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to l \in (K^{I})$
194	191 192 193 179	syl21anc	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i)) \in K$
195	6 9 189 190 194	ringcld	$⊢ (φ \land (l \in (K^{I}) \land b \in D)) \to F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))) \in K$
196	187	mptexd	$⊢ φ \to (b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))) \in V$
197		fvexd	$⊢ φ \to 0_{(S ↑_{𝑠} (K^{I}))} \in V$
198		funmpt	$⊢ Fun (b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))))$
199	198	a1i	$⊢ φ \to Fun (b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))))$
200		eqid	$⊢ 0_{U} = 0_{U}$
201	2 3 200 13	mplelsfi	$⊢ φ \to {finSupp}_{0_{U}} (F)$
202		ssidd	$⊢ φ \to F supp 0_{U} \subseteq F supp 0_{U}$
203		fvexd	$⊢ φ \to 0_{U} \in V$
204	149 202 187 203	suppssr	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to F (b) = 0_{U}$
205		eqid	$⊢ 0_{S} = 0_{S}$
206	4 205	subrg0	$⊢ R \in SubRing (S) \to 0_{S} = 0_{U}$
207	12 206	syl	$⊢ φ \to 0_{S} = 0_{U}$
208	207	adantr	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to 0_{S} = 0_{U}$
209	204 208	eqtr4d	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to F (b) = 0_{S}$
210	209	adantr	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to F (b) = 0_{S}$
211	210	oveq1d	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))) = 0_{S} \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))$
212	67	ad2antrr	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to S \in Ring$
213		eldifi	$⊢ b \in (D ∖ {supp}_{0_{U}} (F)) \to b \in D$
214	213 179	sylanl2	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to \underset{i \in I}{\sum_{M}} (b (i) \underset{˙}{\times} l (i)) \in K$
215	6 9 205 212 214	ringlzd	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to 0_{S} \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))) = 0_{S}$
216	211 215	eqtrd	$⊢ ((φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \land l \in (K^{I})) \to F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))) = 0_{S}$
217	216	mpteq2dva	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))) = (l \in (K^{I}) ⟼ 0_{S})$
218		fconstmpt	$⊢ (K^{I}) \times \{0_{S}\} = (l \in (K^{I}) ⟼ 0_{S})$
219	188	cmnmndd	$⊢ φ \to S \in Mnd$
220	22 205	pws0g	$⊢ (S \in Mnd \land K^{I} \in V) \to (K^{I}) \times \{0_{S}\} = 0_{(S ↑_{𝑠} (K^{I}))}$
221	219 68 220	syl2anc	$⊢ φ \to (K^{I}) \times \{0_{S}\} = 0_{(S ↑_{𝑠} (K^{I}))}$
222	218 221	eqtr3id	$⊢ φ \to (l \in (K^{I}) ⟼ 0_{S}) = 0_{(S ↑_{𝑠} (K^{I}))}$
223	222	adantr	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to (l \in (K^{I}) ⟼ 0_{S}) = 0_{(S ↑_{𝑠} (K^{I}))}$
224	217 223	eqtrd	$⊢ (φ \land b \in (D ∖ {supp}_{0_{U}} (F))) \to (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))) = 0_{(S ↑_{𝑠} (K^{I}))}$
225	224 187	suppss2	$⊢ φ \to (b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))) supp 0_{(S ↑_{𝑠} (K^{I}))} \subseteq F supp 0_{U}$
226	196 197 199 201 225	fsuppsssuppgd	$⊢ φ \to {finSupp}_{0_{(S ↑_{𝑠} (K^{I}))}} ((b \in D ⟼ (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i))))))$
227	22 6 185 68 187 188 195 226	pwsgsum	$⊢ φ \to \underset{b \in D}{\sum_{S ↑_{𝑠} (K^{I})}} (l \in (K^{I}) ⟼ F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))) = (l \in (K^{I}) ⟼ \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))))$
228	28 184 227	3eqtrd	$⊢ φ \to Q (F) = (l \in (K^{I}) ⟼ \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} l (i)))))$
229		ovexd	$⊢ φ \to \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i)))) \in V$
230	21 228 14 229	fvmptd4	$⊢ φ \to Q (F) (A) = \underset{b \in D}{\sum_{S}} (F (b) \underset{˙}{\cdot} (\underset{i \in I}{\sum_{M}}, (b (i) \underset{˙}{\times} A (i))))$

Metamath Proof Explorer

Theorem evlsvvval

Proof