gsumzf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 2-Jun-2019)

	Ref	Expression
Hypotheses	gsumzcl.b	$⊢ B = {Base}_{G}$
	gsumzcl.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumzcl.z	$⊢ Z = Cntz (G)$
	gsumzcl.g	$⊢ φ \to G \in Mnd$
	gsumzcl.a	$⊢ φ \to A \in V$
	gsumzcl.f	$⊢ φ \to F : A ⟶ B$
	gsumzcl.c	$⊢ φ \to ran F \subseteq Z (ran F)$
	gsumzcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumzf1o.h	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
Assertion	gsumzf1o	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$

Proof

Step	Hyp	Ref	Expression
1		gsumzcl.b	$⊢ B = {Base}_{G}$
2		gsumzcl.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumzcl.z	$⊢ Z = Cntz (G)$
4		gsumzcl.g	$⊢ φ \to G \in Mnd$
5		gsumzcl.a	$⊢ φ \to A \in V$
6		gsumzcl.f	$⊢ φ \to F : A ⟶ B$
7		gsumzcl.c	$⊢ φ \to ran F \subseteq Z (ran F)$
8		gsumzcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
9		gsumzf1o.h	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
10	2	gsumz	$⊢ (G \in Mnd \land A \in V) \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
11	4 5 10	syl2anc	$⊢ φ \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
12		f1of1	$⊢ H : C \underset{1-1 onto}{⟶} A \to H : C \underset{1-1}{⟶} A$
13	9 12	syl	$⊢ φ \to H : C \underset{1-1}{⟶} A$
14		f1dmex	$⊢ (H : C \underset{1-1}{⟶} A \land A \in V) \to C \in V$
15	13 5 14	syl2anc	$⊢ φ \to C \in V$
16	2	gsumz	$⊢ (G \in Mnd \land C \in V) \to \underset{x \in C}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
17	4 15 16	syl2anc	$⊢ φ \to \underset{x \in C}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
18	11 17	eqtr4d	$⊢ φ \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{x \in C}{\sum_{G}} \underset{˙}{0}$
19	18	adantr	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to \underset{k \in A}{\sum_{G}} \underset{˙}{0} = \underset{x \in C}{\sum_{G}} \underset{˙}{0}$
20	2	fvexi	$⊢ \underset{˙}{0} \in V$
21	20	a1i	$⊢ φ \to \underset{˙}{0} \in V$
22		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
23	6 5 21 22	gsumcllem	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to F = (k \in A ⟼ \underset{˙}{0})$
24	23	oveq2d	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to \sum_{G} F = \underset{k \in A}{\sum_{G}} \underset{˙}{0}$
25		f1of	$⊢ H : C \underset{1-1 onto}{⟶} A \to H : C ⟶ A$
26	9 25	syl	$⊢ φ \to H : C ⟶ A$
27	26	adantr	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to H : C ⟶ A$
28	27	ffvelrnda	$⊢ ((φ \land F supp \underset{˙}{0} = \emptyset) \land x \in C) \to H (x) \in A$
29	27	feqmptd	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to H = (x \in C ⟼ H (x))$
30		eqidd	$⊢ k = H (x) \to \underset{˙}{0} = \underset{˙}{0}$
31	28 29 23 30	fmptco	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to F \circ H = (x \in C ⟼ \underset{˙}{0})$
32	31	oveq2d	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to \sum_{G} (F \circ H) = \underset{x \in C}{\sum_{G}} \underset{˙}{0}$
33	19 24 32	3eqtr4d	$⊢ (φ \land F supp \underset{˙}{0} = \emptyset) \to \sum_{G} F = \sum_{G} (F \circ H)$
34	33	ex	$⊢ φ \to (F supp \underset{˙}{0} = \emptyset \to \sum_{G} F = \sum_{G} (F \circ H))$
35		coass	$⊢ (H \circ H^{-1}) \circ f = H \circ (H^{-1} \circ f)$
36	9	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to H : C \underset{1-1 onto}{⟶} A$
37		f1ococnv2	$⊢ H : C \underset{1-1 onto}{⟶} A \to H \circ H^{-1} = {I ↾}_{A}$
38	36 37	syl	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to H \circ H^{-1} = {I ↾}_{A}$
39	38	coeq1d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to (H \circ H^{-1}) \circ f = ({I ↾}_{A}) \circ f$
40		f1of1	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \to f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} F supp \underset{˙}{0}$
41	40	ad2antll	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} F supp \underset{˙}{0}$
42		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
43	42 6	fssdm	$⊢ φ \to F supp \underset{˙}{0} \subseteq A$
44	43	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F supp \underset{˙}{0} \subseteq A$
45		f1ss	$⊢ (f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} F supp \underset{˙}{0} \land F supp \underset{˙}{0} \subseteq A) \to f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} A$
46	41 44 45	syl2anc	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} A$
47		f1f	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} A \to f : (1 \dots \|F supp \underset{˙}{0}\|) ⟶ A$
48		fcoi2	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) ⟶ A \to ({I ↾}_{A}) \circ f = f$
49	46 47 48	3syl	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to ({I ↾}_{A}) \circ f = f$
50	39 49	eqtrd	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to (H \circ H^{-1}) \circ f = f$
51	35 50	syl5reqr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to f = H \circ (H^{-1} \circ f)$
52	51	coeq2d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F \circ f = F \circ (H \circ (H^{-1} \circ f))$
53		coass	$⊢ (F \circ H) \circ (H^{-1} \circ f) = F \circ (H \circ (H^{-1} \circ f))$
54	52 53	syl6eqr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F \circ f = (F \circ H) \circ (H^{-1} \circ f)$
55	54	seqeq3d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to seq 1 (+_{G}, (F \circ f)) = seq 1 (+_{G}, ((F \circ H) \circ (H^{-1} \circ f)))$
56	55	fveq1d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to seq 1 (+_{G}, (F \circ f)) (\|F supp \underset{˙}{0}\|) = seq 1 (+_{G}, ((F \circ H) \circ (H^{-1} \circ f))) (\|F supp \underset{˙}{0}\|)$
57		eqid	$⊢ +_{G} = +_{G}$
58	4	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to G \in Mnd$
59	5	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to A \in V$
60	6	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F : A ⟶ B$
61	7	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to ran F \subseteq Z (ran F)$
62		simprl	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to \|F supp \underset{˙}{0}\| \in ℕ$
63		ssid	$⊢ F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
64		f1ofo	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \to f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{onto}{⟶} F supp \underset{˙}{0}$
65		forn	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{onto}{⟶} F supp \underset{˙}{0} \to ran f = F supp \underset{˙}{0}$
66	64 65	syl	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \to ran f = F supp \underset{˙}{0}$
67	66	ad2antll	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to ran f = F supp \underset{˙}{0}$
68	63 67	sseqtrrid	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F supp \underset{˙}{0} \subseteq ran f$
69		eqid	$⊢ (F \circ f) supp \underset{˙}{0} = (F \circ f) supp \underset{˙}{0}$
70	1 2 57 3 58 59 60 61 62 46 68 69	gsumval3	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to \sum_{G} F = seq 1 (+_{G}, (F \circ f)) (\|F supp \underset{˙}{0}\|)$
71	15	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to C \in V$
72		fco	$⊢ (F : A ⟶ B \land H : C ⟶ A) \to (F \circ H) : C ⟶ B$
73	6 26 72	syl2anc	$⊢ φ \to (F \circ H) : C ⟶ B$
74	73	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to (F \circ H) : C ⟶ B$
75		rncoss	$⊢ ran (F \circ H) \subseteq ran F$
76	3	cntzidss	$⊢ (ran F \subseteq Z (ran F) \land ran (F \circ H) \subseteq ran F) \to ran (F \circ H) \subseteq Z (ran (F \circ H))$
77	7 75 76	sylancl	$⊢ φ \to ran (F \circ H) \subseteq Z (ran (F \circ H))$
78	77	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to ran (F \circ H) \subseteq Z (ran (F \circ H))$
79		f1ocnv	$⊢ H : C \underset{1-1 onto}{⟶} A \to H^{-1} : A \underset{1-1 onto}{⟶} C$
80		f1of1	$⊢ H^{-1} : A \underset{1-1 onto}{⟶} C \to H^{-1} : A \underset{1-1}{⟶} C$
81	9 79 80	3syl	$⊢ φ \to H^{-1} : A \underset{1-1}{⟶} C$
82	81	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to H^{-1} : A \underset{1-1}{⟶} C$
83		f1co	$⊢ (H^{-1} : A \underset{1-1}{⟶} C \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} A) \to (H^{-1} \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} C$
84	82 46 83	syl2anc	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to (H^{-1} \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} C$
85		ssidd	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
86		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
87	6 5 86	syl2anc	$⊢ φ \to F \in V$
88		suppimacnv	$⊢ (F \in V \land \underset{˙}{0} \in V) \to F supp \underset{˙}{0} = F^{-1} [V ∖ \{\underset{˙}{0}\}]$
89	87 20 88	sylancl	$⊢ φ \to F supp \underset{˙}{0} = F^{-1} [V ∖ \{\underset{˙}{0}\}]$
90	89	eqcomd	$⊢ φ \to F^{-1} [V ∖ \{\underset{˙}{0}\}] = F supp \underset{˙}{0}$
91	90	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F^{-1} [V ∖ \{\underset{˙}{0}\}] = F supp \underset{˙}{0}$
92	85 91 67	3sstr4d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to F^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran f$
93		imass2	$⊢ F^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran f \to H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]] \subseteq H^{-1} [ran f]$
94	92 93	syl	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]] \subseteq H^{-1} [ran f]$
95		cnvco	$⊢ {(F \circ H)}^{-1} = H^{-1} \circ F^{-1}$
96	95	imaeq1i	$⊢ {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] = (H^{-1} \circ F^{-1}) [V ∖ \{\underset{˙}{0}\}]$
97		imaco	$⊢ (H^{-1} \circ F^{-1}) [V ∖ \{\underset{˙}{0}\}] = H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]]$
98	96 97	eqtri	$⊢ {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] = H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]]$
99		rnco2	$⊢ ran (H^{-1} \circ f) = H^{-1} [ran f]$
100	94 98 99	3sstr4g	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran (H^{-1} \circ f)$
101		f1oexrnex	$⊢ (H : C \underset{1-1 onto}{⟶} A \land A \in V) \to H \in V$
102	9 5 101	syl2anc	$⊢ φ \to H \in V$
103		coexg	$⊢ (F \in V \land H \in V) \to F \circ H \in V$
104	87 102 103	syl2anc	$⊢ φ \to F \circ H \in V$
105		suppimacnv	$⊢ (F \circ H \in V \land \underset{˙}{0} \in V) \to (F \circ H) supp \underset{˙}{0} = {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
106	104 20 105	sylancl	$⊢ φ \to (F \circ H) supp \underset{˙}{0} = {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
107	106	sseq1d	$⊢ φ \to ((F \circ H) supp \underset{˙}{0} \subseteq ran (H^{-1} \circ f) \leftrightarrow {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran (H^{-1} \circ f))$
108	107	adantr	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to ((F \circ H) supp \underset{˙}{0} \subseteq ran (H^{-1} \circ f) \leftrightarrow {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran (H^{-1} \circ f))$
109	100 108	mpbird	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to (F \circ H) supp \underset{˙}{0} \subseteq ran (H^{-1} \circ f)$
110		eqid	$⊢ ((F \circ H) \circ (H^{-1} \circ f)) supp \underset{˙}{0} = ((F \circ H) \circ (H^{-1} \circ f)) supp \underset{˙}{0}$
111	1 2 57 3 58 71 74 78 62 84 109 110	gsumval3	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to \sum_{G} (F \circ H) = seq 1 (+_{G}, ((F \circ H) \circ (H^{-1} \circ f))) (\|F supp \underset{˙}{0}\|)$
112	56 70 111	3eqtr4d	$⊢ (φ \land (\|F supp \underset{˙}{0}\| \in ℕ \land f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})) \to \sum_{G} F = \sum_{G} (F \circ H)$
113	112	expr	$⊢ (φ \land \|F supp \underset{˙}{0}\| \in ℕ) \to (f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \to \sum_{G} F = \sum_{G} (F \circ H))$
114	113	exlimdv	$⊢ (φ \land \|F supp \underset{˙}{0}\| \in ℕ) \to (\exists f f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \to \sum_{G} F = \sum_{G} (F \circ H))$
115	114	expimpd	$⊢ φ \to ((\|F supp \underset{˙}{0}\| \in ℕ \land \exists f f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}) \to \sum_{G} F = \sum_{G} (F \circ H))$
116		fsuppimp	$⊢ {finSupp}_{\underset{˙}{0}} (F) \to (Fun F \land F supp \underset{˙}{0} \in Fin)$
117	116	simprd	$⊢ {finSupp}_{\underset{˙}{0}} (F) \to F supp \underset{˙}{0} \in Fin$
118		fz1f1o	$⊢ F supp \underset{˙}{0} \in Fin \to (F supp \underset{˙}{0} = \emptyset \lor (\|F supp \underset{˙}{0}\| \in ℕ \land \exists f f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}))$
119	8 117 118	3syl	$⊢ φ \to (F supp \underset{˙}{0} = \emptyset \lor (\|F supp \underset{˙}{0}\| \in ℕ \land \exists f f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}))$
120	34 115 119	mpjaod	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$

Metamath Proof Explorer

Theorem gsumzf1o

Proof