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