Theorem gsumval3 19517

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 18483	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
5	1, 2, 4	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
6	5	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
7		gsumval3.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8	7	feqmptd 6846	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
9	8	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
10		gsumval3.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
11		f1f 6679	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴)
12	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴)
13	12	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14		f1f1orn 6736	. . . . . . . . . . . . . . . 16 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
15	10, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
16	15	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17		f1ocnv 6737	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀))
18		f1of 6725	. . . . . . . . . . . . . 14 ⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀))
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀))
20	19	ffvelrnda 6970	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀))
21		fvco3 6876	. . . . . . . . . . . 12 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
22	13, 20, 21	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
23		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅)
24	23	difeq2d 4058	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25		dif0 4307	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑀) ∖ ∅) = (1...𝑀)
26	24, 25	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
27	26	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
28	20, 27	eleqtrrd 2843	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29		fco 6633	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
30	7, 12, 29	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
31	30	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
32		gsumval3.w	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )
33	32	eqimss2i 3981	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊
34	33	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
35		ovexd 7319	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V)
36	3	fvexi 6797	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
37	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V)
38	31, 34, 35, 37	suppssr 8021	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
39	28, 38	syldan 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
40		f1ocnvfv2 7158	. . . . . . . . . . . . 13 ⊢ ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
41	16, 40	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
42	41	fveq2d 6787	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥))
43	22, 39, 42	3eqtr3rd 2788	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 )
44		fvex 6796	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
45	44	elsn 4577	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )
46	43, 45	sylibr 233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
47	46	adantlr 712	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
48		eldif 3898	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49		gsumval3.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
50	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ V)
51	7, 49, 2, 50	suppssr 8021	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
52	51, 45	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
53	48, 52	sylan2br 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
54	53	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
55	54	anassrs 468	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
56	47, 55	pm2.61dan 810	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 })
57	56, 45	sylib 217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 )
58	57	mpteq2dva 5175	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 ))
59	9, 58	eqtrd 2779	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
60	59	oveq2d 7300	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
61		gsumval3.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
62	61, 3	mndidcl 18409	. . . . . 6 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
63		gsumval3.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
64	61, 63, 3	mndlid 18414	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
65	1, 62, 64	syl2anc2 585	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
66	65	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
67		gsumval3.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
68		nnuz 12630	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
69	67, 68	eleqtrdi 2850	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
70	69	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈ (ℤ≥‘1))
71	26	eleq2d 2825	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
72	71	biimpar 478	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
73	31, 34, 35, 37	suppssr 8021	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
74	72, 73	syldan 591	. . . 4 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
75	66, 70, 74	seqid3 13776	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 )
76	6, 60, 75	3eqtr4d 2789	. 2 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
77		fzf 13252	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
78		ffn 6609	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
79		ovelrn 7457	. . . . 5 ⊢ (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
80	77, 78, 79	mp2b 10	. . . 4 ⊢ (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
81	1	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
82		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
83		frel 6614	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
84		reldm0 5840	. . . . . . . . . . . . . . . . 17 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
85	7, 83, 84	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
86	7	fdmd 6620	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
87	86	eqeq1d 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
88	85, 87	bitrd 278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
89		coeq1 5769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻))
90		co01 6169	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∘ 𝐻) = ∅
91	89, 90	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅)
92	91	oveq1d 7299	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0 ))
93		supp0 7991	. . . . . . . . . . . . . . . . . 18 ⊢ ( 0 ∈ V → (∅ supp 0 ) = ∅)
94	36, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ supp 0 ) = ∅
95	92, 94	eqtrdi 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = ∅)
96	32, 95	eqtrid 2791	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = ∅ → 𝑊 = ∅)
97	88, 96	syl6bir 253	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
98	97	necon3d 2965	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
99	98	imp 407	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅)
100	99	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
101	82, 100	eqnetrrd 3013	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
102		fzn0 13279	. . . . . . . . . 10 ⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚))
103	101, 102	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚))
104	7	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵)
105	82	feq2d 6595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵))
106	104, 105	mpbid 231	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
107	61, 63, 81, 103, 106	gsumval2 18379	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
108		frn 6616	. . . . . . . . . . . . . . 15 ⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴)
109	10, 11, 108	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐴)
110	109	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴)
111	110, 82	sseqtrd 3962	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
112		fzssuz 13306	. . . . . . . . . . . . 13 ⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚)
113		uzssz 12612	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑚) ⊆ ℤ
114		zssre 12335	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
115	113, 114	sstri 3931	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑚) ⊆ ℝ
116	112, 115	sstri 3931	. . . . . . . . . . . 12 ⊢ (𝑚...𝑛) ⊆ ℝ
117	111, 116	sstrdi 3934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
118		ltso 11064	. . . . . . . . . . 11 ⊢ < Or ℝ
119		soss 5524	. . . . . . . . . . 11 ⊢ (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
120	117, 118, 119	mpisyl 21	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
121		fzfi 13701	. . . . . . . . . . . 12 ⊢ (1...𝑀) ∈ Fin
122	121	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
123	12, 122	fexd 7112	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 ∈ V)
124		f1oen3g 8763	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
125	123, 15, 124	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻)
126		enfi 8982	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
127	125, 126	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
128	121, 127	mpbii 232	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
129	128	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
130		fz1iso 14185	. . . . . . . . . 10 ⊢ (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
131	120, 129, 130	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
132	67	nnnn0d 12302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
133		hashfz1 14069	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
134	132, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
135	122, 15	hasheqf1od 14077	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
136	134, 135	eqtr3d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻))
137	136	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
138	137	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
139	1	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
140	61, 63	mndcl 18402	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
141	140	3expb 1119	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
142	139, 141	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
143		gsumval3.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
144	143	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
145	144	sselda 3922	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
146		gsumval3.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (Cntz‘𝐺)
147	63, 146	cntzi 18944	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
148	145, 147	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
149	148	anasss 467	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
150	61, 63	mndass 18403	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
151	139, 150	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
152	69	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ≥‘1))
153	7	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵)
154	153	frnd 6617	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵)
155		simprr 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
156		isof1o 7203	. . . . . . . . . . . . . . . . 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 7300	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
159	158	f1oeq2d 6721	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
160	157, 159	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
161		f1ocnv 6737	. . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
164		f1oco 6748	. . . . . . . . . . . . . 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 6609	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
167		dffn4 6703	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
168	166, 167	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹)
169		fof 6697	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹)
170	153, 168, 169	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
171		f1of 6725	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻)
172	160, 171	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
173	109	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴)
174	172, 173	fssd 6627	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
175		fco 6633	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
176	170, 174, 175	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
177	176	ffvelrnda 6970	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹)
178		f1ococnv2 6752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
179	160, 178	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
180	179	coeq1d 5773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
181		f1of 6725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻)
182		fcoi2 6658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
183	163, 181, 182	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
184	180, 183	eqtr2d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻))
185		coass 6173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻))
186	184, 185	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
187	186	coeq2d 5774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))))
188		coass 6173	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
189	187, 188	eqtr4di 2797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)))
190	189	fveq1d 6785	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
191	190	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
192		f1of 6725	. . . . . . . . . . . . . . . . 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 6633	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
196	193, 194, 195	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
197		fvco3 6876	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
198	196, 197	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
199	191, 198	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
200	142, 149, 151, 152, 154, 165, 177, 199	seqf1o 13773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀))
201	61, 63, 3	mndlid 18414	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
202	139, 201	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
203	61, 63, 3	mndrid 18415	. . . . . . . . . . . . . 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 6618	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
207	10, 11, 206	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = (1...𝑀))
208		eluzfz1 13272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑀))
209		ne0i 4269	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
210	69, 208, 209	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
211	207, 210	eqnetrd 3012	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐻 ≠ ∅)
212		dm0rn0 5837	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
213	212	necon3bii 2997	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
214	211, 213	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ≠ ∅)
215	214	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
216	111	adantrr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
217		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
218	217	eleq2d 2825	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛)))
219	218	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴)
220	153	ffvelrnda 6970	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
221	219, 220	syldan 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵)
222	217	difeq1d 4057	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
223	222	eleq2d 2825	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
224	223	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
225	51	ad4ant14 749	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
226	224, 225	syldan 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
227		f1of 6725	. . . . . . . . . . . . . . 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 6876	. . . . . . . . . . . . . 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 14188	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
232	138, 200, 231	3eqtr4d 2789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
233	232	expr 457	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
234	233	exlimdv 1937	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
235	131, 234	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
236	107, 235	eqtr4d 2782	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
237	236	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
238	237	rexlimdvw 3220	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
239	238	rexlimdvw 3220	. . . 4 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
240	80, 239	syl5bi 241	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
241		suppssdm 8002	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻)
242	32, 241	eqsstri 3956	. . . . . . . . . 10 ⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻)
243	242, 30	fssdm 6629	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ⊆ (1...𝑀))
244		fz1ssnn 13296	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ ℕ
245		nnssre 11986	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
246	244, 245	sstri 3931	. . . . . . . . 9 ⊢ (1...𝑀) ⊆ ℝ
247	243, 246	sstrdi 3934	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ ℝ)
248		soss 5524	. . . . . . . 8 ⊢ (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
249	247, 118, 248	mpisyl 21	. . . . . . 7 ⊢ (𝜑 → < Or 𝑊)
250		ssfi 8965	. . . . . . . 8 ⊢ (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
251	121, 243, 250	sylancr 587	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
252		fz1iso 14185	. . . . . . 7 ⊢ (( < Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
253	249, 251, 252	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
254	253	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
255	61, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32	gsumval3lem2 19516	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
256	1	ad2antrr 723	. . . . . . . . . 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 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
262		simplr 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
263	243	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
264	30	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
265	264	ffvelrnda 6970	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵)
266	33	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
267		ovexd 7319	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
268	36	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
269	264, 266, 267, 268	suppssr 8021	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
270		coass 6173	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
271	270	fveq1i 6784	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦)
272		isof1o 7203	. . . . . . . . . . . 12 ⊢ (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)
273		f1of 6725	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊)
274	261, 272, 273	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
275		fvco3 6876	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
276	274, 275	sylan 580	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
277	271, 276	eqtr3id 2793	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
278	257, 258, 259, 260, 261, 262, 263, 265, 269, 277	seqcoll2 14188	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
279	255, 278	eqtr4d 2782	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
280	279	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
281	280	exlimdv 1937	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
282	254, 281	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
283	282	ex 413	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
284	240, 283	pm2.61d 179	. 2 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
285	76, 284	pm2.61dane 3033	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2107   ≠ wne 2944  ∃wrex 3066  Vcvv 3433   ∖ cdif 3885   ⊆ wss 3888  ∅c0 4257  𝒫 cpw 4534  {csn 4562   class class class wbr 5075   ↦ cmpt 5158   I cid 5489   Or wor 5503   × cxp 5588  ^◡ccnv 5589  dom cdm 5590  ran crn 5591   ↾ cres 5592   ∘ ccom 5594  Rel wrel 5595   Fn wfn 6432  ⟶wf 6433  –1-1→wf1 6434  –onto→wfo 6435  –1-1-onto→wf1o 6436  ‘cfv 6437   Isom wiso 6438  (class class class)co 7284   supp csupp 7986   ≈ cen 8739  Fincfn 8742  ℝcr 10879  1c1 10881   < clt 11018  ℕcn 11982  ℕ₀cn0 12242  ℤcz 12328  ℤ_≥cuz 12591  ...cfz 13248  seqcseq 13730  ♯chash 14053  Basecbs 16921  +_gcplusg 16971  0_gc0g 17159   Σ_g cgsu 17160  Mndcmnd 18394  Cntzccntz 18930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329  df-uz 12592  df-fz 13249  df-fzo 13392  df-seq 13731  df-hash 14054  df-0g 17161  df-gsum 17162  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-cntz 18932

This theorem is referenced by:  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  gsumfsum  20674  wilthlem3  26228