psrmonprod

Description: Finite product of bags of variables in a power series. Here the function G maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrmonprod.s	$⊢ S = I mPwSer R$
	psrmonprod.b	$⊢ B = {Base}_{S}$
	psrmonprod.r	$⊢ φ \to R \in CRing$
	psrmonprod.i	$⊢ φ \to I \in V$
	psrmonprod.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	psrmonprod.a	$⊢ φ \to A \in Fin$
	psrmonprod.f	$⊢ φ \to F : A ⟶ D$
	psrmonprod.1	$⊢ \underset{˙}{1} = 1_{R}$
	psrmonprod.0	$⊢ \underset{˙}{0} = 0_{R}$
	psrmonprod.m	$⊢ M = {mulGrp}_{S}$
	psrmonprod.g	$⊢ G = (y \in D ⟼ (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})))$
Assertion	psrmonprod	$⊢ φ \to \sum_{M} (G \circ F) = G ((i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i)))$

Proof

Step	Hyp	Ref	Expression
1		psrmonprod.s	$⊢ S = I mPwSer R$
2		psrmonprod.b	$⊢ B = {Base}_{S}$
3		psrmonprod.r	$⊢ φ \to R \in CRing$
4		psrmonprod.i	$⊢ φ \to I \in V$
5		psrmonprod.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
6		psrmonprod.a	$⊢ φ \to A \in Fin$
7		psrmonprod.f	$⊢ φ \to F : A ⟶ D$
8		psrmonprod.1	$⊢ \underset{˙}{1} = 1_{R}$
9		psrmonprod.0	$⊢ \underset{˙}{0} = 0_{R}$
10		psrmonprod.m	$⊢ M = {mulGrp}_{S}$
11		psrmonprod.g	$⊢ G = (y \in D ⟼ (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})))$
12	7	ffvelcdmda	$⊢ (φ \land k \in A) \to F (k) \in D$
13	7	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
14		fvexd	$⊢ (φ \land y \in D) \to {Base}_{R} \in V$
15		ovex	$⊢ {ℕ_{0}}^{I} \in V$
16	5 15	rabex2	$⊢ D \in V$
17	16	a1i	$⊢ (φ \land y \in D) \to D \in V$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19	3	crngringd	$⊢ φ \to R \in Ring$
20	18 8 19	ringidcld	$⊢ φ \to \underset{˙}{1} \in {Base}_{R}$
21	20	ad2antrr	$⊢ ((φ \land y \in D) \land z \in D) \to \underset{˙}{1} \in {Base}_{R}$
22	3	crnggrpd	$⊢ φ \to R \in Grp$
23	18 9 22	grpidcld	$⊢ φ \to \underset{˙}{0} \in {Base}_{R}$
24	23	ad2antrr	$⊢ ((φ \land y \in D) \land z \in D) \to \underset{˙}{0} \in {Base}_{R}$
25	21 24	ifcld	$⊢ ((φ \land y \in D) \land z \in D) \to if (z = y, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{R}$
26	25	fmpttd	$⊢ (φ \land y \in D) \to (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})) : D ⟶ {Base}_{R}$
27	14 17 26	elmapdd	$⊢ (φ \land y \in D) \to (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})) \in ({Base}_{R}^{D})$
28	5	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
29	1 18 28 2 4	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
30	29	adantr	$⊢ (φ \land y \in D) \to B = {Base}_{R}^{D}$
31	27 30	eleqtrrd	$⊢ (φ \land y \in D) \to (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})) \in B$
32	31 11	fmptd	$⊢ φ \to G : D ⟶ B$
33	32	feqmptd	$⊢ φ \to G = (y \in D ⟼ G (y))$
34		fveq2	$⊢ y = F (k) \to G (y) = G (F (k))$
35	12 13 33 34	fmptco	$⊢ φ \to G \circ F = (k \in A ⟼ G (F (k)))$
36	35	oveq2d	$⊢ φ \to \sum_{M} (G \circ F) = \underset{k \in A}{\sum_{M}} G (F (k))$
37		mpteq1	$⊢ a = \emptyset \to (k \in a ⟼ G (F (k))) = (k \in \emptyset ⟼ G (F (k)))$
38	37	oveq2d	$⊢ a = \emptyset \to \underset{k \in a}{\sum_{M}} G (F (k)) = \underset{k \in \emptyset}{\sum_{M}} G (F (k))$
39		mpteq1	$⊢ a = \emptyset \to (x \in a ⟼ F (x) (i)) = (x \in \emptyset ⟼ F (x) (i))$
40	39	oveq2d	$⊢ a = \emptyset \to \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)$
41	40	mpteq2dv	$⊢ a = \emptyset \to (i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))$
42	41	fveq2d	$⊢ a = \emptyset \to G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) = G ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)))$
43	38 42	eqeq12d	$⊢ a = \emptyset \to (\underset{k \in a}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) \leftrightarrow \underset{k \in \emptyset}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))))$
44		mpteq1	$⊢ a = b \to (k \in a ⟼ G (F (k))) = (k \in b ⟼ G (F (k)))$
45	44	oveq2d	$⊢ a = b \to \underset{k \in a}{\sum_{M}} G (F (k)) = \underset{k \in b}{\sum_{M}} G (F (k))$
46		mpteq1	$⊢ a = b \to (x \in a ⟼ F (x) (i)) = (x \in b ⟼ F (x) (i))$
47	46	oveq2d	$⊢ a = b \to \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)$
48	47	mpteq2dv	$⊢ a = b \to (i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))$
49	48	fveq2d	$⊢ a = b \to G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))$
50	45 49	eqeq12d	$⊢ a = b \to (\underset{k \in a}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) \leftrightarrow \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))))$
51		mpteq1	$⊢ a = b \cup \{f\} \to (k \in a ⟼ G (F (k))) = (k \in (b \cup \{f\}) ⟼ G (F (k)))$
52	51	oveq2d	$⊢ a = b \cup \{f\} \to \underset{k \in a}{\sum_{M}} G (F (k)) = \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k))$
53		mpteq1	$⊢ a = b \cup \{f\} \to (x \in a ⟼ F (x) (i)) = (x \in (b \cup \{f\}) ⟼ F (x) (i))$
54	53	oveq2d	$⊢ a = b \cup \{f\} \to \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)$
55	54	mpteq2dv	$⊢ a = b \cup \{f\} \to (i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))$
56	55	fveq2d	$⊢ a = b \cup \{f\} \to G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
57	52 56	eqeq12d	$⊢ a = b \cup \{f\} \to (\underset{k \in a}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) \leftrightarrow \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))))$
58		mpteq1	$⊢ a = A \to (k \in a ⟼ G (F (k))) = (k \in A ⟼ G (F (k)))$
59	58	oveq2d	$⊢ a = A \to \underset{k \in a}{\sum_{M}} G (F (k)) = \underset{k \in A}{\sum_{M}} G (F (k))$
60		mpteq1	$⊢ a = A \to (x \in a ⟼ F (x) (i)) = (x \in A ⟼ F (x) (i))$
61	60	oveq2d	$⊢ a = A \to \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i)$
62	61	mpteq2dv	$⊢ a = A \to (i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i))$
63	62	fveq2d	$⊢ a = A \to G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) = G ((i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i)))$
64	59 63	eqeq12d	$⊢ a = A \to (\underset{k \in a}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in a}{\sum_{ℂ_{fld}}} F (x) (i))) \leftrightarrow \underset{k \in A}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i))))$
65		eqid	$⊢ 1_{S} = 1_{S}$
66	10 65	ringidval	$⊢ 1_{S} = 0_{M}$
67	66	gsum0	$⊢ \sum_{M} \emptyset = 1_{S}$
68		mpt0	$⊢ (k \in \emptyset ⟼ G (F (k))) = \emptyset$
69	68	oveq2i	$⊢ \underset{k \in \emptyset}{\sum_{M}} G (F (k)) = \sum_{M} \emptyset$
70	69	a1i	$⊢ φ \to \underset{k \in \emptyset}{\sum_{M}} G (F (k)) = \sum_{M} \emptyset$
71		mpt0	$⊢ (x \in \emptyset ⟼ F (x) (i)) = \emptyset$
72	71	oveq2i	$⊢ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i) = \sum_{ℂ_{fld}} \emptyset$
73		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
74	73	gsum0	$⊢ \sum_{ℂ_{fld}} \emptyset = 0$
75	72 74	eqtri	$⊢ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i) = 0$
76	75	mpteq2i	$⊢ (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ 0)$
77		fconstmpt	$⊢ I \times \{0\} = (i \in I ⟼ 0)$
78	76 77	eqtr4i	$⊢ (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) = I \times \{0\}$
79	78	a1i	$⊢ φ \to (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) = I \times \{0\}$
80	79	eqeq2d	$⊢ φ \to (y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) \leftrightarrow y = I \times \{0\})$
81	80	biimpa	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to y = I \times \{0\}$
82	81	eqeq2d	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to (z = y \leftrightarrow z = I \times \{0\})$
83	82	ifbid	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to if (z = y, \underset{˙}{1}, \underset{˙}{0}) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
84	83	mpteq2dv	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})) = (z \in D ⟼ if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
85	1 4 19 28 9 8 65	psr1	$⊢ φ \to 1_{S} = (z \in D ⟼ if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
86	85	adantr	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to 1_{S} = (z \in D ⟼ if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
87	84 86	eqtr4d	$⊢ (φ \land y = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) \to (z \in D ⟼ if (z = y, \underset{˙}{1}, \underset{˙}{0})) = 1_{S}$
88		breq1	$⊢ h = (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))))$
89		nn0ex	$⊢ ℕ_{0} \in V$
90	89	a1i	$⊢ φ \to ℕ_{0} \in V$
91		0nn0	$⊢ 0 \in ℕ_{0}$
92	91	fconst6	$⊢ (I \times \{0\}) : I ⟶ ℕ_{0}$
93	92	a1i	$⊢ φ \to (I \times \{0\}) : I ⟶ ℕ_{0}$
94	90 4 93	elmapdd	$⊢ φ \to I \times \{0\} \in ({ℕ_{0}}^{I})$
95	78 94	eqeltrid	$⊢ φ \to (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) \in ({ℕ_{0}}^{I})$
96	91	a1i	$⊢ φ \to 0 \in ℕ_{0}$
97	4 96	fczfsuppd	$⊢ φ \to {finSupp}_{0} ((I \times \{0\}))$
98	78 97	eqbrtrid	$⊢ φ \to {finSupp}_{0} ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)))$
99	88 95 98	elrabd	$⊢ φ \to (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
100	99 5	eleqtrrdi	$⊢ φ \to (i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)) \in D$
101		fvexd	$⊢ φ \to 1_{S} \in V$
102	11 87 100 101	fvmptd2	$⊢ φ \to G ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i))) = 1_{S}$
103	67 70 102	3eqtr4a	$⊢ φ \to \underset{k \in \emptyset}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in \emptyset}{\sum_{ℂ_{fld}}} F (x) (i)))$
104		2fveq3	$⊢ k = l \to G (F (k)) = G (F (l))$
105	104	cbvmptv	$⊢ (k \in (b \cup \{f\}) ⟼ G (F (k))) = (l \in (b \cup \{f\}) ⟼ G (F (l)))$
106	105	oveq2i	$⊢ \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k)) = \underset{l \in b \cup \{f\}}{\sum_{M}} G (F (l))$
107	10 2	mgpbas	$⊢ B = {Base}_{M}$
108		eqid	$⊢ \cdot_{S} = \cdot_{S}$
109	10 108	mgpplusg	$⊢ \cdot_{S} = +_{M}$
110	1 4 3	psrcrng	$⊢ φ \to S \in CRing$
111	10	crngmgp	$⊢ S \in CRing \to M \in CMnd$
112	110 111	syl	$⊢ φ \to M \in CMnd$
113	112	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to M \in CMnd$
114	6	adantr	$⊢ (φ \land b \subseteq A) \to A \in Fin$
115		simpr	$⊢ (φ \land b \subseteq A) \to b \subseteq A$
116	114 115	ssfid	$⊢ (φ \land b \subseteq A) \to b \in Fin$
117	116	ad2antrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to b \in Fin$
118	32	ad4antr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \land l \in b) \to G : D ⟶ B$
119	7	ad4antr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \land l \in b) \to F : A ⟶ D$
120		simpllr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to b \subseteq A$
121	120	sselda	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \land l \in b) \to l \in A$
122	119 121	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \land l \in b) \to F (l) \in D$
123	118 122	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \land l \in b) \to G (F (l)) \in B$
124		simplr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to f \in (A ∖ b)$
125	124	eldifbd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to \neg f \in b$
126	32	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to G : D ⟶ B$
127	7	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to F : A ⟶ D$
128	124	eldifad	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to f \in A$
129	127 128	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to F (f) \in D$
130	126 129	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to G (F (f)) \in B$
131		2fveq3	$⊢ l = f \to G (F (l)) = G (F (f))$
132	107 109 113 117 123 124 125 130 131	gsumunsn	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to \underset{l \in b \cup \{f\}}{\sum_{M}} G (F (l)) = (\underset{l \in b}{\sum_{M}}, G (F (l))) \cdot_{S} G (F (f))$
133	104	cbvmptv	$⊢ (k \in b ⟼ G (F (k))) = (l \in b ⟼ G (F (l)))$
134	133	oveq2i	$⊢ \underset{k \in b}{\sum_{M}} G (F (k)) = \underset{l \in b}{\sum_{M}} G (F (l))$
135		id	$⊢ \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \to \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))$
136	134 135	eqtr3id	$⊢ \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \to \underset{l \in b}{\sum_{M}} G (F (l)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))$
137	136	oveq1d	$⊢ \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \to (\underset{l \in b}{\sum_{M}}, G (F (l))) \cdot_{S} G (F (f)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \cdot_{S} G (F (f))$
138	137	adantl	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to (\underset{l \in b}{\sum_{M}}, G (F (l))) \cdot_{S} G (F (f)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \cdot_{S} G (F (f))$
139	4	ad2antrr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to I \in V$
140	19	ad2antrr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to R \in Ring$
141		breq1	$⊢ h = (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))))$
142	89	a1i	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to ℕ_{0} \in V$
143		cnfldfld	$⊢ ℂ_{fld} \in Field$
144		id	$⊢ ℂ_{fld} \in Field \to ℂ_{fld} \in Field$
145	144	fldcrngd	$⊢ ℂ_{fld} \in Field \to ℂ_{fld} \in CRing$
146		crngring	$⊢ ℂ_{fld} \in CRing \to ℂ_{fld} \in Ring$
147		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
148	145 146 147	3syl	$⊢ ℂ_{fld} \in Field \to ℂ_{fld} \in CMnd$
149	143 148	ax-mp	$⊢ ℂ_{fld} \in CMnd$
150	149	a1i	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to ℂ_{fld} \in CMnd$
151	116	ad2antrr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to b \in Fin$
152		nn0subm	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
153	152	a1i	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to ℕ_{0} \in SubMnd (ℂ_{fld})$
154	5	ssrab3	$⊢ D \subseteq {ℕ_{0}}^{I}$
155	7	ad2antrr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F : A ⟶ D$
156	155	ad2antrr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to F : A ⟶ D$
157		simpllr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to b \subseteq A$
158	157	sselda	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to x \in A$
159	156 158	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to F (x) \in D$
160	154 159	sselid	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to F (x) \in ({ℕ_{0}}^{I})$
161	160	elmaprd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to F (x) : I ⟶ ℕ_{0}$
162		simplr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to i \in I$
163	161 162	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \land x \in b) \to F (x) (i) \in ℕ_{0}$
164	163	fmpttd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to (x \in b ⟼ F (x) (i)) : b ⟶ ℕ_{0}$
165	91	a1i	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to 0 \in ℕ_{0}$
166	164 151 165	fdmfifsupp	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to {finSupp}_{0} ((x \in b ⟼ F (x) (i)))$
167	73 150 151 153 164 166	gsumsubmcl	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i) \in ℕ_{0}$
168	167	fmpttd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) : I ⟶ ℕ_{0}$
169	142 139 168	elmapdd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) \in ({ℕ_{0}}^{I})$
170	91	a1i	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to 0 \in ℕ_{0}$
171	168	ffund	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to Fun (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))$
172	116	adantr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to b \in Fin$
173	155	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F : A ⟶ D$
174		simplr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to b \subseteq A$
175	174	sselda	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to x \in A$
176	173 175	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) \in D$
177	154 176	sselid	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) \in ({ℕ_{0}}^{I})$
178	177	elmaprd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) : I ⟶ ℕ_{0}$
179	178	feqmptd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) = (i \in I ⟼ F (x) (i))$
180	179	oveq1d	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) supp 0 = (i \in I ⟼ F (x) (i)) supp 0$
181		breq1	$⊢ h = F (x) \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (F (x)))$
182	176 5	eleqtrdi	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
183	181 182	elrabrd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to {finSupp}_{0} (F (x))$
184	183	fsuppimpd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to F (x) supp 0 \in Fin$
185	180 184	eqeltrrd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land x \in b) \to (i \in I ⟼ F (x) (i)) supp 0 \in Fin$
186	185	ralrimiva	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to \forall x \in b (i \in I ⟼ F (x) (i)) supp 0 \in Fin$
187		iunfi	$⊢ (b \in Fin \land \forall x \in b (i \in I ⟼ F (x) (i)) supp 0 \in Fin) \to ⋃_{x \in b} {supp}_{0} ((i \in I ⟼ F (x) (i))) \in Fin$
188	172 186 187	syl2anc	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to ⋃_{x \in b} {supp}_{0} ((i \in I ⟼ F (x) (i))) \in Fin$
189		cmnmnd	$⊢ ℂ_{fld} \in CMnd \to ℂ_{fld} \in Mnd$
190	149 189	ax-mp	$⊢ ℂ_{fld} \in Mnd$
191	190	a1i	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to ℂ_{fld} \in Mnd$
192	114	adantr	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to A \in Fin$
193	192 174	ssexd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to b \in V$
194	73 191 193 139 163	suppgsumssiun	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) supp 0 \subseteq ⋃_{x \in b} {supp}_{0} ((i \in I ⟼ F (x) (i)))$
195	188 194	ssfid	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) supp 0 \in Fin$
196	169 170 171 195	isfsuppd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to {finSupp}_{0} ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))$
197	141 169 196	elrabd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
198	197 5	eleqtrrdi	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) \in D$
199		difssd	$⊢ (φ \land b \subseteq A) \to A ∖ b \subseteq A$
200	199	sselda	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to f \in A$
201	155 200	ffvelcdmd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) \in D$
202	1 2 9 8 5 139 140 198 108 201 11	psrmonmul2	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \cdot_{S} G (F (f)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) +_{f} F (f))$
203	168	ffnd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) Fn I$
204	154 201	sselid	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) \in ({ℕ_{0}}^{I})$
205	204	elmaprd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) : I ⟶ ℕ_{0}$
206	205	ffnd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to F (f) Fn I$
207		nfv	$⊢ Ⅎ i ((φ \land b \subseteq A) \land f \in (A ∖ b))$
208		ovexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land i \in I) \to \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i) \in V$
209		eqid	$⊢ (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))$
210	207 208 209	fnmptd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)) Fn I$
211		eqid	$⊢ (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) = (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))$
212		fveq2	$⊢ i = j \to F (x) (i) = F (x) (j)$
213	212	mpteq2dv	$⊢ i = j \to (x \in b ⟼ F (x) (i)) = (x \in b ⟼ F (x) (j))$
214	213	oveq2d	$⊢ i = j \to \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (j)$
215		simpr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to j \in I$
216		ovexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (j) \in V$
217	211 214 215 216	fvmptd3	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) (j) = \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (j)$
218		eqidd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to F (f) (j) = F (f) (j)$
219	212	mpteq2dv	$⊢ i = j \to (x \in (b \cup \{f\}) ⟼ F (x) (i)) = (x \in (b \cup \{f\}) ⟼ F (x) (j))$
220	219	oveq2d	$⊢ i = j \to \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i) = \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (j)$
221		ovexd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (j) \in V$
222	209 220 215 221	fvmptd3	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)) (j) = \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (j)$
223		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
224		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
225	149	a1i	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to ℂ_{fld} \in CMnd$
226	172	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to b \in Fin$
227	178	adantlr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \land x \in b) \to F (x) : I ⟶ ℕ_{0}$
228		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
229	228	a1i	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \land x \in b) \to ℕ_{0} \subseteq ℂ$
230	227 229	fssd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \land x \in b) \to F (x) : I ⟶ ℂ$
231		simplr	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \land x \in b) \to j \in I$
232	230 231	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \land x \in b) \to F (x) (j) \in ℂ$
233		simplr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to f \in (A ∖ b)$
234	233	eldifbd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to \neg f \in b$
235	205	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to F (f) : I ⟶ ℕ_{0}$
236	228	a1i	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to ℕ_{0} \subseteq ℂ$
237	235 236	fssd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to F (f) : I ⟶ ℂ$
238	237 215	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to F (f) (j) \in ℂ$
239		fveq2	$⊢ x = f \to F (x) = F (f)$
240	239	fveq1d	$⊢ x = f \to F (x) (j) = F (f) (j)$
241	223 224 225 226 232 233 234 238 240	gsumunsn	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (j) = (\underset{x \in b}{\sum_{ℂ_{fld}}}, F (x) (j)) + F (f) (j)$
242	222 241	eqtr2d	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land j \in I) \to (\underset{x \in b}{\sum_{ℂ_{fld}}}, F (x) (j)) + F (f) (j) = (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)) (j)$
243	139 203 206 210 217 218 242	offveq	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) +_{f} F (f) = (i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))$
244	243	fveq2d	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)) +_{f} F (f)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
245	202 244	eqtrd	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \cdot_{S} G (F (f)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
246	245	adantr	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \cdot_{S} G (F (f)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
247	132 138 246	3eqtrd	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to \underset{l \in b \cup \{f\}}{\sum_{M}} G (F (l)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
248	106 247	eqtrid	$⊢ (((φ \land b \subseteq A) \land f \in (A ∖ b)) \land \underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i)))) \to \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i)))$
249	248	ex	$⊢ ((φ \land b \subseteq A) \land f \in (A ∖ b)) \to (\underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \to \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))))$
250	249	anasss	$⊢ (φ \land (b \subseteq A \land f \in (A ∖ b))) \to (\underset{k \in b}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b}{\sum_{ℂ_{fld}}} F (x) (i))) \to \underset{k \in b \cup \{f\}}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in b \cup \{f\}}{\sum_{ℂ_{fld}}} F (x) (i))))$
251	43 50 57 64 103 250 6	findcard2d	$⊢ φ \to \underset{k \in A}{\sum_{M}} G (F (k)) = G ((i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i)))$
252	36 251	eqtrd	$⊢ φ \to \sum_{M} (G \circ F) = G ((i \in I ⟼ \underset{x \in A}{\sum_{ℂ_{fld}}} F (x) (i)))$

Metamath Proof Explorer

Theorem psrmonprod

Proof