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	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$
36		f1ococnv2	$⊢ H : C \underset{1-1 onto}{⟶} A \to H \circ H^{-1} = {I ↾}_{A}$
37	35 36	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}$
38	37	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$
39		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}$
40	39	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}$
41		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
42	41 6	fssdm	$⊢ φ \to F supp \underset{˙}{0} \subseteq A$
43	42	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$
44		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$
45	40 43 44	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$
46		f1f	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1}{⟶} A \to f : (1 \dots \|F supp \underset{˙}{0}\|) ⟶ A$
47		fcoi2	$⊢ f : (1 \dots \|F supp \underset{˙}{0}\|) ⟶ A \to ({I ↾}_{A}) \circ f = f$
48	45 46 47	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$
49	38 48	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$
50		coass	$⊢ (H \circ H^{-1}) \circ f = H \circ (H^{-1} \circ f)$
51	49 50	eqtr3di	$⊢ (φ \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	eqtr4di	$⊢ (φ \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 45 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 45 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	6 5	fexd	$⊢ φ \to F \in V$
87		suppimacnv	$⊢ (F \in V \land \underset{˙}{0} \in V) \to F supp \underset{˙}{0} = F^{-1} [V ∖ \{\underset{˙}{0}\}]$
88	86 20 87	sylancl	$⊢ φ \to F supp \underset{˙}{0} = F^{-1} [V ∖ \{\underset{˙}{0}\}]$
89	88	eqcomd	$⊢ φ \to F^{-1} [V ∖ \{\underset{˙}{0}\}] = F supp \underset{˙}{0}$
90	89	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}$
91	85 90 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$
92		imass2	$⊢ F^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran f \to H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]] \subseteq H^{-1} [ran f]$
93	91 92	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]$
94		cnvco	$⊢ {(F \circ H)}^{-1} = H^{-1} \circ F^{-1}$
95	94	imaeq1i	$⊢ {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] = (H^{-1} \circ F^{-1}) [V ∖ \{\underset{˙}{0}\}]$
96		imaco	$⊢ (H^{-1} \circ F^{-1}) [V ∖ \{\underset{˙}{0}\}] = H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]]$
97	95 96	eqtri	$⊢ {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}] = H^{-1} [F^{-1} [V ∖ \{\underset{˙}{0}\}]]$
98		rnco2	$⊢ ran (H^{-1} \circ f) = H^{-1} [ran f]$
99	93 97 98	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)$
100		f1oexrnex	$⊢ (H : C \underset{1-1 onto}{⟶} A \land A \in V) \to H \in V$
101	9 5 100	syl2anc	$⊢ φ \to H \in V$
102		coexg	$⊢ (F \in V \land H \in V) \to F \circ H \in V$
103	86 101 102	syl2anc	$⊢ φ \to F \circ H \in V$
104		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}\}]$
105	103 20 104	sylancl	$⊢ φ \to (F \circ H) supp \underset{˙}{0} = {(F \circ H)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
106	105	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))$
107	106	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))$
108	99 107	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)$
109		eqid	$⊢ ((F \circ H) \circ (H^{-1} \circ f)) supp \underset{˙}{0} = ((F \circ H) \circ (H^{-1} \circ f)) supp \underset{˙}{0}$
110	1 2 57 3 58 71 74 78 62 84 108 109	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}\|)$
111	56 70 110	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)$
112	111	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))$
113	112	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))$
114	113	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))$
115		fsuppimp	$⊢ {finSupp}_{\underset{˙}{0}} (F) \to (Fun F \land F supp \underset{˙}{0} \in Fin)$
116	115	simprd	$⊢ {finSupp}_{\underset{˙}{0}} (F) \to F supp \underset{˙}{0} \in Fin$
117		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}))$
118	8 116 117	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}))$
119	34 114 118	mpjaod	$⊢ φ \to \sum_{G} F = \sum_{G} (F \circ H)$

Metamath Proof Explorer

Theorem gsumzf1o

Proof