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		fex2	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in Fin \land A \in V) \to H \in V$
17	14 15 6 16	syl3anc	$⊢ φ \to H \in V$
18		vex	$⊢ f \in V$
19		coexg	$⊢ (H \in V \land f \in V) \to H \circ f \in V$
20	17 18 19	sylancl	$⊢ φ \to H \circ f \in V$
21	20	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to H \circ f \in V$
22	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}$
23		fzfi	$⊢ (1 \dots M) \in Fin$
24		suppssdm	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq dom (F \circ H)$
25	12 24	eqsstri	$⊢ W \subseteq dom (F \circ H)$
26		fco	$⊢ (F : A ⟶ B \land H : (1 \dots M) ⟶ A) \to (F \circ H) : (1 \dots M) ⟶ B$
27	7 14 26	syl2anc	$⊢ φ \to (F \circ H) : (1 \dots M) ⟶ B$
28	25 27	fssdm	$⊢ φ \to W \subseteq (1 \dots M)$
29		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
30	23 28 29	sylancr	$⊢ φ \to W \in Fin$
31	30	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \in Fin$
32	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$
33	28	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \subseteq (1 \dots M)$
34		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]$
35	32 33 34	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]$
36	12	imaeq2i	$⊢ H [W] = H [(F \circ H) supp \underset{˙}{0}]$
37		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
38	7 6 37	syl2anc	$⊢ φ \to F \in V$
39		ovex	$⊢ (1 \dots M) \in V$
40		fex	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to H \in V$
41	14 39 40	sylancl	$⊢ φ \to H \in V$
42	38 41	jca	$⊢ φ \to (F \in V \land H \in V)$
43		f1fun	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to Fun H$
44	10 43	syl	$⊢ φ \to Fun H$
45	44 11	jca	$⊢ φ \to (Fun H \land F supp \underset{˙}{0} \subseteq ran H)$
46		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})$
47	42 45 46	sylc	$⊢ φ \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
48	47	adantr	$⊢ (φ \land W \neq \emptyset) \to H [(F \circ H) supp \underset{˙}{0}] = F supp \underset{˙}{0}$
49	36 48	syl5eq	$⊢ (φ \land W \neq \emptyset) \to H [W] = F supp \underset{˙}{0}$
50	49	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}$
51	50	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})$
52	35 51	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}$
53	31 52	hasheqf1od	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \|W\| = \|F supp \underset{˙}{0}\|$
54	53	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}\|)$
55	22 54	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}\|))$
56		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})$
57		coeq2	$⊢ g = H \circ f \to F \circ g = F \circ (H \circ f)$
58	57	seqeq3d	$⊢ g = H \circ f \to seq 1 (\underset{˙}{+}, (F \circ g)) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f)))$
59	58	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}\|)$
60	59	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}\|))$
61	56 60	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}\|)))$
62	21 55 61	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}\|))$
63	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to G \in Mnd$
64	6	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to A \in V$
65	7	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to F : A ⟶ B$
66	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)$
67		f1f1orn	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
68	10 67	syl	$⊢ φ \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
69		f1oen3g	$⊢ (H \in V \land H : (1 \dots M) \underset{1-1 onto}{⟶} ran H) \to (1 \dots M) \approx ran H$
70	17 68 69	syl2anc	$⊢ φ \to (1 \dots M) \approx ran H$
71		enfi	$⊢ (1 \dots M) \approx ran H \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
72	70 71	syl	$⊢ φ \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
73	23 72	mpbii	$⊢ φ \to ran H \in Fin$
74	73 11	ssfid	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
75	74	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$
76	12	neeq1i	$⊢ W \neq \emptyset \leftrightarrow (F \circ H) supp \underset{˙}{0} \neq \emptyset$
77		supp0cosupp0	$⊢ (F \in V \land H \in V) \to (F supp \underset{˙}{0} = \emptyset \to (F \circ H) supp \underset{˙}{0} = \emptyset)$
78	77	necon3d	$⊢ (F \in V \land H \in V) \to ((F \circ H) supp \underset{˙}{0} \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
79	38 41 78	syl2anc	$⊢ φ \to ((F \circ H) supp \underset{˙}{0} \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
80	76 79	syl5bi	$⊢ φ \to (W \neq \emptyset \to F supp \underset{˙}{0} \neq \emptyset)$
81	80	imp	$⊢ (φ \land W \neq \emptyset) \to F supp \underset{˙}{0} \neq \emptyset$
82	81	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$
83	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$
84	14	frnd	$⊢ φ \to ran H \subseteq A$
85	84	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to ran H \subseteq A$
86	83 85	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$
87	1 2 3 4 63 64 65 66 75 82 86	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}\|))$
88		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)$
89	87 88	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)$
90		eqid	$⊢ F supp \underset{˙}{0} = F supp \underset{˙}{0}$
91		simprl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \neg A \in ran \dots$
92	1 2 3 4 63 64 65 66 75 82 90 91	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}\|)))$
93	92	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)$
94	89 93	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)$
95	94	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)$
96		fvex	$⊢ seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|) \in V$
97		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}\|))$
98	97	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}\|)))$
99	98	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}\|)))$
100		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\|))$
101	99 100	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\|)))$
102	96 101	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\|))$
103	95 102	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\|))$
104	62 103	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