gsumval3lem2

	Ref	Expression
Hypotheses	gsumval3.b	$⊢ B = {Base}_{G}$
	gsumval3.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumval3.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumval3.z	$⊢ Z = Cntz (G)$
	gsumval3.g	$⊢ φ \to G \in Mnd$
	gsumval3.a	$⊢ φ \to A \in V$
	gsumval3.f	$⊢ φ \to F : A ⟶ B$
	gsumval3.c	$⊢ φ \to ran F \subseteq Z (ran F)$
	gsumval3.m	$⊢ φ \to M \in ℕ$
	gsumval3.h	$⊢ φ \to H : (1 \dots M) \underset{1-1}{⟶} A$
	gsumval3.n	$⊢ φ \to F supp \underset{˙}{0} \subseteq ran H$
	gsumval3.w	$⊢ W = (F \circ H) supp \underset{˙}{0}$
Assertion	gsumval3lem2	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|)$

Proof

Step	Hyp	Ref	Expression
1		gsumval3.b	$⊢ B = {Base}_{G}$
2		gsumval3.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumval3.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumval3.z	$⊢ Z = Cntz (G)$
5		gsumval3.g	$⊢ φ \to G \in Mnd$
6		gsumval3.a	$⊢ φ \to A \in V$
7		gsumval3.f	$⊢ φ \to F : A ⟶ B$
8		gsumval3.c	$⊢ φ \to ran F \subseteq Z (ran F)$
9		gsumval3.m	$⊢ φ \to M \in ℕ$
10		gsumval3.h	$⊢ φ \to H : (1 \dots M) \underset{1-1}{⟶} A$
11		gsumval3.n	$⊢ φ \to F supp \underset{˙}{0} \subseteq ran H$
12		gsumval3.w	$⊢ W = (F \circ H) supp \underset{˙}{0}$
13		f1f	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) ⟶ A$
14	10 13	syl	$⊢ φ \to H : (1 \dots M) ⟶ A$
15		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
16	14 15	fexd	$⊢ φ \to H \in V$
17		vex	$⊢ f \in V$
18		coexg	$⊢ (H \in V \land f \in V) \to H \circ f \in V$
19	16 17 18	sylancl	$⊢ φ \to H \circ f \in V$
20	19	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H \circ f \in V$
21	1 2 3 4 5 6 7 8 9 10 11 12	gsumval3lem1	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
22		fzfi	$⊢ (1 \dots M) \in Fin$
23		suppssdm	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq dom (F \circ H)$
24	12 23	eqsstri	$⊢ W \subseteq dom (F \circ H)$
25	7 14	fcod	$⊢ φ \to (F \circ H) : (1 \dots M) ⟶ B$
26	24 25	fssdm	$⊢ φ \to W \subseteq (1 \dots M)$
27		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
28	22 26 27	sylancr	$⊢ φ \to W \in Fin$
29	28	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \in Fin$
30	10	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H : (1 \dots M) \underset{1-1}{⟶} A$
31	26	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \subseteq (1 \dots M)$
32		f1ores	$⊢ (H : (1 \dots M) \underset{1-1}{⟶} A \land W \subseteq (1 \dots M)) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W]$
33	30 31 32	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W]$
34	12	imaeq2i	$⊢ H [W] = H [(F \circ H) supp \underset{˙}{0}]$
35	7 6	fexd	$⊢ φ \to F \in V$
36		ovex	$⊢ (1 \dots M) \in V$
37		fex	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to H \in V$
38	14 36 37	sylancl	$⊢ φ \to H \in V$
39	35 38	jca	$⊢ φ \to (F \in V \land H \in V)$
40		f1fun	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to Fun H$
41	10 40	syl	$⊢ φ \to Fun H$
42	41 11	jca	$⊢ φ \to (Fun H \land F supp \underset{˙}{0} \subseteq ran H)$
43		imacosupp	$⊢ (F \in V \land H \in V) \to ((Fun H \land F supp \underset{˙}{0} \subseteq ran H) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0})$
44	39 42 43	sylc	$⊢ φ \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
45	44	adantr	$⊢ (φ \land W \neq \emptyset) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
46	34 45	syl5eq	$⊢ (φ \land W \neq \emptyset) \to H [W] = F supp \underset{˙}{0}$
47	46	adantr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H [W] = F supp \underset{˙}{0}$
48	47	f1oeq3d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (({H ↾}_{W}) : W \underset{1-1 onto}{⟶} H [W] \leftrightarrow ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
49	33 48	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ({H ↾}_{W}) : W \underset{1-1 onto}{⟶} F supp \underset{˙}{0}$
50	29 49	hasheqf1od	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \|W\| = \|F supp \underset{˙}{0}\|$
51	50	fveq2d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|F supp \underset{˙}{0}\|)$
52	21 51	jca	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ((H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|F supp \underset{˙}{0}\|))$
53		f1oeq1	$⊢ g = H \circ f \to (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \leftrightarrow (H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0})$
54		coeq2	$⊢ g = H \circ f \to F \circ g = F \circ (H \circ f)$
55	54	seqeq3d	$⊢ g = H \circ f \to seq 1 (\underset{˙}{+}, (F \circ g)) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f)))$
56	55	fveq1d	$⊢ g = H \circ f \to seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|F supp \underset{˙}{0}\|)$
57	56	eqeq2d	$⊢ g = H \circ f \to (seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|) \leftrightarrow seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|F supp \underset{˙}{0}\|))$
58	53 57	anbi12d	$⊢ g = H \circ f \to ((g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow ((H \circ f) : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|F supp \underset{˙}{0}\|)))$
59	20 52 58	spcedv	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))$
60	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to G \in Mnd$
61	6	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to A \in V$
62	7	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F : A ⟶ B$
63	8	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ran F \subseteq Z (ran F)$
64		f1f1orn	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
65	10 64	syl	$⊢ φ \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
66		f1oen3g	$⊢ (H \in V \land H : (1 \dots M) \underset{1-1 onto}{⟶} ran H) \to (1 \dots M) \approx ran H$
67	16 65 66	syl2anc	$⊢ φ \to (1 \dots M) \approx ran H$
68		enfi	$⊢ (1 \dots M) \approx ran H \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
69	67 68	syl	$⊢ φ \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
70	22 69	mpbii	$⊢ φ \to ran H \in Fin$
71	70 11	ssfid	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
72	71	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F supp \underset{˙}{0} \in Fin$
73	12	neeq1i	$⊢ W \neq \emptyset \leftrightarrow (F \circ H) supp \underset{˙}{0} \neq \emptyset$
74		supp0cosupp0	$⊢ (F \in V \land H \in V) \to (F supp \underset{˙}{0} = \emptyset \to (F \circ H) supp \underset{˙}{0} = \emptyset)$
75	74	necon3d	$⊢ (F \in V \land H \in V) \to ((F \circ H) supp \underset{˙}{0} \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
76	35 38 75	syl2anc	$⊢ φ \to ((F \circ H) supp \underset{˙}{0} \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
77	73 76	syl5bi	$⊢ φ \to (W \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
78	77	imp	$⊢ (φ \land W \neq \emptyset) \to F supp \underset{˙}{0} \neq \emptyset$
79	78	adantr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F supp \underset{˙}{0} \neq \emptyset$
80	11	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F supp \underset{˙}{0} \subseteq ran H$
81	14	frnd	$⊢ φ \to ran H \subseteq A$
82	81	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ran H \subseteq A$
83	80 82	sstrd	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F supp \underset{˙}{0} \subseteq A$
84	1 2 3 4 60 61 62 63 72 79 83	gsumval3eu	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \exists! x \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))$
85		iota1	$⊢ \exists! x \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow (ι x \| \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))) = x)$
86	84 85	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow (ι x \| \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))) = x)$
87		eqid	$⊢ F supp \underset{˙}{0} = F supp \underset{˙}{0}$
88		simprl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \neg A \in ran \dots$
89	1 2 3 4 60 61 62 63 72 79 87 88	gsumval3a	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \sum_{G} F = (ι x \| \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)))$
90	89	eqeq1d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (\sum_{G} F = x \leftrightarrow (ι x \| \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))) = x)$
91	86 90	bitr4d	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = x)$
92	91	alrimiv	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \forall x (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = x)$
93		fvex	$⊢ seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \in V$
94		eqeq1	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \to (x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|) \leftrightarrow seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|))$
95	94	anbi2d	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \to ((g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)))$
96	95	exbidv	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)))$
97		eqeq2	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \to (\sum_{G} F = x \leftrightarrow \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|))$
98	96 97	bibi12d	$⊢ x = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \to ((\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = x) \leftrightarrow (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|)))$
99	93 98	spcv	$⊢ \forall x (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land x = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = x) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|))$
100	92 99	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (\exists g (g : (1 \dots \|F supp \underset{˙}{0}\|) \underset{1-1 onto}{⟶} F supp \underset{˙}{0} \land seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ g)) (\|F supp \underset{˙}{0}\|)) \leftrightarrow \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|))$
101	59 100	mpbid	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|)$

Metamath Proof Explorer

Theorem gsumval3lem2

Proof