gsumval3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gsumval3		Structured version Visualization version GIF version

Theorem gsumval3 18131

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 = (0_g‘𝐺)
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 = (0_g‘𝐺)
4	3	gsumz 17197	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σ_g (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
5	1, 2, 4	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
6	5	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σ_g (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
7		gsumval3.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8	7	feqmptd 6159	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
10		gsumval3.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)
11		f1f 6014	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴)
12	10, 11	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴)
13	12	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14		f1f1orn 6061	. . . . . . . . . . . . . . . 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 6062	. . . . . . . . . . . . . 14 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → ^◡𝐻:ran 𝐻–1-1-onto→(1...𝑀))
18		f1of 6050	. . . . . . . . . . . . . 14 ⊢ (^◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ^◡𝐻:ran 𝐻⟶(1...𝑀))
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ^◡𝐻:ran 𝐻⟶(1...𝑀))
20	19	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (^◡𝐻‘𝑥) ∈ (1...𝑀))
21		fvco3 6185	. . . . . . . . . . . 12 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (^◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(^◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(^◡𝐻‘𝑥))))
22	13, 20, 21	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(^◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(^◡𝐻‘𝑥))))
23		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅)
24	23	difeq2d 3690	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25		dif0 3904	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑀) ∖ ∅) = (1...𝑀)
26	24, 25	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
28	20, 27	eleqtrrd 2691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (^◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29		fco 5971	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
30	7, 12, 29	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
31	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
32		gsumval3.w	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )
33	32	eqimss2i 3623	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊
34	33	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
35		ovex 6577	. . . . . . . . . . . . . 14 ⊢ (1...𝑀) ∈ V
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V)
37		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐺) ∈ V
38	3, 37	eqeltri 2684	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
39	38	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V)
40	31, 34, 36, 39	suppssr 7213	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (^◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(^◡𝐻‘𝑥)) = 0 )
41	28, 40	syldan 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(^◡𝐻‘𝑥)) = 0 )
42		f1ocnvfv2 6433	. . . . . . . . . . . . 13 ⊢ ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(^◡𝐻‘𝑥)) = 𝑥)
43	16, 42	sylan 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(^◡𝐻‘𝑥)) = 𝑥)
44	43	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(^◡𝐻‘𝑥))) = (𝐹‘𝑥))
45	22, 41, 44	3eqtr3rd 2653	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 )
46		fvex 6113	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
47	46	elsn 4140	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )
48	45, 47	sylibr 223	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
49	48	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
50		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
51		gsumval3.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
52	38	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ V)
53	7, 51, 2, 52	suppssr 7213	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
54	53, 47	sylibr 223	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
55	50, 54	sylan2br 492	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
56	55	adantlr 747	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 })
57	56	anassrs 678	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 })
58	49, 57	pm2.61dan 828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 })
59	58, 47	sylib 207	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 )
60	59	mpteq2dva 4672	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 ))
61	9, 60	eqtrd 2644	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
62	61	oveq2d 6565	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝑥 ∈ 𝐴 ↦ 0 )))
63		gsumval3.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐺)
64	63, 3	mndidcl 17131	. . . . . . 7 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
65	1, 64	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ∈ 𝐵)
66		gsumval3.p	. . . . . . 7 ⊢ + = (+_g‘𝐺)
67	63, 66, 3	mndlid 17134	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
68	1, 65, 67	syl2anc 691	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
69	68	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
70		gsumval3.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
71		nnuz 11599	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
72	70, 71	syl6eleq 2698	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
73	72	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈ (ℤ_≥‘1))
74	26	eleq2d 2673	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
75	74	biimpar 501	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
76	31, 34, 36, 39	suppssr 7213	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
77	75, 76	syldan 486	. . . 4 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
78	69, 73, 77	seqid3 12707	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 )
79	6, 62, 78	3eqtr4d 2654	. 2 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
80		fzf 12201	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
81		ffn 5958	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
82		ovelrn 6708	. . . . 5 ⊢ (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
83	80, 81, 82	mp2b 10	. . . 4 ⊢ (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
84	1	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
85		simpr 476	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
86		frel 5963	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
87		reldm0 5264	. . . . . . . . . . . . . . . . 17 ⊢ (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
88	7, 86, 87	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
89		fdm 5964	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
90	7, 89	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
91	90	eqeq1d 2612	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
92	88, 91	bitrd 267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
93		coeq1 5201	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻))
94		co01 5567	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∘ 𝐻) = ∅
95	93, 94	syl6eq 2660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅)
96	95	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0 ))
97		supp0 7187	. . . . . . . . . . . . . . . . . 18 ⊢ ( 0 ∈ V → (∅ supp 0 ) = ∅)
98	38, 97	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ supp 0 ) = ∅
99	96, 98	syl6eq 2660	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = ∅)
100	32, 99	syl5eq 2656	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = ∅ → 𝑊 = ∅)
101	92, 100	syl6bir 243	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
102	101	necon3d 2803	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
103	102	imp 444	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅)
104	103	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
105	85, 104	eqnetrrd 2850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
106		fzn0 12226	. . . . . . . . . 10 ⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ_≥‘𝑚))
107	105, 106	sylib 207	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ_≥‘𝑚))
108	7	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵)
109	85	feq2d 5944	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵))
110	108, 109	mpbid 221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
111	63, 66, 84, 107, 110	gsumval2 17103	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σ_g 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
112		frn 5966	. . . . . . . . . . . . . . 15 ⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴)
113	10, 11, 112	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐴)
114	113	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴)
115	114, 85	sseqtrd 3604	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
116		fzssuz 12253	. . . . . . . . . . . . 13 ⊢ (𝑚...𝑛) ⊆ (ℤ_≥‘𝑚)
117		uzssz 11583	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑚) ⊆ ℤ
118		zssre 11261	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
119	117, 118	sstri 3577	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑚) ⊆ ℝ
120	116, 119	sstri 3577	. . . . . . . . . . . 12 ⊢ (𝑚...𝑛) ⊆ ℝ
121	115, 120	syl6ss 3580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
122		ltso 9997	. . . . . . . . . . 11 ⊢ < Or ℝ
123		soss 4977	. . . . . . . . . . 11 ⊢ (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
124	121, 122, 123	mpisyl 21	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
125		fzfi 12633	. . . . . . . . . . . 12 ⊢ (1...𝑀) ∈ Fin
126	125	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
127		fex2 7014	. . . . . . . . . . . . . . 15 ⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V)
128	12, 126, 2, 127	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 ∈ V)
129		f1oen3g 7857	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
130	128, 15, 129	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻)
131		enfi 8061	. . . . . . . . . . . . 13 ⊢ ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
132	130, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
133	125, 132	mpbii 222	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
134	133	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
135		fz1iso 13103	. . . . . . . . . 10 ⊢ (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
136	124, 134, 135	syl2anc 691	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
137	70	nnnn0d 11228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
138		hashfz1 12996	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (#‘(1...𝑀)) = 𝑀)
139	137, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘(1...𝑀)) = 𝑀)
140		hashen 12997	. . . . . . . . . . . . . . . . 17 ⊢ (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
141	125, 133, 140	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
142	130, 141	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘(1...𝑀)) = (#‘ran 𝐻))
143	139, 142	eqtr3d 2646	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 = (#‘ran 𝐻))
144	143	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 = (#‘ran 𝐻))
145	144	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘ran 𝐻)))
146	1	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
147	63, 66	mndcl 17124	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
148	147	3expb 1258	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
149	146, 148	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
150		gsumval3.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
151	150	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
152	151	sselda 3568	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
153		gsumval3.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (Cntz‘𝐺)
154	66, 153	cntzi 17585	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
155	152, 154	sylan 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
156	155	anasss 677	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
157	63, 66	mndass 17125	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
158	146, 157	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
159	72	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ_≥‘1))
160	7	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵)
161		frn 5966	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
162	160, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵)
163		simprr 792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
164		isof1o 6473	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
165	163, 164	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
166	144	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(#‘ran 𝐻)))
167		f1oeq2 6041	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑀) = (1...(#‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
168	166, 167	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 ↔ 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
169	165, 168	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
170		f1ocnv 6062	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → ^◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
171	169, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ^◡𝑓:ran 𝐻–1-1-onto→(1...𝑀))
172	15	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
173		f1oco 6072	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (^◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
174	171, 172, 173	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (^◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
175		ffn 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
176		dffn4 6034	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
177	175, 176	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹)
178		fof 6028	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹)
179	160, 177, 178	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
180		f1of 6050	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻)
181	169, 180	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
182	113	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴)
183	181, 182	fssd 5970	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
184		fco 5971	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
185	179, 183, 184	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹)
186	185	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹)
187		f1ococnv2 6076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓 ∘ ^◡𝑓) = ( I ↾ ran 𝐻))
188	169, 187	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ^◡𝑓) = ( I ↾ ran 𝐻))
189	188	coeq1d 5205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ^◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
190		f1of 6050	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)–1-1-onto→ran 𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻)
191		fcoi2 5992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
192	172, 190, 191	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
193	189, 192	eqtr2d 2645	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ^◡𝑓) ∘ 𝐻))
194		coass 5571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∘ ^◡𝑓) ∘ 𝐻) = (𝑓 ∘ (^◡𝑓 ∘ 𝐻))
195	193, 194	syl6eq 2660	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (^◡𝑓 ∘ 𝐻)))
196	195	coeq2d 5206	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (^◡𝑓 ∘ 𝐻))))
197		coass 5571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (^◡𝑓 ∘ 𝐻)))
198	196, 197	syl6eqr 2662	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻)))
199	198	fveq1d 6105	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻))‘𝑘))
200	199	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻))‘𝑘))
201		f1of 6050	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ^◡𝑓:ran 𝐻⟶(1...𝑀))
202	169, 170, 201	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ^◡𝑓:ran 𝐻⟶(1...𝑀))
203	172, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
204		fco 5971	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (^◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
205	202, 203, 204	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (^◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀))
206		fvco3 6185	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((^◡𝑓 ∘ 𝐻)‘𝑘)))
207	205, 206	sylan 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (^◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((^◡𝑓 ∘ 𝐻)‘𝑘)))
208	200, 207	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((^◡𝑓 ∘ 𝐻)‘𝑘)))
209	149, 156, 158, 159, 162, 174, 186, 208	seqf1o 12704	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀))
210	63, 66, 3	mndlid 17134	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
211	146, 210	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
212	63, 66, 3	mndrid 17135	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
213	146, 212	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
214	146, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 0 ∈ 𝐵)
215		fdm 5964	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
216	10, 11, 215	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = (1...𝑀))
217		eluzfz1 12219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑀))
218		ne0i 3880	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
219	72, 217, 218	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
220	216, 219	eqnetrd 2849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐻 ≠ ∅)
221		dm0rn0 5263	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
222	221	necon3bii 2834	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
223	220, 222	sylib 207	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐻 ≠ ∅)
224	223	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
225	115	adantrr 749	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
226		simprl 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
227	226	eleq2d 2673	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛)))
228	227	biimpar 501	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴)
229	160	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
230	228, 229	syldan 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵)
231	226	difeq1d 3689	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
232	231	eleq2d 2673	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
233	232	biimpar 501	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
234		simpll 786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝜑)
235	234, 53	sylan 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
236	233, 235	syldan 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 )
237		f1of 6050	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻 → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
238	163, 164, 237	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
239		fvco3 6185	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
240	238, 239	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦)))
241	211, 213, 149, 214, 163, 224, 225, 230, 236, 240	seqcoll2 13106	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘ran 𝐻)))
242	145, 209, 241	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
243	242	expr 641	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
244	243	exlimdv 1848	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
245	136, 244	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
246	111, 245	eqtr4d 2647	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
247	246	ex 449	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
248	247	rexlimdvw 3016	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
249	248	rexlimdvw 3016	. . . 4 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
250	83, 249	syl5bi 231	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
251		suppssdm 7195	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻)
252	32, 251	eqsstri 3598	. . . . . . . . . 10 ⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻)
253		fdm 5964	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵 → dom (𝐹 ∘ 𝐻) = (1...𝑀))
254	30, 253	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝐹 ∘ 𝐻) = (1...𝑀))
255	252, 254	syl5sseq 3616	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ⊆ (1...𝑀))
256		fzssuz 12253	. . . . . . . . . . 11 ⊢ (1...𝑀) ⊆ (ℤ_≥‘1)
257	256, 71	sseqtr4i 3601	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ ℕ
258		nnssre 10901	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
259	257, 258	sstri 3577	. . . . . . . . 9 ⊢ (1...𝑀) ⊆ ℝ
260	255, 259	syl6ss 3580	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ ℝ)
261		soss 4977	. . . . . . . 8 ⊢ (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
262	260, 122, 261	mpisyl 21	. . . . . . 7 ⊢ (𝜑 → < Or 𝑊)
263		ssfi 8065	. . . . . . . 8 ⊢ (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
264	125, 255, 263	sylancr 694	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
265		fz1iso 13103	. . . . . . 7 ⊢ (( < Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
266	262, 264, 265	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
267	266	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
268	63, 3, 66, 153, 1, 2, 7, 150, 70, 10, 51, 32	gsumval3lem2 18130	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)))
269	1	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
270	269, 210	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)
271	269, 212	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)
272	269, 148	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
273	269, 64	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0 ∈ 𝐵)
274		simprr 792	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
275		simplr 788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
276	255	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
277	30	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵)
278	277	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵)
279	33	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊)
280	35	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
281	38	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0 ∈ V)
282	277, 279, 280, 281	suppssr 7213	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 )
283		coass 5571	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
284	283	fveq1i 6104	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦)
285		isof1o 6473	. . . . . . . . . . . 12 ⊢ (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)
286		f1of 6050	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))⟶𝑊)
287	274, 285, 286	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝑊)
288		fvco3 6185	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(#‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
289	287, 288	sylan 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
290	284, 289	syl5eqr 2658	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦)))
291	270, 271, 272, 273, 274, 275, 276, 278, 282, 290	seqcoll2 13106	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)))
292	268, 291	eqtr4d 2647	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
293	292	expr 641	. . . . . 6 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
294	293	exlimdv 1848	. . . . 5 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
295	267, 294	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
296	295	ex 449	. . 3 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)))
297	250, 296	pm2.61d 169	. 2 ⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
298	79, 297	pm2.61dane 2869	1 ⊢ (𝜑 → (𝐺 Σ_g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ≠ wne 2780 ∃wrex 2897 Vcvv 3173 ∖ cdif 3537 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 I cid 4948 Or wor 4958 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 ↾ cres 5040 ∘ ccom 5042 Rel wrel 5043 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 Isom wiso 5805 (class class class)co 6549 supp csupp 7182 ≈ cen 7838 Fincfn 7841 ℝcr 9814 1c1 9816 < clt 9953 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 seqcseq 12663 #chash 12979 Basecbs 15695 +_gcplusg 15768 0_gc0g 15923 Σ_g cgsu 15924 Mndcmnd 17117 Cntzccntz 17571

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-oi 8298 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-seq 12664 df-hash 12980 df-0g 15925 df-gsum 15926 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-cntz 17573

This theorem is referenced by: gsumzres 18133 gsumzcl2 18134 gsumzf1o 18136 gsumzaddlem 18144 gsumconst 18157 gsumzmhm 18160 gsumzoppg 18167 gsumfsum 19632 wilthlem3 24596

W3C validator