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

Theorem gsumval3 18354
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.
StepHypRef Expression
1 gsumval3.g . . . . 5 (𝜑𝐺 ∈ Mnd)
2 gsumval3.a . . . . 5 (𝜑𝐴𝑉)
3 gsumval3.0 . . . . . 6 0 = (0g𝐺)
43gsumz 17421 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
51, 2, 4syl2anc 694 . . . 4 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
65adantr 480 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
7 gsumval3.f . . . . . . 7 (𝜑𝐹:𝐴𝐵)
87feqmptd 6288 . . . . . 6 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
98adantr 480 . . . . 5 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
10 gsumval3.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...𝑀)–1-1𝐴)
11 f1f 6139 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)⟶𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (𝜑𝐻:(1...𝑀)⟶𝐴)
1312ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14 f1f1orn 6186 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1615adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17 f1ocnv 6187 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:ran 𝐻1-1-onto→(1...𝑀))
18 f1of 6175 . . . . . . . . . . . . . 14 (𝐻:ran 𝐻1-1-onto→(1...𝑀) → 𝐻:ran 𝐻⟶(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 𝐻:ran 𝐻⟶(1...𝑀))
2019ffvelrnda 6399 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ (1...𝑀))
21 fvco3 6314 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟶𝐴 ∧ (𝐻𝑥) ∈ (1...𝑀)) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
2213, 20, 21syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
23 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑊 = ∅) → 𝑊 = ∅)
2423difeq2d 3761 . . . . . . . . . . . . . . 15 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25 dif0 3983 . . . . . . . . . . . . . . 15 ((1...𝑀) ∖ ∅) = (1...𝑀)
2624, 25syl6eq 2701 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2726adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2820, 27eleqtrrd 2733 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29 fco 6096 . . . . . . . . . . . . . . 15 ((𝐹:𝐴𝐵𝐻:(1...𝑀)⟶𝐴) → (𝐹𝐻):(1...𝑀)⟶𝐵)
307, 12, 29syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻):(1...𝑀)⟶𝐵)
3130adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (𝐹𝐻):(1...𝑀)⟶𝐵)
32 gsumval3.w . . . . . . . . . . . . . . 15 𝑊 = ((𝐹𝐻) supp 0 )
3332eqimss2i 3693 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ 𝑊
3433a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
35 ovexd 6720 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (1...𝑀) ∈ V)
36 fvex 6239 . . . . . . . . . . . . . . 15 (0g𝐺) ∈ V
373, 36eqeltri 2726 . . . . . . . . . . . . . 14 0 ∈ V
3837a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 0 ∈ V)
3931, 34, 35, 38suppssr 7371 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
4028, 39syldan 486 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
41 f1ocnvfv2 6573 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4216, 41sylan 487 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4342fveq2d 6233 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(𝐻𝑥))) = (𝐹𝑥))
4422, 40, 433eqtr3rd 2694 . . . . . . . . . 10 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) = 0 )
45 fvex 6239 . . . . . . . . . . 11 (𝐹𝑥) ∈ V
4645elsn 4225 . . . . . . . . . 10 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
4744, 46sylibr 224 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
4847adantlr 751 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
49 eldif 3617 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
50 gsumval3.n . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
5137a1i 11 . . . . . . . . . . . . 13 (𝜑0 ∈ V)
527, 50, 2, 51suppssr 7371 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
5352, 46sylibr 224 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5449, 53sylan2br 492 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5554adantlr 751 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5655anassrs 681 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
5748, 56pm2.61dan 849 . . . . . . 7 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ { 0 })
5857, 46sylib 208 . . . . . 6 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) = 0 )
5958mpteq2dva 4777 . . . . 5 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴0 ))
609, 59eqtrd 2685 . . . 4 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
6160oveq2d 6706 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
62 gsumval3.b . . . . . . . 8 𝐵 = (Base‘𝐺)
6362, 3mndidcl 17355 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
641, 63syl 17 . . . . . 6 (𝜑0𝐵)
65 gsumval3.p . . . . . . 7 + = (+g𝐺)
6662, 65, 3mndlid 17358 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
671, 64, 66syl2anc 694 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
6867adantr 480 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
69 gsumval3.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
70 nnuz 11761 . . . . . 6 ℕ = (ℤ‘1)
7169, 70syl6eleq 2740 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
7271adantr 480 . . . 4 ((𝜑𝑊 = ∅) → 𝑀 ∈ (ℤ‘1))
7326eleq2d 2716 . . . . . 6 ((𝜑𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
7473biimpar 501 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
7531, 34, 35, 38suppssr 7371 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
7674, 75syldan 486 . . . 4 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) = 0 )
7768, 72, 76seqid3 12885 . . 3 ((𝜑𝑊 = ∅) → (seq1( + , (𝐹𝐻))‘𝑀) = 0 )
786, 61, 773eqtr4d 2695 . 2 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
79 fzf 12368 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
80 ffn 6083 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
81 ovelrn 6852 . . . . 5 (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
8279, 80, 81mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
831ad2antrr 762 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
84 simpr 476 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
85 frel 6088 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → Rel 𝐹)
86 reldm0 5375 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
877, 85, 863syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
88 fdm 6089 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
897, 88syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
9089eqeq1d 2653 . . . . . . . . . . . . . . . 16 (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
9187, 90bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
92 coeq1 5312 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ∅ → (𝐹𝐻) = (∅ ∘ 𝐻))
93 co01 5688 . . . . . . . . . . . . . . . . . . 19 (∅ ∘ 𝐻) = ∅
9492, 93syl6eq 2701 . . . . . . . . . . . . . . . . . 18 (𝐹 = ∅ → (𝐹𝐻) = ∅)
9594oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = (∅ supp 0 ))
96 supp0 7345 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V → (∅ supp 0 ) = ∅)
9737, 96ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ supp 0 ) = ∅
9895, 97syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = ∅)
9932, 98syl5eq 2697 . . . . . . . . . . . . . . 15 (𝐹 = ∅ → 𝑊 = ∅)
10091, 99syl6bir 244 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
101100necon3d 2844 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
102101imp 444 . . . . . . . . . . . 12 ((𝜑𝑊 ≠ ∅) → 𝐴 ≠ ∅)
103102adantr 480 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
10484, 103eqnetrrd 2891 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
105 fzn0 12393 . . . . . . . . . 10 ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ𝑚))
106104, 105sylib 208 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ𝑚))
1077ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴𝐵)
10884feq2d 6069 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴𝐵𝐹:(𝑚...𝑛)⟶𝐵))
109107, 108mpbid 222 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
11062, 65, 83, 106, 109gsumval2 17327 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
111 frn 6091 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻𝐴)
11210, 11, 1113syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻𝐴)
113112ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻𝐴)
114113, 84sseqtrd 3674 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
115 fzssuz 12420 . . . . . . . . . . . . 13 (𝑚...𝑛) ⊆ (ℤ𝑚)
116 uzssz 11745 . . . . . . . . . . . . . 14 (ℤ𝑚) ⊆ ℤ
117 zssre 11422 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
118116, 117sstri 3645 . . . . . . . . . . . . 13 (ℤ𝑚) ⊆ ℝ
119115, 118sstri 3645 . . . . . . . . . . . 12 (𝑚...𝑛) ⊆ ℝ
120114, 119syl6ss 3648 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
121 ltso 10156 . . . . . . . . . . 11 < Or ℝ
122 soss 5082 . . . . . . . . . . 11 (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
123120, 121, 122mpisyl 21 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
124 fzfi 12811 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
125124a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑀) ∈ Fin)
126 fex2 7163 . . . . . . . . . . . . . . 15 ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴𝑉) → 𝐻 ∈ V)
12712, 125, 2, 126syl3anc 1366 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ V)
128 f1oen3g 8013 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
129127, 15, 128syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ≈ ran 𝐻)
130 enfi 8217 . . . . . . . . . . . . 13 ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
131129, 130syl 17 . . . . . . . . . . . 12 (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
132124, 131mpbii 223 . . . . . . . . . . 11 (𝜑 → ran 𝐻 ∈ Fin)
133132ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
134 fz1iso 13284 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
135123, 133, 134syl2anc 694 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
13669nnnn0d 11389 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ0)
137 hashfz1 13174 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (#‘(1...𝑀)) = 𝑀)
138136, 137syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(1...𝑀)) = 𝑀)
139 hashen 13175 . . . . . . . . . . . . . . . . 17 (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
140124, 132, 139sylancr 696 . . . . . . . . . . . . . . . 16 (𝜑 → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
141129, 140mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(1...𝑀)) = (#‘ran 𝐻))
142138, 141eqtr3d 2687 . . . . . . . . . . . . . 14 (𝜑𝑀 = (#‘ran 𝐻))
143142ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 = (#‘ran 𝐻))
144143fveq2d 6233 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝑓))‘𝑀) = (seq1( + , (𝐹𝑓))‘(#‘ran 𝐻)))
1451ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
14662, 65mndcl 17348 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
1471463expb 1285 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
148145, 147sylan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
149 gsumval3.c . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
150149ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
151150sselda 3636 . . . . . . . . . . . . . . 15 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
152 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntz‘𝐺)
15365, 152cntzi 17808 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
154151, 153sylan 487 . . . . . . . . . . . . . 14 (((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
155154anasss 680 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
15662, 65mndass 17349 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
157145, 156sylan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15871ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ‘1))
1597ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴𝐵)
160 frn 6091 . . . . . . . . . . . . . 14 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
161159, 160syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹𝐵)
162 simprr 811 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
163 isof1o 6613 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
164162, 163syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
165143oveq2d 6706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(#‘ran 𝐻)))
166 f1oeq2 6166 . . . . . . . . . . . . . . . . 17 ((1...𝑀) = (1...(#‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
167165, 166syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
168164, 167mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
169 f1ocnv 6187 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:ran 𝐻1-1-onto→(1...𝑀))
170168, 169syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻1-1-onto→(1...𝑀))
17115ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
172 f1oco 6197 . . . . . . . . . . . . . 14 ((𝑓:ran 𝐻1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
173170, 171, 172syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
174 ffn 6083 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
175 dffn4 6159 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
176174, 175sylib 208 . . . . . . . . . . . . . . . 16 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
177 fof 6153 . . . . . . . . . . . . . . . 16 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
178159, 176, 1773syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
179 f1of 6175 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...𝑀)⟶ran 𝐻)
180168, 179syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
181112ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻𝐴)
182180, 181fssd 6095 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
183 fco 6096 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ran 𝐹𝑓:(1...𝑀)⟶𝐴) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
184178, 182, 183syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
185184ffvelrnda 6399 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝑓)‘𝑥) ∈ ran 𝐹)
186 f1ococnv2 6201 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓𝑓) = ( I ↾ ran 𝐻))
187168, 186syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝑓) = ( I ↾ ran 𝐻))
188187coeq1d 5316 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝑓𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
189 f1of 6175 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:(1...𝑀)⟶ran 𝐻)
190 fcoi2 6117 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
191171, 189, 1903syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
192188, 191eqtr2d 2686 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓𝑓) ∘ 𝐻))
193 coass 5692 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑓) ∘ 𝐻) = (𝑓 ∘ (𝑓𝐻))
194192, 193syl6eq 2701 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (𝑓𝐻)))
195194coeq2d 5317 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻))))
196 coass 5692 . . . . . . . . . . . . . . . . 17 ((𝐹𝑓) ∘ (𝑓𝐻)) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻)))
197195, 196syl6eqr 2703 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = ((𝐹𝑓) ∘ (𝑓𝐻)))
198197fveq1d 6231 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
199198adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
200 f1of 6175 . . . . . . . . . . . . . . . . 17 (𝑓:ran 𝐻1-1-onto→(1...𝑀) → 𝑓:ran 𝐻⟶(1...𝑀))
201168, 169, 2003syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻⟶(1...𝑀))
202171, 189syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
203 fco 6096 . . . . . . . . . . . . . . . 16 ((𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
204201, 202, 203syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
205 fvco3 6314 . . . . . . . . . . . . . . 15 (((𝑓𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
206204, 205sylan 487 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
207199, 206eqtrd 2685 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
208148, 155, 157, 158, 161, 173, 185, 207seqf1o 12882 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹𝑓))‘𝑀))
20962, 65, 3mndlid 17358 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
210145, 209sylan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
21162, 65, 3mndrid 17359 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
212145, 211sylan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
213145, 63syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 0𝐵)
214 fdm 6089 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
21510, 11, 2143syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = (1...𝑀))
216 eluzfz1 12386 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
217 ne0i 3954 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
21871, 216, 2173syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ≠ ∅)
219215, 218eqnetrd 2890 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐻 ≠ ∅)
220 dm0rn0 5374 . . . . . . . . . . . . . . . 16 (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
221220necon3bii 2875 . . . . . . . . . . . . . . 15 (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
222219, 221sylib 208 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻 ≠ ∅)
223222ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
224114adantrr 753 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
225 simprl 809 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
226225eleq2d 2716 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥𝐴𝑥 ∈ (𝑚...𝑛)))
227226biimpar 501 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥𝐴)
228159ffvelrnda 6399 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
229227, 228syldan 486 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹𝑥) ∈ 𝐵)
230225difeq1d 3760 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
231230eleq2d 2716 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
232231biimpar 501 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
233 simpll 805 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝜑)
234233, 52sylan 487 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
235232, 234syldan 486 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
236 f1of 6175 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
237162, 163, 2363syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
238 fvco3 6314 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
239237, 238sylan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
240210, 212, 148, 213, 162, 223, 224, 229, 235, 239seqcoll2 13287 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹𝑓))‘(#‘ran 𝐻)))
241144, 208, 2403eqtr4d 2695 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
242241expr 642 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
243242exlimdv 1901 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
244135, 243mpd 15 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
245110, 244eqtr4d 2688 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
246245ex 449 . . . . . 6 ((𝜑𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
247246rexlimdvw 3063 . . . . 5 ((𝜑𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
248247rexlimdvw 3063 . . . 4 ((𝜑𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
24982, 248syl5bi 232 . . 3 ((𝜑𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
250 suppssdm 7353 . . . . . . . . . . 11 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
25132, 250eqsstri 3668 . . . . . . . . . 10 𝑊 ⊆ dom (𝐹𝐻)
252 fdm 6089 . . . . . . . . . . 11 ((𝐹𝐻):(1...𝑀)⟶𝐵 → dom (𝐹𝐻) = (1...𝑀))
25330, 252syl 17 . . . . . . . . . 10 (𝜑 → dom (𝐹𝐻) = (1...𝑀))
254251, 253syl5sseq 3686 . . . . . . . . 9 (𝜑𝑊 ⊆ (1...𝑀))
255 fzssuz 12420 . . . . . . . . . . 11 (1...𝑀) ⊆ (ℤ‘1)
256255, 70sseqtr4i 3671 . . . . . . . . . 10 (1...𝑀) ⊆ ℕ
257 nnssre 11062 . . . . . . . . . 10 ℕ ⊆ ℝ
258256, 257sstri 3645 . . . . . . . . 9 (1...𝑀) ⊆ ℝ
259254, 258syl6ss 3648 . . . . . . . 8 (𝜑𝑊 ⊆ ℝ)
260 soss 5082 . . . . . . . 8 (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
261259, 121, 260mpisyl 21 . . . . . . 7 (𝜑 → < Or 𝑊)
262 ssfi 8221 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
263124, 254, 262sylancr 696 . . . . . . 7 (𝜑𝑊 ∈ Fin)
264 fz1iso 13284 . . . . . . 7 (( < Or 𝑊𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
265261, 263, 264syl2anc 694 . . . . . 6 (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
266265ad2antrr 762 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
26762, 3, 65, 152, 1, 2, 7, 149, 69, 10, 50, 32gsumval3lem2 18353 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(#‘𝑊)))
2681ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
269268, 209sylan 487 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
270268, 211sylan 487 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
271268, 147sylan 487 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
272268, 63syl 17 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0𝐵)
273 simprr 811 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
274 simplr 807 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
275254ad2antrr 762 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
27630ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐹𝐻):(1...𝑀)⟶𝐵)
277276ffvelrnda 6399 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) ∈ 𝐵)
27833a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
279 ovexd 6720 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
28037a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0 ∈ V)
281276, 278, 279, 280suppssr 7371 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
282 coass 5692 . . . . . . . . . . 11 ((𝐹𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻𝑓))
283282fveq1i 6230 . . . . . . . . . 10 (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻𝑓))‘𝑦)
284 isof1o 6613 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
285 f1of 6175 . . . . . . . . . . . 12 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))⟶𝑊)
286273, 284, 2853syl 18 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝑊)
287 fvco3 6314 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))⟶𝑊𝑦 ∈ (1...(#‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
288286, 287sylan 487 . . . . . . . . . 10 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
289283, 288syl5eqr 2699 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ (𝐻𝑓))‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
290269, 270, 271, 272, 273, 274, 275, 277, 281, 289seqcoll2 13287 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(#‘𝑊)))
291267, 290eqtr4d 2688 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
292291expr 642 . . . . . 6 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
293292exlimdv 1901 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
294266, 293mpd 15 . . . 4 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
295294ex 449 . . 3 ((𝜑𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
296249, 295pm2.61d 170 . 2 ((𝜑𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
29778, 296pm2.61dane 2910 1 (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wne 2823  wrex 2942  Vcvv 3231  cdif 3604  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   class class class wbr 4685  cmpt 4762   I cid 5052   Or wor 5063   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  ccom 5147  Rel wrel 5148   Fn wfn 5921  wf 5922  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  (class class class)co 6690   supp csupp 7340  cen 7994  Fincfn 7997  cr 9973  1c1 9975   < clt 10112  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  seqcseq 12841  #chash 13157  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341  Cntzccntz 17794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-0g 16149  df-gsum 16150  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-cntz 17796
This theorem is referenced by:  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  gsumfsum  19861  wilthlem3  24841
  Copyright terms: Public domain W3C validator