Theorem gsumval3 19786

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 18710	. . . . 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 6891	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
10		gsumval3.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
11		f1f 6720	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴)
12	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴)
13	12	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14		f1f1orn 6775	. . . . . . . . . . . . . . . 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 6776	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀))
18		f1of 6764	. . . . . . . . . . . . . 14 ⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀))
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀))
20	19	ffvelcdmda 7018	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀))
21		fvco3 6922	. . . . . . . . . . . 12 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
22	13, 20, 21	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥))))
23		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅)
24	23	difeq2d 4077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25		dif0 4329	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑀) ∖ ∅) = (1...𝑀)
26	24, 25	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
28	20, 27	eleqtrrd 2831	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29		fco 6676	. . . . . . . . . . . . . . 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 3997	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊
34	33	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
35		ovexd 7384	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V)
36	3	fvexi 6836	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
37	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V)
38	31, 34, 35, 37	suppssr 8128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
39	28, 38	syldan 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 )
40		f1ocnvfv2 7214	. . . . . . . . . . . . 13 ⊢ ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
41	16, 40	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥)
42	41	fveq2d 6826	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥))
43	22, 39, 42	3eqtr3rd 2773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 )
44		fvex 6835	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
45	44	elsn 4592	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )
46	43, 45	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
47	46	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
48		eldif 3913	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49		gsumval3.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
50	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ V)
51	7, 49, 2, 50	suppssr 8128	. . . . . . . . . . . 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 5185	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 ))
59	9, 58	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
60	59	oveq2d 7365	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
61		gsumval3.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
62	61, 3	mndidcl 18623	. . . . . 6 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
63		gsumval3.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
64	61, 63, 3	mndlid 18628	. . . . . 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 12778	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
69	67, 68	eleqtrdi 2838	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
70	69	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈ (ℤ≥‘1))
71	26	eleq2d 2814	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
72	71	biimpar 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
73	31, 34, 35, 37	suppssr 8128	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
74	72, 73	syldan 591	. . . 4 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
75	66, 70, 74	seqid3 13953	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 )
76	6, 60, 75	3eqtr4d 2774	. 2 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
77		fzf 13414	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
78		ffn 6652	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
79		ovelrn 7525	. . . . 5 ⊢ (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
80	77, 78, 79	mp2b 10	. . . 4 ⊢ (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
81	1	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
82		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
83		frel 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
84		reldm0 5870	. . . . . . . . . . . . . . . . 17 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
85	7, 83, 84	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
86	7	fdmd 6662	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
87	86	eqeq1d 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
88	85, 87	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
89		coeq1 5800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻))
90		co01 6210	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∘ 𝐻) = ∅
91	89, 90	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅)
92	91	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0 ))
93		supp0 8098	. . . . . . . . . . . . . . . . . 18 ⊢ ( 0 ∈ V → (∅ supp 0 ) = ∅)
94	36, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ supp 0 ) = ∅
95	92, 94	eqtrdi 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = ∅)
96	32, 95	eqtrid 2776	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = ∅ → 𝑊 = ∅)
97	88, 96	biimtrrdi 254	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
98	97	necon3d 2946	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
99	98	imp 406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅)
100	99	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
101	82, 100	eqnetrrd 2993	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
102		fzn0 13441	. . . . . . . . . 10 ⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚))
103	101, 102	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚))
104	7	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵)
105	82	feq2d 6636	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵))
106	104, 105	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
107	61, 63, 81, 103, 106	gsumval2 18560	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
108		frn 6659	. . . . . . . . . . . . . . 15 ⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴)
109	10, 11, 108	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐴)
110	109	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴)
111	110, 82	sseqtrd 3972	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
112		fzssuz 13468	. . . . . . . . . . . . 13 ⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚)
113		uzssz 12756	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑚) ⊆ ℤ
114		zssre 12478	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
115	113, 114	sstri 3945	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑚) ⊆ ℝ
116	112, 115	sstri 3945	. . . . . . . . . . . 12 ⊢ (𝑚...𝑛) ⊆ ℝ
117	111, 116	sstrdi 3948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
118		ltso 11196	. . . . . . . . . . 11 ⊢ < Or ℝ
119		soss 5547	. . . . . . . . . . 11 ⊢ (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
120	117, 118, 119	mpisyl 21	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
121		fzfi 13879	. . . . . . . . . . . 12 ⊢ (1...𝑀) ∈ Fin
122	121	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
123	12, 122	fexd 7163	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 ∈ V)
124		f1oen3g 8892	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
125	123, 15, 124	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻)
126		enfi 9101	. . . . . . . . . . . . 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 14369	. . . . . . . . . 10 ⊢ (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
131	120, 129, 130	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
132	67	nnnn0d 12445	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
133		hashfz1 14253	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
134	132, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
135	122, 15	hasheqf1od 14260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
136	134, 135	eqtr3d 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻))
137	136	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
138	137	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
139	1	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
140	61, 63	mndcl 18616	. . . . . . . . . . . . . . 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 3935	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
146		gsumval3.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (Cntz‘𝐺)
147	63, 146	cntzi 19208	. . . . . . . . . . . . . . 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 18617	. . . . . . . . . . . . . 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 6660	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵)
155		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
156		isof1o 7260	. . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
159	158	f1oeq2d 6760	. . . . . . . . . . . . . . . 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 6776	. . . . . . . . . . . . . . 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 6787	. . . . . . . . . . . . . 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 6652	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
167		dffn4 6742	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
168	166, 167	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹)
169		fof 6736	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹)
170	153, 168, 169	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
171		f1of 6764	. . . . . . . . . . . . . . . . 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 6669	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
175		fco 6676	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
176	170, 174, 175	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
177	176	ffvelcdmda 7018	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹)
178		f1ococnv2 6791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
179	160, 178	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻))
180	179	coeq1d 5804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
181		f1of 6764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻)
182		fcoi2 6699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
183	163, 181, 182	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
184	180, 183	eqtr2d 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻))
185		coass 6214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻))
186	184, 185	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
187	186	coeq2d 5805	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))))
188		coass 6214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))
189	187, 188	eqtr4di 2782	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)))
190	189	fveq1d 6824	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
191	190	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘))
192		f1of 6764	. . . . . . . . . . . . . . . . 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 6676	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
196	193, 194, 195	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
197		fvco3 6922	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
198	196, 197	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
199	191, 198	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘)))
200	142, 149, 151, 152, 154, 165, 177, 199	seqf1o 13950	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀))
201	61, 63, 3	mndlid 18628	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
202	139, 201	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
203	61, 63, 3	mndrid 18629	. . . . . . . . . . . . . 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 6661	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
207	10, 11, 206	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = (1...𝑀))
208		eluzfz1 13434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (ℤ≥‘1) → 1 ∈ (1...𝑀))
209		ne0i 4292	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
210	69, 208, 209	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
211	207, 210	eqnetrd 2992	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐻 ≠ ∅)
212		dm0rn0 5867	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
213	212	necon3bii 2977	. . . . . . . . . . . . . . 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 2814	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛)))
219	218	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴)
220	153	ffvelcdmda 7018	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
221	219, 220	syldan 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵)
222	217	difeq1d 4076	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
223	222	eleq2d 2814	. . . . . . . . . . . . . . 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 6764	. . . . . . . . . . . . . . 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 6922	. . . . . . . . . . . . . 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 14372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻)))
232	138, 200, 231	3eqtr4d 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
233	232	expr 456	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
234	233	exlimdv 1933	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
235	131, 234	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
236	107, 235	eqtr4d 2767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
237	236	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
238	237	rexlimdvw 3135	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
239	238	rexlimdvw 3135	. . . 4 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
240	80, 239	biimtrid 242	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
241		suppssdm 8110	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻)
242	32, 241	eqsstri 3982	. . . . . . . . . 10 ⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻)
243	242, 30	fssdm 6671	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ⊆ (1...𝑀))
244		fz1ssnn 13458	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ ℕ
245		nnssre 12132	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
246	244, 245	sstri 3945	. . . . . . . . 9 ⊢ (1...𝑀) ⊆ ℝ
247	243, 246	sstrdi 3948	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ ℝ)
248		soss 5547	. . . . . . . 8 ⊢ (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
249	247, 118, 248	mpisyl 21	. . . . . . 7 ⊢ (𝜑 → < Or 𝑊)
250		ssfi 9087	. . . . . . . 8 ⊢ (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
251	121, 243, 250	sylancr 587	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
252		fz1iso 14369	. . . . . . 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 19785	. . . . . . . 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 7018	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵)
266	33	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
267		ovexd 7384	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
268	36	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
269	264, 266, 267, 268	suppssr 8128	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
270		coass 6214	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
271	270	fveq1i 6823	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦)
272		isof1o 7260	. . . . . . . . . . . 12 ⊢ (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)
273		f1of 6764	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊)
274	261, 272, 273	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
275		fvco3 6922	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
276	274, 275	sylan 580	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
277	271, 276	eqtr3id 2778	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
278	257, 258, 259, 260, 261, 262, 263, 265, 269, 277	seqcoll2 14372	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
279	255, 278	eqtr4d 2767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
280	279	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
281	280	exlimdv 1933	. . . . 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 3012	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  Vcvv 3436   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  {csn 4577   class class class wbr 5092   ↦ cmpt 5173   I cid 5513   Or wor 5526   × cxp 5617  ^◡ccnv 5618  dom cdm 5619  ran crn 5620   ↾ cres 5621   ∘ ccom 5623  Rel wrel 5624   Fn wfn 6477  ⟶wf 6478  –1-1→wf1 6479  –onto→wfo 6480  –1-1-onto→wf1o 6481  ‘cfv 6482   Isom wiso 6483  (class class class)co 7349   supp csupp 8093   ≈ cen 8869  Fincfn 8872  ℝcr 11008  1c1 11010   < clt 11149  ℕcn 12128  ℕ₀cn0 12384  ℤcz 12471  ℤ_≥cuz 12735  ...cfz 13410  seqcseq 13908  ♯chash 14237  Basecbs 17120  +_gcplusg 17161  0_gc0g 17343   Σ_g cgsu 17344  Mndcmnd 18608  Cntzccntz 19194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-supp 8094  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472  df-uz 12736  df-fz 13411  df-fzo 13558  df-seq 13909  df-hash 14238  df-0g 17345  df-gsum 17346  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-cntz 19196

This theorem is referenced by:  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  gsumfsum  21341  wilthlem3  26978