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	ffvelcdmda	$⊢ ((φ \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	eqtrid	$⊢ F = \emptyset \to W = \emptyset$
99	90 98	biimtrrdi	$⊢ φ \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	19 124	fexd	$⊢ φ \to H \in V$
126		f1oen3g	$⊢ (H \in V \land H : (1 \dots M) \underset{1-1 onto}{⟶} ran H) \to (1 \dots M) \approx ran H$
127	125 22 126	syl2anc	$⊢ φ \to (1 \dots M) \approx ran H$
128		enfi	$⊢ (1 \dots M) \approx ran H \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
129	127 128	syl	$⊢ φ \to ((1 \dots M) \in Fin \leftrightarrow ran H \in Fin)$
130	123 129	mpbii	$⊢ φ \to ran H \in Fin$
131	130	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to ran H \in Fin$
132		fz1iso	$⊢ (< Or ran H \land ran H \in Fin) \to \exists f f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H)$
133	122 131 132	syl2anc	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to \exists f f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H)$
134	9	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
135		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
136	134 135	syl	$⊢ φ \to \|(1 \dots M)\| = M$
137	124 22	hasheqf1od	$⊢ φ \to \|(1 \dots M)\| = \|ran H\|$
138	136 137	eqtr3d	$⊢ φ \to M = \|ran H\|$
139	138	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to M = \|ran H\|$
140	139	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\|)$
141	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to G \in Mnd$
142	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
143	142	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
144	141 143	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$
145	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)$
146	145	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)$
147	3 4	cntzi	$⊢ (x \in Z (ran F) \land y \in ran F) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
148	146 147	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$
149	148	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$
150	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)$
151	141 150	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)$
152	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}$
153	7	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F : A ⟶ B$
154	153	frnd	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran F \subseteq B$
155		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)$
156		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H) \to f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H$
157	155 156	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$
158	139	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\|)$
159	158	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)$
160	157 159	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$
161		f1ocnv	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M)$
162	160 161	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)$
163	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$
164		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)$
165	162 163 164	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)$
166		ffn	$⊢ F : A ⟶ B \to F Fn A$
167		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
168	166 167	sylib	$⊢ F : A ⟶ B \to F : A \underset{onto}{⟶} ran F$
169		fof	$⊢ F : A \underset{onto}{⟶} ran F \to F : A ⟶ ran F$
170	153 168 169	3syl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to F : A ⟶ ran F$
171		f1of	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f : (1 \dots M) ⟶ ran H$
172	160 171	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$
173	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$
174	172 173	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$
175		fco	$⊢ (F : A ⟶ ran F \land f : (1 \dots M) ⟶ A) \to (F \circ f) : (1 \dots M) ⟶ ran F$
176	170 174 175	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$
177	176	ffvelcdmda	$⊢ (((φ \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$
178		f1ococnv2	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to f \circ f^{-1} = {I ↾}_{ran H}$
179	160 178	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}$
180	179	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$
181		f1of	$⊢ H : (1 \dots M) \underset{1-1 onto}{⟶} ran H \to H : (1 \dots M) ⟶ ran H$
182		fcoi2	$⊢ H : (1 \dots M) ⟶ ran H \to ({I ↾}_{ran H}) \circ H = H$
183	163 181 182	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$
184	180 183	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$
185		coass	$⊢ (f \circ f^{-1}) \circ H = f \circ (f^{-1} \circ H)$
186	184 185	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)$
187	186	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))$
188		coass	$⊢ (F \circ f) \circ (f^{-1} \circ H) = F \circ (f \circ (f^{-1} \circ H))$
189	187 188	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)$
190	189	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)$
191	190	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)$
192		f1of	$⊢ f^{-1} : ran H \underset{1-1 onto}{⟶} (1 \dots M) \to f^{-1} : ran H ⟶ (1 \dots M)$
193	160 161 192	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)$
194	163 181	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$
195		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)$
196	193 194 195	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)$
197		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))$
198	196 197	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))$
199	191 198	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))$
200	144 149 151 152 154 165 177 199	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)$
201	1 3 2	mndlid	$⊢ (G \in Mnd \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
202	141 201	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$
203	1 3 2	mndrid	$⊢ (G \in Mnd \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
204	141 203	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$
205	141 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$
206		fdm	$⊢ H : (1 \dots M) ⟶ A \to dom H = (1 \dots M)$
207	10 18 206	3syl	$⊢ φ \to dom H = (1 \dots M)$
208		eluzfz1	$⊢ M \in ℤ_{\geq 1} \to 1 \in (1 \dots M)$
209		ne0i	$⊢ 1 \in (1 \dots M) \to (1 \dots M) \neq \emptyset$
210	71 208 209	3syl	$⊢ φ \to (1 \dots M) \neq \emptyset$
211	207 210	eqnetrd	$⊢ φ \to dom H \neq \emptyset$
212		dm0rn0	$⊢ dom H = \emptyset \leftrightarrow ran H = \emptyset$
213	212	necon3bii	$⊢ dom H \neq \emptyset \leftrightarrow ran H \neq \emptyset$
214	211 213	sylib	$⊢ φ \to ran H \neq \emptyset$
215	214	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to ran H \neq \emptyset$
216	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)$
217		simprl	$⊢ ((φ \land W \neq \emptyset) \land (A = (m \dots n) \land f {Isom}_{<, <} ((1 \dots \|ran H\|), ran H))) \to A = (m \dots n)$
218	217	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))$
219	218	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$
220	153	ffvelcdmda	$⊢ (((φ \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$
221	219 220	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$
222	217	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$
223	222	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))$
224	223	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)$
225	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}$
226	224 225	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}$
227		f1of	$⊢ f : (1 \dots \|ran H\|) \underset{1-1 onto}{⟶} ran H \to f : (1 \dots \|ran H\|) ⟶ ran H$
228	155 156 227	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$
229		fvco3	$⊢ (f : (1 \dots \|ran H\|) ⟶ ran H \land y \in (1 \dots \|ran H\|)) \to (F \circ f) (y) = F (f (y))$
230	228 229	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))$
231	202 204 144 205 155 215 216 221 226 230	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\|)$
232	140 200 231	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)$
233	232	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))$
234	233	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))$
235	133 234	mpd	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to seq 1 (\underset{˙}{+}, (F \circ H)) (M) = seq m (\underset{˙}{+}, F) (n)$
236	109 235	eqtr4d	$⊢ ((φ \land W \neq \emptyset) \land A = (m \dots n)) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
237	236	ex	$⊢ (φ \land W \neq \emptyset) \to (A = (m \dots n) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
238	237	rexlimdvw	$⊢ (φ \land W \neq \emptyset) \to (\exists n \in ℤ A = (m \dots n) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
239	238	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))$
240	82 239	biimtrid	$⊢ (φ \land W \neq \emptyset) \to (A \in ran \dots \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
241		suppssdm	$⊢ (F \circ H) supp \underset{˙}{0} \subseteq dom (F \circ H)$
242	12 241	eqsstri	$⊢ W \subseteq dom (F \circ H)$
243	242 37	fssdm	$⊢ φ \to W \subseteq (1 \dots M)$
244		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
245		nnssre	$⊢ ℕ \subseteq ℝ$
246	244 245	sstri	$⊢ (1 \dots M) \subseteq ℝ$
247	243 246	sstrdi	$⊢ φ \to W \subseteq ℝ$
248		soss	$⊢ W \subseteq ℝ \to (< Or ℝ \to < Or W)$
249	247 120 248	mpisyl	$⊢ φ \to < Or W$
250		ssfi	$⊢ ((1 \dots M) \in Fin \land W \subseteq (1 \dots M)) \to W \in Fin$
251	123 243 250	sylancr	$⊢ φ \to W \in Fin$
252		fz1iso	$⊢ (< Or W \land W \in Fin) \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
253	249 251 252	syl2anc	$⊢ φ \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
254	253	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to \exists f f {Isom}_{<, <} ((1 \dots \|W\|), W)$
255	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\|)$
256	5	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to G \in Mnd$
257	256 201	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$
258	256 203	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$
259	256 143	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$
260	256 66	syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \underset{˙}{0} \in B$
261		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)$
262		simplr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \neq \emptyset$
263	243	ad2antrr	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to W \subseteq (1 \dots M)$
264	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$
265	264	ffvelcdmda	$⊢ (((φ \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$
266	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$
267		ovexd	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to (1 \dots M) \in V$
268	42	a1i	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to \underset{˙}{0} \in V$
269	264 266 267 268	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}$
270		coass	$⊢ (F \circ H) \circ f = F \circ (H \circ f)$
271	270	fveq1i	$⊢ ((F \circ H) \circ f) (y) = (F \circ (H \circ f)) (y)$
272		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|W\|), W) \to f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W$
273		f1of	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) ⟶ W$
274	261 272 273	3syl	$⊢ ((φ \land W \neq \emptyset) \land (\neg A \in ran \dots \land f {Isom}_{<, <} ((1 \dots \|W\|), W))) \to f : (1 \dots \|W\|) ⟶ W$
275		fvco3	$⊢ (f : (1 \dots \|W\|) ⟶ W \land y \in (1 \dots \|W\|)) \to ((F \circ H) \circ f) (y) = (F \circ H) (f (y))$
276	274 275	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))$
277	271 276	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))$
278	257 258 259 260 261 262 263 265 269 277	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\|)$
279	255 278	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)$
280	279	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))$
281	280	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))$
282	254 281	mpd	$⊢ ((φ \land W \neq \emptyset) \land \neg A \in ran \dots) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
283	282	ex	$⊢ (φ \land W \neq \emptyset) \to (\neg A \in ran \dots \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M))$
284	240 283	pm2.61d	$⊢ (φ \land W \neq \emptyset) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$
285	78 284	pm2.61dane	$⊢ φ \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ H)) (M)$

Metamath Proof Explorer

Theorem gsumval3

Proof