gsumval3

Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by AV, 31-May-2019)

	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	gsumval3	$⊢ φ \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$

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	2	gsumz	$⊢ (G \in Mnd \land A \in V) \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
14	5 6 13	syl2anc	$⊢ φ \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
15	14	adantr	$⊢ (φ \land W = \emptyset) \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
16	7	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
17	16	adantr	$⊢ (φ \land W = \emptyset) \to F = (x \in A ⟼ F (x))$
18		f1f	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) ⟶ A$
19	10 18	syl	$⊢ φ \to H : (1 \dots M) ⟶ A$
20	19	ad2antrr	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to H : (1 \dots M) ⟶ A$
21		f1f1orn	$⊢ H : (1 \dots M) \underset{1-1}{⟶} A \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
22	10 21	syl	$⊢ φ \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
23	22	adantr	$⊢ (φ \land W = \emptyset) \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
24		f1ocnv	$⊢ H : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to H^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M)$
25		f1of	$⊢ H^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M) \to H^{-1} : ran H ⟶ (1 \dots M)$
26	23 24 25	3syl	$⊢ (φ \land W = \emptyset) \to H^{-1} : ran H ⟶ (1 \dots M)$
27	26	ffvelrnda	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to H^{-1} (x) \in (1 \dots M)$
28		fvco3	$⊢ (H : (1 \dots M) ⟶ A \land H^{-1} (x) \in (1 \dots M)) \to (F \circ H) (H^{-1} (x)) = F (H (H^{-1} (x)))$
29	20 27 28	syl2anc	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to (F \circ H) (H^{-1} (x)) = F (H (H^{-1} (x)))$
30		simpr	$⊢ (φ \land W = \emptyset) \to W = \emptyset$
31	30	difeq2d	$⊢ (φ \land W = \emptyset) \to (1 \dots M) ∖ W = (1 \dots M) ∖ \emptyset$
32		dif0	$⊢ (1 \dots M) ∖ \emptyset = (1 \dots M)$
33	31 32	eqtrdi	$⊢ (φ \land W = \emptyset) \to (1 \dots M) ∖ W = (1 \dots M)$
34	33	adantr	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to (1 \dots M) ∖ W = (1 \dots M)$
35	27 34	eleqtrrd	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to H^{-1} (x) \in ((1 \dots M) ∖ W)$
36		fco	$⊢ (F : A ⟶ B \land H : (1 \dots M) ⟶ A) \to (F \circ H) : (1 \dots M) ⟶ B$
37	7 19 36	syl2anc	$⊢ φ \to (F \circ H) : (1 \dots M) ⟶ B$
38	37	adantr	$⊢ (φ \land W = \emptyset) \to (F \circ H) : (1 \dots M) ⟶ B$
39	12	eqimss2i	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq W$
40	39	a1i	$⊢ (φ \land W = \emptyset) \to (F \circ H) supp \underset{˙}{0} \subseteq W$
41		ovexd	$⊢ (φ \land W = \emptyset) \to (1 \dots M) \in V$
42	2	fvexi	$⊢ \underset{˙}{0} \in V$
43	42	a1i	$⊢ (φ \land W = \emptyset) \to \underset{˙}{0} \in V$
44	38 40 41 43	suppssr	$⊢ ((φ \land W = \emptyset) \land H^{-1} (x) \in ((1 \dots M) ∖ W)) \to (F \circ H) (H^{-1} (x)) = \underset{˙}{0}$
45	35 44	syldan	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to (F \circ H) (H^{-1} (x)) = \underset{˙}{0}$
46		f1ocnvfv2	$⊢ (H : (1 \dots M) \underset{1-1 onto}{⟶} ran H \land x \in ran H) \to H (H^{-1} (x)) = x$
47	23 46	sylan	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to H (H^{-1} (x)) = x$
48	47	fveq2d	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to F (H (H^{-1} (x))) = F (x)$
49	29 45 48	3eqtr3rd	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to F (x) = \underset{˙}{0}$
50		fvex	$⊢ F (x) \in V$
51	50	elsn	$⊢ F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0}$
52	49 51	sylibr	$⊢ ((φ \land W = \emptyset) \land x \in ran H) \to F (x) \in \{\underset{˙}{0}\}$
53	52	adantlr	$⊢ (((φ \land W = \emptyset) \land x \in A) \land x \in ran H) \to F (x) \in \{\underset{˙}{0}\}$
54		eldif	$⊢ x \in (A ∖ ran H) \leftrightarrow (x \in A \land \neg x \in ran H)$
55	42	a1i	$⊢ φ \to \underset{˙}{0} \in V$
56	7 11 6 55	suppssr	$⊢ (φ \land x \in (A ∖ ran H)) \to F (x) = \underset{˙}{0}$
57	56 51	sylibr	$⊢ (φ \land x \in (A ∖ ran H)) \to F (x) \in \{\underset{˙}{0}\}$
58	54 57	sylan2br	$⊢ (φ \land (x \in A \land \neg x \in ran H)) \to F (x) \in \{\underset{˙}{0}\}$
59	58	adantlr	$⊢ ((φ \land W = \emptyset) \land (x \in A \land \neg x \in ran H)) \to F (x) \in \{\underset{˙}{0}\}$
60	59	anassrs	$⊢ (((φ \land W = \emptyset) \land x \in A) \land \neg x \in ran H) \to F (x) \in \{\underset{˙}{0}\}$
61	53 60	pm2.61dan	$⊢ ((φ \land W = \emptyset) \land x \in A) \to F (x) \in \{\underset{˙}{0}\}$
62	61 51	sylib	$⊢ ((φ \land W = \emptyset) \land x \in A) \to F (x) = \underset{˙}{0}$
63	62	mpteq2dva	$⊢ (φ \land W = \emptyset) \to (x \in A ⟼ F (x)) = (x \in A ⟼ \underset{˙}{0})$
64	17 63	eqtrd	$⊢ (φ \land W = \emptyset) \to F = (x \in A ⟼ \underset{˙}{0})$
65	64	oveq2d	$⊢ (φ \land W = \emptyset) \to \sum_{G} F = \underset{x \in A}{\sum_{G}} \underset{˙}{0}$
66	1 2	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in B$
67	1 3 2	mndlid	$⊢ (G \in Mnd \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
68	5 66 67	syl2anc2	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
69	68	adantr	$⊢ (φ \land W = \emptyset) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
70		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
71	9 70	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
72	71	adantr	$⊢ (φ \land W = \emptyset) \to M \in ℤ_{\geq 1}$
73	33	eleq2d	$⊢ (φ \land W = \emptyset) \to (x \in ((1 \dots M) ∖ W) \leftrightarrow x \in (1 \dots M))$
74	73	biimpar	$⊢ ((φ \land W = \emptyset) \land x \in (1 \dots M)) \to x \in ((1 \dots M) ∖ W)$
75	38 40 41 43	suppssr	$⊢ ((φ \land W = \emptyset) \land x \in ((1 \dots M) ∖ W)) \to (F \circ H) (x) = \underset{˙}{0}$
76	74 75	syldan	$⊢ ((φ \land W = \emptyset) \land x \in (1 \dots M)) \to (F \circ H) (x) = \underset{˙}{0}$
77	69 72 76	seqid3	$⊢ (φ \land W = \emptyset) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = \underset{˙}{0}$
78	15 65 77	3eqtr4d	$⊢ (φ \land W = \emptyset) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
79		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
80		ffn	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ \to \dots Fn (ℤ \times ℤ)$
81		ovelrn	$⊢ \dots Fn (ℤ \times ℤ) \to (A \in ran \dots \leftrightarrow \exists m \in ℤ \exists n \in ℤ A = (m \dots n))$
82	79 80 81	mp2b	$⊢ A \in ran \dots \leftrightarrow \exists m \in ℤ \exists n \in ℤ A = (m \dots n)$
83	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to G \in Mnd$
84		simpr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to A = (m \dots n)$
85		frel	$⊢ F : A ⟶ B \to Rel F$
86		reldm0	$⊢ Rel F \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
87	7 85 86	3syl	$⊢ φ \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
88	7	fdmd	$⊢ φ \to dom F = A$
89	88	eqeq1d	$⊢ φ \to (dom F = \emptyset \leftrightarrow A = \emptyset)$
90	87 89	bitrd	$⊢ φ \to (F = \emptyset \leftrightarrow A = \emptyset)$
91		coeq1	$⊢ F = \emptyset \to F \circ H = \emptyset \circ H$
92		co01	$⊢ \emptyset \circ H = \emptyset$
93	91 92	eqtrdi	$⊢ F = \emptyset \to F \circ H = \emptyset$
94	93	oveq1d	$⊢ F = \emptyset \to (F \circ H) supp \underset{˙}{0} = \emptyset supp \underset{˙}{0}$
95		supp0	$⊢ \underset{˙}{0} \in V \to \emptyset supp \underset{˙}{0} = \emptyset$
96	42 95	ax-mp	$⊢ \emptyset supp \underset{˙}{0} = \emptyset$
97	94 96	eqtrdi	$⊢ F = \emptyset \to (F \circ H) supp \underset{˙}{0} = \emptyset$
98	12 97	syl5eq	$⊢ F = \emptyset \to W = \emptyset$
99	90 98	syl6bir	$⊢ φ \to (A = \emptyset \to W = \emptyset)$
100	99	necon3d	$⊢ φ \to (W \neq \emptyset \to A \neq \emptyset)$
101	100	imp	$⊢ (φ \land W \neq \emptyset) \to A \neq \emptyset$
102	101	adantr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to A \neq \emptyset$
103	84 102	eqnetrrd	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to (m \dots n) \neq \emptyset$
104		fzn0	$⊢ (m \dots n) \neq \emptyset \leftrightarrow n \in ℤ_{\geq m}$
105	103 104	sylib	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to n \in ℤ_{\geq m}$
106	7	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to F : A ⟶ B$
107	84	feq2d	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to (F : A ⟶ B \leftrightarrow F : (m \dots n) ⟶ B)$
108	106 107	mpbid	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to F : (m \dots n) ⟶ B$
109	1 3 83 105 108	gsumval2	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to \sum_{G} F = seq m (\underset{˙}{+}, F) (n)$
110		frn	$⊢ H : (1 \dots M) ⟶ A \to ran H \subseteq A$
111	10 18 110	3syl	$⊢ φ \to ran H \subseteq A$
112	111	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to ran H \subseteq A$
113	112 84	sseqtrd	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to ran H \subseteq (m \dots n)$
114		fzssuz	$⊢ (m \dots n) \subseteq ℤ_{\geq m}$
115		uzssz	$⊢ ℤ_{\geq m} \subseteq ℤ$
116		zssre	$⊢ ℤ \subseteq ℝ$
117	115 116	sstri	$⊢ ℤ_{\geq m} \subseteq ℝ$
118	114 117	sstri	$⊢ (m \dots n) \subseteq ℝ$
119	113 118	sstrdi	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to ran H \subseteq ℝ$
120		ltso	$⊢ < Or ℝ$
121		soss	$⊢ ran H \subseteq ℝ \to (< Or ℝ \to < Or ran H)$
122	119 120 121	mpisyl	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to < Or ran H$
123		fzfi	$⊢ (1 \dots M) \in Fin$
124	123	a1i	$⊢ φ \to (1 \dots M) \in Fin$
125		fex2	$⊢ (H : (1 \dots M) ⟶ A \land (1 \dots M) \in Fin \land A \in V) \to H \in V$
126	19 124 6 125	syl3anc	$⊢ φ \to H \in V$
127		f1oen3g	$⊢ (H \in V \land H : (1 \dots M) \underset{1-1 onto}{⟶} ran H) \to (1 \dots M) \approx ran H$
128	126 22 127	syl2anc	$⊢ φ \to (1 \dots M) \approx ran H$
129		enfi	$⊢ (1 \dots M) \approx ran H \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
130	128 129	syl	$⊢ φ \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
131	123 130	mpbii	$⊢ φ \to ran H \in Fin$
132	131	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to ran H \in Fin$
133		fz1iso	$⊢ (< Or ran H \land ran H \in Fin) \to \exists f f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H)$
134	122 132 133	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to \exists f f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H)$
135	9	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
136		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
137	135 136	syl	$⊢ φ \to \|(1 \dots M)\| = M$
138	124 22	hasheqf1od	$⊢ φ \to \|(1 \dots M)\| = \|ran H\|$
139	137 138	eqtr3d	$⊢ φ \to M = \|ran H\|$
140	139	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to M = \|ran H\|$
141	140	fveq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to seq 1 (\underset{˙}{+}, (F \circ f)) (M) = seq 1 (\underset{˙}{+}, (F \circ f)) (\|ran H\|)$
142	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to G \in Mnd$
143	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
144	143	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
145	142 144	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
146	8	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran F \subseteq Z (ran F)$
147	146	sselda	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in ran F) \to x \in Z (ran F)$
148	3 4	cntzi	$⊢ (x \in Z (ran F) \land y \in ran F) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
149	147 148	sylan	$⊢ ((((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in ran F) \land y \in ran F) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
150	149	anasss	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land (x \in ran F \land y \in ran F)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
151	1 3	mndass	$⊢ (G \in Mnd \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
152	142 151	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
153	71	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to M \in ℤ_{\geq 1}$
154	7	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F : A ⟶ B$
155	154	frnd	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran F \subseteq B$
156		simprr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H)$
157		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H) \to f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H$
158	156 157	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H$
159	140	oveq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (1 \dots M) = (1 \dots \|ran H\|)$
160	159	f1oeq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \leftrightarrow f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H)$
161	158 160	mpbird	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
162		f1ocnv	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M)$
163	161 162	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M)$
164	22	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to H : (1 \dots M) \underset{1-1 onto}{⟶} ran H$
165		f1oco	$⊢ (f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M) \land H : (1 \dots M) \underset{1-1 onto}{⟶} ran H) \to (f^{-1} \circ H) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
166	163 164 165	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (f^{-1} \circ H) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
167		ffn	$⊢ F : A ⟶ B \to F Fn A$
168		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
169	167 168	sylib	$⊢ F : A ⟶ B \to F : A \underset{onto}{⟶} ran F$
170		fof	$⊢ F : A \underset{onto}{⟶} ran F \to F : A ⟶ ran F$
171	154 169 170	3syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F : A ⟶ ran F$
172		f1of	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f : (1 \dots M) ⟶ ran H$
173	161 172	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f : (1 \dots M) ⟶ ran H$
174	111	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran H \subseteq A$
175	173 174	fssd	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f : (1 \dots M) ⟶ A$
176		fco	$⊢ (F : A ⟶ ran F \land f : (1 \dots M) ⟶ A) \to (F \circ f) : (1 \dots M) ⟶ ran F$
177	171 175 176	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (F \circ f) : (1 \dots M) ⟶ ran F$
178	177	ffvelrnda	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in (1 \dots M)) \to (F \circ f) (x) \in ran F$
179		f1ococnv2	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f \circ f^{-1} = {I ↾}_{ran H}$
180	161 179	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f \circ f^{-1} = {I ↾}_{ran H}$
181	180	coeq1d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (f \circ f^{-1}) \circ H = ({I ↾}_{ran H}) \circ H$
182		f1of	$⊢ H : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to H : (1 \dots M) ⟶ ran H$
183		fcoi2	$⊢ H : (1 \dots M) ⟶ ran H \to ({I ↾}_{ran H}) \circ H = H$
184	164 182 183	3syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ({I ↾}_{ran H}) \circ H = H$
185	181 184	eqtr2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to H = (f \circ f^{-1}) \circ H$
186		coass	$⊢ (f \circ f^{-1}) \circ H = f \circ (f^{-1} \circ H)$
187	185 186	eqtrdi	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to H = f \circ (f^{-1} \circ H)$
188	187	coeq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F \circ H = F \circ (f \circ (f^{-1} \circ H))$
189		coass	$⊢ (F \circ f) \circ (f^{-1} \circ H) = F \circ (f \circ (f^{-1} \circ H))$
190	188 189	eqtr4di	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F \circ H = (F \circ f) \circ (f^{-1} \circ H)$
191	190	fveq1d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (F \circ H) (k) = ((F \circ f) \circ (f^{-1} \circ H)) (k)$
192	191	adantr	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land k \in (1 \dots M)) \to (F \circ H) (k) = ((F \circ f) \circ (f^{-1} \circ H)) (k)$
193		f1of	$⊢ f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M) \to f^{-1} : ran H ⟶ (1 \dots M)$
194	161 162 193	3syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f^{-1} : ran H ⟶ (1 \dots M)$
195	164 182	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to H : (1 \dots M) ⟶ ran H$
196		fco	$⊢ (f^{-1} : ran H ⟶ (1 \dots M) \land H : (1 \dots M) ⟶ ran H) \to (f^{-1} \circ H) : (1 \dots M) ⟶ (1 \dots M)$
197	194 195 196	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (f^{-1} \circ H) : (1 \dots M) ⟶ (1 \dots M)$
198		fvco3	$⊢ ((f^{-1} \circ H) : (1 \dots M) ⟶ (1 \dots M) \land k \in (1 \dots M)) \to ((F \circ f) \circ (f^{-1} \circ H)) (k) = (F \circ f) ((f^{-1} \circ H) (k))$
199	197 198	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land k \in (1 \dots M)) \to ((F \circ f) \circ (f^{-1} \circ H)) (k) = (F \circ f) ((f^{-1} \circ H) (k))$
200	192 199	eqtrd	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land k \in (1 \dots M)) \to (F \circ H) (k) = (F \circ f) ((f^{-1} \circ H) (k))$
201	145 150 152 153 155 166 178 200	seqf1o	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq 1 (\underset{˙}{+}, (F \circ f)) (M)$
202	1 3 2	mndlid	$⊢ (G \in Mnd \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
203	142 202	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
204	1 3 2	mndrid	$⊢ (G \in Mnd \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
205	142 204	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
206	142 66	syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to \underset{˙}{0} \in B$
207		fdm	$⊢ H : (1 \dots M) ⟶ A \to dom H = (1 \dots M)$
208	10 18 207	3syl	$⊢ φ \to dom H = (1 \dots M)$
209		eluzfz1	$⊢ M \in ℤ_{\geq 1} \to 1 \in (1 \dots M)$
210		ne0i	$⊢ 1 \in (1 \dots M) \to (1 \dots M) \neq \emptyset$
211	71 209 210	3syl	$⊢ φ \to (1 \dots M) \neq \emptyset$
212	208 211	eqnetrd	$⊢ φ \to dom H \neq \emptyset$
213		dm0rn0	$⊢ dom H = \emptyset \leftrightarrow ran H = \emptyset$
214	213	necon3bii	$⊢ dom H \neq \emptyset \leftrightarrow ran H \neq \emptyset$
215	212 214	sylib	$⊢ φ \to ran H \neq \emptyset$
216	215	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran H \neq \emptyset$
217	113	adantrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran H \subseteq (m \dots n)$
218		simprl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to A = (m \dots n)$
219	218	eleq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (x \in A \leftrightarrow x \in (m \dots n))$
220	219	biimpar	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in (m \dots n)) \to x \in A$
221	154	ffvelrnda	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in A) \to F (x) \in B$
222	220 221	syldan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in (m \dots n)) \to F (x) \in B$
223	218	difeq1d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to A ∖ ran H = (m \dots n) ∖ ran H$
224	223	eleq2d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to (x \in (A ∖ ran H) \leftrightarrow x \in ((m \dots n) ∖ ran H))$
225	224	biimpar	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in ((m \dots n) ∖ ran H)) \to x \in (A ∖ ran H)$
226	56	ad4ant14	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in (A ∖ ran H)) \to F (x) = \underset{˙}{0}$
227	225 226	syldan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land x \in ((m \dots n) ∖ ran H)) \to F (x) = \underset{˙}{0}$
228		f1of	$⊢ f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H \to f : (1 \dots \|ran H\|) ⟶ ran H$
229	156 157 228	3syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to f : (1 \dots \|ran H\|) ⟶ ran H$
230		fvco3	$⊢ (f : (1 \dots \|ran H\|) ⟶ ran H \land y \in (1 \dots \|ran H\|)) \to (F \circ f) (y) = F (f (y))$
231	229 230	sylan	$⊢ (((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \land y \in (1 \dots \|ran H\|)) \to (F \circ f) (y) = F (f (y))$
232	203 205 145 206 156 216 217 222 227 231	seqcoll2	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to seq m (\underset{˙}{+}, F) (n) = seq 1 (\underset{˙}{+}, (F \circ f)) (\|ran H\|)$
233	141 201 232	3eqtr4d	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq m (\underset{˙}{+}, F) (n)$
234	233	expr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to (f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq m (\underset{˙}{+}, F) (n))$
235	234	exlimdv	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to (\exists f f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq m (\underset{˙}{+}, F) (n))$
236	134 235	mpd	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq m (\underset{˙}{+}, F) (n)$
237	109 236	eqtr4d	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
238	237	ex	$⊢ (φ \land W \neq \emptyset) \to (A = (m \dots n) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
239	238	rexlimdvw	$⊢ (φ \land W \neq \emptyset) \to (\exists n \in ℤ A = (m \dots n) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
240	239	rexlimdvw	$⊢ (φ \land W \neq \emptyset) \to (\exists m \in ℤ \exists n \in ℤ A = (m \dots n) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
241	82 240	syl5bi	$⊢ (φ \land W \neq \emptyset) \to (A \in ran \dots \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
242		suppssdm	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq dom (F \circ H)$
243	12 242	eqsstri	$⊢ W \subseteq dom (F \circ H)$
244	243 37	fssdm	$⊢ φ \to W \subseteq (1 \dots M)$
245		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
246		nnssre	$⊢ ℕ \subseteq ℝ$
247	245 246	sstri	$⊢ (1 \dots M) \subseteq ℝ$
248	244 247	sstrdi	$⊢ φ \to W \subseteq ℝ$
249		soss	$⊢ W \subseteq ℝ \to (< Or ℝ \to < Or W)$
250	248 120 249	mpisyl	$⊢ φ \to < Or W$
251		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
252	123 244 251	sylancr	$⊢ φ \to W \in Fin$
253		fz1iso	$⊢ (< Or W \land W \in Fin) \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
254	250 252 253	syl2anc	$⊢ φ \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
255	254	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
256	1 2 3 4 5 6 7 8 9 10 11 12	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\|)$
257	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to G \in Mnd$
258	257 202	sylan	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
259	257 204	sylan	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
260	257 144	sylan	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
261	257 66	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \underset{˙}{0} \in B$
262		simprr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to f {Isom}_{<, <} ((1 \dots \|W\|), W)$
263		simplr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \neq \emptyset$
264	244	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \subseteq (1 \dots M)$
265	37	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (F \circ H) : (1 \dots M) ⟶ B$
266	265	ffvelrnda	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land x \in (1 \dots M)) \to (F \circ H) (x) \in B$
267	39	a1i	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (F \circ H) supp \underset{˙}{0} \subseteq W$
268		ovexd	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (1 \dots M) \in V$
269	42	a1i	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \underset{˙}{0} \in V$
270	265 267 268 269	suppssr	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land x \in ((1 \dots M) ∖ W)) \to (F \circ H) (x) = \underset{˙}{0}$
271		coass	$⊢ (F \circ H) \circ f = F \circ (H \circ f)$
272	271	fveq1i	$⊢ ((F \circ H) \circ f) (y) = (F \circ (H \circ f)) (y)$
273		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|W\|), W) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
274		f1of	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) ⟶ W$
275	262 273 274	3syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to f : (1 \dots \|W\|) ⟶ W$
276		fvco3	$⊢ (f : (1 \dots \|W\|) ⟶ W \land y \in (1 \dots \|W\|)) \to ((F \circ H) \circ f) (y) = (F \circ H) (f (y))$
277	275 276	sylan	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land y \in (1 \dots \|W\|)) \to ((F \circ H) \circ f) (y) = (F \circ H) (f (y))$
278	272 277	eqtr3id	$⊢ (((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \land y \in (1 \dots \|W\|)) \to (F \circ (H \circ f)) (y) = (F \circ H) (f (y))$
279	258 259 260 261 262 263 264 266 270 278	seqcoll2	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq 1 (\underset{˙}{+}, (F \circ (H \circ f))) (\|W\|)$
280	256 279	eqtr4d	$⊢ ((φ \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)) (M)$
281	280	expr	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to (f {Isom}_{<, <} ((1 \dots \|W\|), W) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
282	281	exlimdv	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to (\exists f f {Isom}_{<, <} ((1 \dots \|W\|), W) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
283	255 282	mpd	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
284	283	ex	$⊢ (φ \land W \neq \emptyset) \to (\neg A \in ran \dots \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
285	241 284	pm2.61d	$⊢ (φ \land W \neq \emptyset) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
286	78 285	pm2.61dane	$⊢ φ \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$

Metamath Proof Explorer

Theorem gsumval3

Proof