Theorem gsumval3 19836

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 18761	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
5	1, 2, 4	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
6	5	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
7		gsumval3.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8	7	feqmptd 6902	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
10		gsumval3.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
11		f1f 6730	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴)
12	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴)
13	12	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14		f1f1orn 6785	. . . . . . . . . . . . . . . 16 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
15	10, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
16	15	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17		f1ocnv 6786	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀))
18		f1of 6774	. . . . . . . . . . . . . 14 ⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀))
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀))
20	19	ffvelcdmda 7029	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀))
21		fvco3 6933	. . . . . . . . . . . 12 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
22	13, 20, 21	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
23		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅)
24	23	difeq2d 4078	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25		dif0 4330	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑀) ∖ ∅) = (1...𝑀)
26	24, 25	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
28	20, 27	eleqtrrd 2839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29		fco 6686	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
30	7, 12, 29	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
31	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
32		gsumval3.w	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )
33	32	eqimss2i 3995	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊
34	33	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
35		ovexd 7393	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V)
36	3	fvexi 6848	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
37	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V)
38	31, 34, 35, 37	suppssr 8137	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
39	28, 38	syldan 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
40		f1ocnvfv2 7223	. . . . . . . . . . . . 13 ⊢ ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
41	16, 40	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
42	41	fveq2d 6838	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥))
43	22, 39, 42	3eqtr3rd 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 )
44		fvex 6847	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
45	44	elsn 4595	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )
46	43, 45	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
47	46	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
48		eldif 3911	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49		gsumval3.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
50	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ V)
51	7, 49, 2, 50	suppssr 8137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
52	51, 45	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
53	48, 52	sylan2br 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
54	53	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
55	54	anassrs 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
56	47, 55	pm2.61dan 812	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 })
57	56, 45	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 )
58	57	mpteq2dva 5191	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 ))
59	9, 58	eqtrd 2771	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
60	59	oveq2d 7374	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
61		gsumval3.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
62	61, 3	mndidcl 18674	. . . . . 6 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
63		gsumval3.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
64	61, 63, 3	mndlid 18679	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
65	1, 62, 64	syl2anc2 585	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
66	65	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
67		gsumval3.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
68		nnuz 12790	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
69	67, 68	eleqtrdi 2846	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
70	69	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈ (ℤ≥‘1))
71	26	eleq2d 2822	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
72	71	biimpar 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
73	31, 34, 35, 37	suppssr 8137	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
74	72, 73	syldan 591	. . . 4 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
75	66, 70, 74	seqid3 13969	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 )
76	6, 60, 75	3eqtr4d 2781	. 2 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
77		fzf 13427	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
78		ffn 6662	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
79		ovelrn 7534	. . . . 5 ⊢ (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
80	77, 78, 79	mp2b 10	. . . 4 ⊢ (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
81	1	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
82		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
83		frel 6667	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
84		reldm0 5877	. . . . . . . . . . . . . . . . 17 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
85	7, 83, 84	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
86	7	fdmd 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
87	86	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
88	85, 87	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
89		coeq1 5806	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻))
90		co01 6220	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∘ 𝐻) = ∅
91	89, 90	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅)
92	91	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0 ))
93		supp0 8107	. . . . . . . . . . . . . . . . . 18 ⊢ ( 0 ∈ V → (∅ supp 0 ) = ∅)
94	36, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ supp 0 ) = ∅
95	92, 94	eqtrdi 2787	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = ∅)
96	32, 95	eqtrid 2783	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = ∅ → 𝑊 = ∅)
97	88, 96	biimtrrdi 254	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
98	97	necon3d 2953	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
99	98	imp 406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅)
100	99	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
101	82, 100	eqnetrrd 3000	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
102		fzn0 13454	. . . . . . . . . 10 ⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚))
103	101, 102	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚))
104	7	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵)
105	82	feq2d 6646	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵))
106	104, 105	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
107	61, 63, 81, 103, 106	gsumval2 18611	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
108		frn 6669	. . . . . . . . . . . . . . 15 ⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴)
109	10, 11, 108	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐴)
110	109	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴)
111	110, 82	sseqtrd 3970	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
112		fzssuz 13481	. . . . . . . . . . . . 13 ⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚)
113		uzssz 12772	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑚) ⊆ ℤ
114		zssre 12495	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
115	113, 114	sstri 3943	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑚) ⊆ ℝ
116	112, 115	sstri 3943	. . . . . . . . . . . 12 ⊢ (𝑚...𝑛) ⊆ ℝ
117	111, 116	sstrdi 3946	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
118		ltso 11213	. . . . . . . . . . 11 ⊢ < Or ℝ
119		soss 5552	. . . . . . . . . . 11 ⊢ (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
120	117, 118, 119	mpisyl 21	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
121		fzfi 13895	. . . . . . . . . . . 12 ⊢ (1...𝑀) ∈ Fin
122	121	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
123	12, 122	fexd 7173	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 ∈ V)
124		f1oen3g 8903	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
125	123, 15, 124	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻)
126		enfi 9111	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
127	125, 126	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
128	121, 127	mpbii 233	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
129	128	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
130		fz1iso 14385	. . . . . . . . . 10 ⊢ (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
131	120, 129, 130	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
132	67	nnnn0d 12462	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
133		hashfz1 14269	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
134	132, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
135	122, 15	hasheqf1od 14276	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
136	134, 135	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻))
137	136	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
138	137	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
139	1	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
140	61, 63	mndcl 18667	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
141	140	3expb 1120	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
142	139, 141	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
143		gsumval3.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
144	143	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
145	144	sselda 3933	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
146		gsumval3.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (Cntz‘𝐺)
147	63, 146	cntzi 19258	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
148	145, 147	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
149	148	anasss 466	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
150	61, 63	mndass 18668	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
151	139, 150	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
152	69	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ≥‘1))
153	7	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵)
154	153	frnd 6670	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵)
155		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
156		isof1o 7269	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
157	155, 156	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
158	137	oveq2d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
159	158	f1oeq2d 6770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
160	157, 159	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
161		f1ocnv 6786	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
162	160, 161	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
163	15	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
164		f1oco 6797	. . . . . . . . . . . . . 14 ⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
165	162, 163, 164	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
166		ffn 6662	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
167		dffn4 6752	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
168	166, 167	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹)
169		fof 6746	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹)
170	153, 168, 169	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
171		f1of 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻)
172	160, 171	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
173	109	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴)
174	172, 173	fssd 6679	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
175		fco 6686	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
176	170, 174, 175	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
177	176	ffvelcdmda 7029	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹)
178		f1ococnv2 6801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
179	160, 178	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
180	179	coeq1d 5810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
181		f1of 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻)
182		fcoi2 6709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
183	163, 181, 182	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
184	180, 183	eqtr2d 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻))
185		coass 6224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻))
186	184, 185	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
187	186	coeq2d 5811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))))
188		coass 6224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
189	187, 188	eqtr4di 2789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)))
190	189	fveq1d 6836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
191	190	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
192		f1of 6774	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀))
193	160, 161, 192	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀))
194	163, 181	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
195		fco 6686	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
196	193, 194, 195	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
197		fvco3 6933	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
198	196, 197	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
199	191, 198	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
200	142, 149, 151, 152, 154, 165, 177, 199	seqf1o 13966	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀))
201	61, 63, 3	mndlid 18679	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
202	139, 201	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
203	61, 63, 3	mndrid 18680	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
204	139, 203	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
205	139, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 0 ∈ 𝐵)
206		fdm 6671	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
207	10, 11, 206	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = (1...𝑀))
208		eluzfz1 13447	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑀))
209		ne0i 4293	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
210	69, 208, 209	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
211	207, 210	eqnetrd 2999	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐻 ≠ ∅)
212		dm0rn0 5873	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
213	212	necon3bii 2984	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
214	211, 213	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ≠ ∅)
215	214	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
216	111	adantrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
217		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
218	217	eleq2d 2822	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛)))
219	218	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴)
220	153	ffvelcdmda 7029	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
221	219, 220	syldan 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵)
222	217	difeq1d 4077	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
223	222	eleq2d 2822	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
224	223	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
225	51	ad4ant14 752	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
226	224, 225	syldan 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
227		f1of 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻 → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
228	155, 156, 227	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
229		fvco3 6933	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
230	228, 229	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
231	202, 204, 142, 205, 155, 215, 216, 221, 226, 230	seqcoll2 14388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
232	138, 200, 231	3eqtr4d 2781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
233	232	expr 456	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
234	233	exlimdv 1934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
235	131, 234	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
236	107, 235	eqtr4d 2774	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
237	236	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
238	237	rexlimdvw 3142	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
239	238	rexlimdvw 3142	. . . 4 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
240	80, 239	biimtrid 242	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
241		suppssdm 8119	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻)
242	32, 241	eqsstri 3980	. . . . . . . . . 10 ⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻)
243	242, 30	fssdm 6681	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ⊆ (1...𝑀))
244		fz1ssnn 13471	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ ℕ
245		nnssre 12149	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
246	244, 245	sstri 3943	. . . . . . . . 9 ⊢ (1...𝑀) ⊆ ℝ
247	243, 246	sstrdi 3946	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ ℝ)
248		soss 5552	. . . . . . . 8 ⊢ (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
249	247, 118, 248	mpisyl 21	. . . . . . 7 ⊢ (𝜑 → < Or 𝑊)
250		ssfi 9097	. . . . . . . 8 ⊢ (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
251	121, 243, 250	sylancr 587	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
252		fz1iso 14385	. . . . . . 7 ⊢ (( < Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
253	249, 251, 252	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
254	253	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
255	61, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32	gsumval3lem2 19835	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
256	1	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
257	256, 201	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
258	256, 203	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
259	256, 141	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
260	256, 62	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ 𝐵)
261		simprr 772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
262		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
263	243	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
264	30	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
265	264	ffvelcdmda 7029	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵)
266	33	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
267		ovexd 7393	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
268	36	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
269	264, 266, 267, 268	suppssr 8137	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
270		coass 6224	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
271	270	fveq1i 6835	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦)
272		isof1o 7269	. . . . . . . . . . . 12 ⊢ (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)
273		f1of 6774	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊)
274	261, 272, 273	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
275		fvco3 6933	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
276	274, 275	sylan 580	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
277	271, 276	eqtr3id 2785	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
278	257, 258, 259, 260, 261, 262, 263, 265, 269, 277	seqcoll2 14388	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
279	255, 278	eqtr4d 2774	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
280	279	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
281	280	exlimdv 1934	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
282	254, 281	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
283	282	ex 412	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
284	240, 283	pm2.61d 179	. 2 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
285	76, 284	pm2.61dane 3019	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∃wrex 3060  Vcvv 3440   ∖ cdif 3898   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554  {csn 4580   class class class wbr 5098   ↦ cmpt 5179   I cid 5518   Or wor 5531   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   ↾ cres 5626   ∘ ccom 5628  Rel wrel 5629   Fn wfn 6487  ⟶wf 6488  –1-1→wf1 6489  –onto→wfo 6490  –1-1-onto→wf1o 6491  ‘cfv 6492   Isom wiso 6493  (class class class)co 7358   supp csupp 8102   ≈ cen 8880  Fincfn 8883  ℝcr 11025  1c1 11027   < clt 11166  ℕcn 12145  ℕ₀cn0 12401  ℤcz 12488  ℤ_≥cuz 12751  ...cfz 13423  seqcseq 13924  ♯chash 14253  Basecbs 17136  +_gcplusg 17177  0_gc0g 17359   Σ_g cgsu 17360  Mndcmnd 18659  Cntzccntz 19244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9415  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489  df-uz 12752  df-fz 13424  df-fzo 13571  df-seq 13925  df-hash 14254  df-0g 17361  df-gsum 17362  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-cntz 19246

This theorem is referenced by:  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  gsumfsum  21389  wilthlem3  27036