Theorem gsumval3 18508

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.)

Hypotheses

Ref	Expression
gsumval3.b	⊢ 𝐵 = (Base‘𝐺)
gsumval3.0	⊢ 0 = (0g‘𝐺)
gsumval3.p	⊢ + = (+g‘𝐺)
gsumval3.z	⊢ 𝑍 = (Cntz‘𝐺)
gsumval3.g	⊢ (𝜑 → 𝐺 ∈ Mnd)
gsumval3.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
gsumval3.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsumval3.c	⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
gsumval3.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
gsumval3.h	⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
gsumval3.n	⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
gsumval3.w	⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )

Assertion

Ref	Expression
gsumval3	⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Proof of Theorem gsumval3

Dummy variables 𝑓 𝑘 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumval3.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
2		gsumval3.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		gsumval3.0	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	3	gsumz 17575	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
5	1, 2, 4	syl2anc 573	. . . 4 ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
6	5	adantr 466	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
7		gsumval3.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8	7	feqmptd 6389	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
9	8	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
10		gsumval3.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
11		f1f 6239	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴)
12	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴)
13	12	ad2antrr 705	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14		f1f1orn 6287	. . . . . . . . . . . . . . . 16 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
15	10, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
16	15	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17		f1ocnv 6288	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀))
18		f1of 6276	. . . . . . . . . . . . . 14 ⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀))
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀))
20	19	ffvelrnda 6500	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀))
21		fvco3 6415	. . . . . . . . . . . 12 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
22	13, 20, 21	syl2anc 573	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
23		simpr 471	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅)
24	23	difeq2d 3879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25		dif0 4097	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑀) ∖ ∅) = (1...𝑀)
26	24, 25	syl6eq 2821	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
27	26	adantr 466	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
28	20, 27	eleqtrrd 2853	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29		fco 6196	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
30	7, 12, 29	syl2anc 573	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
31	30	adantr 466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
32		gsumval3.w	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )
33	32	eqimss2i 3809	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊
34	33	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
35		ovexd 6823	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V)
36	3	fvexi 6341	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
37	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V)
38	31, 34, 35, 37	suppssr 7476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
39	28, 38	syldan 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
40		f1ocnvfv2 6674	. . . . . . . . . . . . 13 ⊢ ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
41	16, 40	sylan 569	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
42	41	fveq2d 6334	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥))
43	22, 39, 42	3eqtr3rd 2814	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 )
44		fvex 6340	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
45	44	elsn 4331	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )
46	43, 45	sylibr 224	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
47	46	adantlr 694	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
48		eldif 3733	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49		gsumval3.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
50	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ V)
51	7, 49, 2, 50	suppssr 7476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
52	51, 45	sylibr 224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
53	48, 52	sylan2br 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
54	53	adantlr 694	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
55	54	anassrs 453	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
56	47, 55	pm2.61dan 814	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 })
57	56, 45	sylib 208	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 )
58	57	mpteq2dva 4878	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 ))
59	9, 58	eqtrd 2805	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
60	59	oveq2d 6807	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
61		gsumval3.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐺)
62	61, 3	mndidcl 17509	. . . . . . 7 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
63	1, 62	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ∈ 𝐵)
64		gsumval3.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
65	61, 64, 3	mndlid 17512	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
66	1, 63, 65	syl2anc 573	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
67	66	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
68		gsumval3.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
69		nnuz 11923	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
70	68, 69	syl6eleq 2860	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
71	70	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈ (ℤ≥‘1))
72	26	eleq2d 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
73	72	biimpar 463	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
74	31, 34, 35, 37	suppssr 7476	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
75	73, 74	syldan 579	. . . 4 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
76	67, 71, 75	seqid3 13045	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 )
77	6, 60, 76	3eqtr4d 2815	. 2 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
78		fzf 12530	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
79		ffn 6183	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
80		ovelrn 6955	. . . . 5 ⊢ (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
81	78, 79, 80	mp2b 10	. . . 4 ⊢ (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
82	1	ad2antrr 705	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
83		simpr 471	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
84		frel 6188	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
85		reldm0 5479	. . . . . . . . . . . . . . . . 17 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
86	7, 84, 85	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
87		fdm 6189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
88	7, 87	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
89	88	eqeq1d 2773	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
90	86, 89	bitrd 268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
91		coeq1 5416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻))
92		co01 5792	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∘ 𝐻) = ∅
93	91, 92	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅)
94	93	oveq1d 6806	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0 ))
95		supp0 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ( 0 ∈ V → (∅ supp 0 ) = ∅)
96	36, 95	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ supp 0 ) = ∅
97	94, 96	syl6eq 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = ∅)
98	32, 97	syl5eq 2817	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = ∅ → 𝑊 = ∅)
99	90, 98	syl6bir 244	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
100	99	necon3d 2964	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
101	100	imp 393	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅)
102	101	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
103	83, 102	eqnetrrd 3011	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
104		fzn0 12555	. . . . . . . . . 10 ⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚))
105	103, 104	sylib 208	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚))
106	7	ad2antrr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵)
107	83	feq2d 6169	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵))
108	106, 107	mpbid 222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
109	61, 64, 82, 105, 108	gsumval2 17481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
110		frn 6191	. . . . . . . . . . . . . . 15 ⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴)
111	10, 11, 110	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐴)
112	111	ad2antrr 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴)
113	112, 83	sseqtrd 3790	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
114		fzssuz 12582	. . . . . . . . . . . . 13 ⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚)
115		uzssz 11906	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑚) ⊆ ℤ
116		zssre 11584	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
117	115, 116	sstri 3761	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑚) ⊆ ℝ
118	114, 117	sstri 3761	. . . . . . . . . . . 12 ⊢ (𝑚...𝑛) ⊆ ℝ
119	113, 118	syl6ss 3764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
120		ltso 10318	. . . . . . . . . . 11 ⊢ < Or ℝ
121		soss 5188	. . . . . . . . . . 11 ⊢ (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
122	119, 120, 121	mpisyl 21	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
123		fzfi 12972	. . . . . . . . . . . 12 ⊢ (1...𝑀) ∈ Fin
124	123	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
125		fex2 7266	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V)
126	12, 124, 2, 125	syl3anc 1476	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 ∈ V)
127		f1oen3g 8123	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
128	126, 15, 127	syl2anc 573	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻)
129		enfi 8330	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
130	128, 129	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
131	123, 130	mpbii 223	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
132	131	ad2antrr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
133		fz1iso 13441	. . . . . . . . . 10 ⊢ (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
134	122, 132, 133	syl2anc 573	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
135	68	nnnn0d 11551	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
136		hashfz1 13331	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
137	135, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
138		hashen 13332	. . . . . . . . . . . . . . . . 17 ⊢ (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
139	123, 131, 138	sylancr 575	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
140	128, 139	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
141	137, 140	eqtr3d 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻))
142	141	ad2antrr 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
143	142	fveq2d 6334	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
144	1	ad2antrr 705	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
145	61, 64	mndcl 17502	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
146	145	3expb 1113	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
147	144, 146	sylan 569	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
148		gsumval3.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
149	148	ad2antrr 705	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
150	149	sselda 3752	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
151		gsumval3.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (Cntz‘𝐺)
152	64, 151	cntzi 17962	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
153	150, 152	sylan 569	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
154	153	anasss 452	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
155	61, 64	mndass 17503	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
156	144, 155	sylan 569	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
157	70	ad2antrr 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ≥‘1))
158	7	ad2antrr 705	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵)
159		frn 6191	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
160	158, 159	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵)
161		simprr 756	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
162		isof1o 6714	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
163	161, 162	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
164	142	oveq2d 6807	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
165		f1oeq2 6267	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑀) = (1...(♯‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
166	164, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
167	163, 166	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
168		f1ocnv 6288	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
169	167, 168	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
170	15	ad2antrr 705	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
171		f1oco 6298	. . . . . . . . . . . . . 14 ⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
172	169, 170, 171	syl2anc 573	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
173		ffn 6183	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
174		dffn4 6260	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
175	173, 174	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹)
176		fof 6254	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹)
177	158, 175, 176	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
178		f1of 6276	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻)
179	167, 178	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
180	111	ad2antrr 705	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴)
181	179, 180	fssd 6195	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
182		fco 6196	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
183	177, 181, 182	syl2anc 573	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
184	183	ffvelrnda 6500	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹)
185		f1ococnv2 6302	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
186	167, 185	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
187	186	coeq1d 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
188		f1of 6276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻)
189		fcoi2 6217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
190	170, 188, 189	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
191	187, 190	eqtr2d 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻))
192		coass 5796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻))
193	191, 192	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
194	193	coeq2d 5421	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))))
195		coass 5796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
196	194, 195	syl6eqr 2823	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)))
197	196	fveq1d 6332	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
198	197	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
199		f1of 6276	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀))
200	167, 168, 199	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀))
201	170, 188	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
202		fco 6196	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
203	200, 201, 202	syl2anc 573	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
204		fvco3 6415	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
205	203, 204	sylan 569	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
206	198, 205	eqtrd 2805	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
207	147, 154, 156, 157, 160, 172, 184, 206	seqf1o 13042	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀))
208	61, 64, 3	mndlid 17512	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
209	144, 208	sylan 569	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
210	61, 64, 3	mndrid 17513	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
211	144, 210	sylan 569	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
212	144, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 0 ∈ 𝐵)
213		fdm 6189	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
214	10, 11, 213	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = (1...𝑀))
215		eluzfz1 12548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑀))
216		ne0i 4069	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
217	70, 215, 216	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
218	214, 217	eqnetrd 3010	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐻 ≠ ∅)
219		dm0rn0 5478	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
220	219	necon3bii 2995	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
221	218, 220	sylib 208	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ≠ ∅)
222	221	ad2antrr 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
223	113	adantrr 696	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
224		simprl 754	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
225	224	eleq2d 2836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛)))
226	225	biimpar 463	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴)
227	158	ffvelrnda 6500	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
228	226, 227	syldan 579	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵)
229	224	difeq1d 3878	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
230	229	eleq2d 2836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
231	230	biimpar 463	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
232		simpll 750	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝜑)
233	232, 51	sylan 569	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
234	231, 233	syldan 579	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
235		f1of 6276	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻 → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
236	161, 162, 235	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
237		fvco3 6415	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
238	236, 237	sylan 569	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
239	209, 211, 147, 212, 161, 222, 223, 228, 234, 238	seqcoll2 13444	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
240	143, 207, 239	3eqtr4d 2815	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
241	240	expr 444	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
242	241	exlimdv 2013	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
243	134, 242	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
244	109, 243	eqtr4d 2808	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
245	244	ex 397	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
246	245	rexlimdvw 3182	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
247	246	rexlimdvw 3182	. . . 4 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
248	81, 247	syl5bi 232	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
249		suppssdm 7457	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻)
250	32, 249	eqsstri 3784	. . . . . . . . . 10 ⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻)
251		fdm 6189	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵 → dom (𝐹 ∘ 𝐻) = (1...𝑀))
252	30, 251	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝐹 ∘ 𝐻) = (1...𝑀))
253	250, 252	syl5sseq 3802	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ⊆ (1...𝑀))
254		fzssuz 12582	. . . . . . . . . . 11 ⊢ (1...𝑀) ⊆ (ℤ≥‘1)
255	254, 69	sseqtr4i 3787	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ ℕ
256		nnssre 11224	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
257	255, 256	sstri 3761	. . . . . . . . 9 ⊢ (1...𝑀) ⊆ ℝ
258	253, 257	syl6ss 3764	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ ℝ)
259		soss 5188	. . . . . . . 8 ⊢ (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
260	258, 120, 259	mpisyl 21	. . . . . . 7 ⊢ (𝜑 → < Or 𝑊)
261		ssfi 8334	. . . . . . . 8 ⊢ (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
262	123, 253, 261	sylancr 575	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
263		fz1iso 13441	. . . . . . 7 ⊢ (( < Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
264	260, 262, 263	syl2anc 573	. . . . . 6 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
265	264	ad2antrr 705	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
266	61, 3, 64, 151, 1, 2, 7, 148, 68, 10, 49, 32	gsumval3lem2 18507	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
267	1	ad2antrr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
268	267, 208	sylan 569	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
269	267, 210	sylan 569	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
270	267, 146	sylan 569	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
271	267, 62	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ 𝐵)
272		simprr 756	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
273		simplr 752	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
274	253	ad2antrr 705	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
275	30	ad2antrr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
276	275	ffvelrnda 6500	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵)
277	33	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
278		ovexd 6823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
279	36	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
280	275, 277, 278, 279	suppssr 7476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
281		coass 5796	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
282	281	fveq1i 6331	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦)
283		isof1o 6714	. . . . . . . . . . . 12 ⊢ (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)
284		f1of 6276	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊)
285	272, 283, 284	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
286		fvco3 6415	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
287	285, 286	sylan 569	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
288	282, 287	syl5eqr 2819	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
289	268, 269, 270, 271, 272, 273, 274, 276, 280, 288	seqcoll2 13444	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
290	266, 289	eqtr4d 2808	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
291	290	expr 444	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
292	291	exlimdv 2013	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
293	265, 292	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
294	293	ex 397	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
295	248, 294	pm2.61d 171	. 2 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
296	77, 295	pm2.61dane 3030	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  ∃wrex 3062  Vcvv 3351   ∖ cdif 3720   ⊆ wss 3723  ∅c0 4063  𝒫 cpw 4297  {csn 4316   class class class wbr 4786   ↦ cmpt 4863   I cid 5156   Or wor 5169   × cxp 5247  ^◡ccnv 5248  dom cdm 5249  ran crn 5250   ↾ cres 5251   ∘ ccom 5253  Rel wrel 5254   Fn wfn 6024  ⟶wf 6025  –1-1→wf1 6026  –onto→wfo 6027  –1-1-onto→wf1o 6028  ‘cfv 6029   Isom wiso 6030  (class class class)co 6791   supp csupp 7444   ≈ cen 8104  Fincfn 8107  ℝcr 10135  1c1 10137   < clt 10274  ℕcn 11220  ℕ₀cn0 11492  ℤcz 11577  ℤ_≥cuz 11886  ...cfz 12526  seqcseq 13001  ♯chash 13314  Basecbs 16057  +_gcplusg 16142  0_gc0g 16301   Σ_g cgsu 16302  Mndcmnd 17495  Cntzccntz 17948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-isom 6038  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-supp 7445  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-oadd 7715  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-oi 8569  df-card 8963  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-nn 11221  df-n0 11493  df-z 11578  df-uz 11887  df-fz 12527  df-fzo 12667  df-seq 13002  df-hash 13315  df-0g 16303  df-gsum 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-cntz 17950

This theorem is referenced by:  gsumzres  18510  gsumzcl2  18511  gsumzf1o  18513  gsumzaddlem  18521  gsumconst  18534  gsumzmhm  18537  gsumzoppg  18544  gsumfsum  20021  wilthlem3  25010