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

Theorem gsumval3 18505
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 17575 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
51, 2, 4syl2anc 575 . . . 4 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
65adantr 468 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
7 gsumval3.f . . . . . . 7 (𝜑𝐹:𝐴𝐵)
87feqmptd 6466 . . . . . 6 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
98adantr 468 . . . . 5 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
10 gsumval3.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...𝑀)–1-1𝐴)
11 f1f 6312 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)⟶𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (𝜑𝐻:(1...𝑀)⟶𝐴)
1312ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14 f1f1orn 6360 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1615adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17 f1ocnv 6361 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:ran 𝐻1-1-onto→(1...𝑀))
18 f1of 6349 . . . . . . . . . . . . . 14 (𝐻:ran 𝐻1-1-onto→(1...𝑀) → 𝐻:ran 𝐻⟶(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 𝐻:ran 𝐻⟶(1...𝑀))
2019ffvelrnda 6577 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ (1...𝑀))
21 fvco3 6492 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟶𝐴 ∧ (𝐻𝑥) ∈ (1...𝑀)) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
2213, 20, 21syl2anc 575 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
23 simpr 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑊 = ∅) → 𝑊 = ∅)
2423difeq2d 3927 . . . . . . . . . . . . . . 15 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25 dif0 4151 . . . . . . . . . . . . . . 15 ((1...𝑀) ∖ ∅) = (1...𝑀)
2624, 25syl6eq 2856 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2726adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2820, 27eleqtrrd 2888 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29 fco 6269 . . . . . . . . . . . . . . 15 ((𝐹:𝐴𝐵𝐻:(1...𝑀)⟶𝐴) → (𝐹𝐻):(1...𝑀)⟶𝐵)
307, 12, 29syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻):(1...𝑀)⟶𝐵)
3130adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (𝐹𝐻):(1...𝑀)⟶𝐵)
32 gsumval3.w . . . . . . . . . . . . . . 15 𝑊 = ((𝐹𝐻) supp 0 )
3332eqimss2i 3857 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ 𝑊
3433a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
35 ovexd 6904 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (1...𝑀) ∈ V)
363fvexi 6418 . . . . . . . . . . . . . 14 0 ∈ V
3736a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 0 ∈ V)
3831, 34, 35, 37suppssr 7557 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
3928, 38syldan 581 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
40 f1ocnvfv2 6753 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4116, 40sylan 571 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4241fveq2d 6408 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(𝐻𝑥))) = (𝐹𝑥))
4322, 39, 423eqtr3rd 2849 . . . . . . . . . 10 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) = 0 )
44 fvex 6417 . . . . . . . . . . 11 (𝐹𝑥) ∈ V
4544elsn 4385 . . . . . . . . . 10 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
4643, 45sylibr 225 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
4746adantlr 697 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
48 eldif 3779 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49 gsumval3.n . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
5036a1i 11 . . . . . . . . . . . . 13 (𝜑0 ∈ V)
517, 49, 2, 50suppssr 7557 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
5251, 45sylibr 225 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5348, 52sylan2br 584 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5453adantlr 697 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5554anassrs 455 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
5647, 55pm2.61dan 838 . . . . . . 7 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ { 0 })
5756, 45sylib 209 . . . . . 6 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) = 0 )
5857mpteq2dva 4938 . . . . 5 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴0 ))
599, 58eqtrd 2840 . . . 4 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
6059oveq2d 6886 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
61 gsumval3.b . . . . . . . 8 𝐵 = (Base‘𝐺)
6261, 3mndidcl 17509 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
631, 62syl 17 . . . . . 6 (𝜑0𝐵)
64 gsumval3.p . . . . . . 7 + = (+g𝐺)
6561, 64, 3mndlid 17512 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
661, 63, 65syl2anc 575 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
6766adantr 468 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
68 gsumval3.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
69 nnuz 11937 . . . . . 6 ℕ = (ℤ‘1)
7068, 69syl6eleq 2895 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
7170adantr 468 . . . 4 ((𝜑𝑊 = ∅) → 𝑀 ∈ (ℤ‘1))
7226eleq2d 2871 . . . . . 6 ((𝜑𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
7372biimpar 465 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
7431, 34, 35, 37suppssr 7557 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
7573, 74syldan 581 . . . 4 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) = 0 )
7667, 71, 75seqid3 13064 . . 3 ((𝜑𝑊 = ∅) → (seq1( + , (𝐹𝐻))‘𝑀) = 0 )
776, 60, 763eqtr4d 2850 . 2 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
78 fzf 12549 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
79 ffn 6252 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
80 ovelrn 7036 . . . . 5 (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
8178, 79, 80mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
821ad2antrr 708 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
83 simpr 473 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
84 frel 6257 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → Rel 𝐹)
85 reldm0 5544 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
867, 84, 853syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
877fdmd 6261 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
8887eqeq1d 2808 . . . . . . . . . . . . . . . 16 (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
8986, 88bitrd 270 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
90 coeq1 5481 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ∅ → (𝐹𝐻) = (∅ ∘ 𝐻))
91 co01 5864 . . . . . . . . . . . . . . . . . . 19 (∅ ∘ 𝐻) = ∅
9290, 91syl6eq 2856 . . . . . . . . . . . . . . . . . 18 (𝐹 = ∅ → (𝐹𝐻) = ∅)
9392oveq1d 6885 . . . . . . . . . . . . . . . . 17 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = (∅ supp 0 ))
94 supp0 7530 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V → (∅ supp 0 ) = ∅)
9536, 94ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ supp 0 ) = ∅
9693, 95syl6eq 2856 . . . . . . . . . . . . . . . 16 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = ∅)
9732, 96syl5eq 2852 . . . . . . . . . . . . . . 15 (𝐹 = ∅ → 𝑊 = ∅)
9889, 97syl6bir 245 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
9998necon3d 2999 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
10099imp 395 . . . . . . . . . . . 12 ((𝜑𝑊 ≠ ∅) → 𝐴 ≠ ∅)
101100adantr 468 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
10283, 101eqnetrrd 3046 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
103 fzn0 12574 . . . . . . . . . 10 ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ𝑚))
104102, 103sylib 209 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ𝑚))
1057ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴𝐵)
10683feq2d 6238 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴𝐵𝐹:(𝑚...𝑛)⟶𝐵))
107105, 106mpbid 223 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
10861, 64, 82, 104, 107gsumval2 17481 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
109 frn 6258 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻𝐴)
11010, 11, 1093syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻𝐴)
111110ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻𝐴)
112111, 83sseqtrd 3838 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
113 fzssuz 12601 . . . . . . . . . . . . 13 (𝑚...𝑛) ⊆ (ℤ𝑚)
114 uzssz 11920 . . . . . . . . . . . . . 14 (ℤ𝑚) ⊆ ℤ
115 zssre 11646 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
116114, 115sstri 3807 . . . . . . . . . . . . 13 (ℤ𝑚) ⊆ ℝ
117113, 116sstri 3807 . . . . . . . . . . . 12 (𝑚...𝑛) ⊆ ℝ
118112, 117syl6ss 3810 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
119 ltso 10399 . . . . . . . . . . 11 < Or ℝ
120 soss 5250 . . . . . . . . . . 11 (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
121118, 119, 120mpisyl 21 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
122 fzfi 12991 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
123122a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑀) ∈ Fin)
124 fex2 7347 . . . . . . . . . . . . . . 15 ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴𝑉) → 𝐻 ∈ V)
12512, 123, 2, 124syl3anc 1483 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ V)
126 f1oen3g 8204 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
127125, 15, 126syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ≈ ran 𝐻)
128 enfi 8411 . . . . . . . . . . . . 13 ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
129127, 128syl 17 . . . . . . . . . . . 12 (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
130122, 129mpbii 224 . . . . . . . . . . 11 (𝜑 → ran 𝐻 ∈ Fin)
131130ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
132 fz1iso 13459 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
133121, 131, 132syl2anc 575 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
13468nnnn0d 11613 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ0)
135 hashfz1 13350 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
136134, 135syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
137 hashen 13351 . . . . . . . . . . . . . . . . 17 (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
138122, 130, 137sylancr 577 . . . . . . . . . . . . . . . 16 (𝜑 → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
139127, 138mpbird 248 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
140136, 139eqtr3d 2842 . . . . . . . . . . . . . 14 (𝜑𝑀 = (♯‘ran 𝐻))
141140ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
142141fveq2d 6408 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝑓))‘𝑀) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
1431ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
14461, 64mndcl 17502 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
1451443expb 1142 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
146143, 145sylan 571 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
147 gsumval3.c . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
148147ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
149148sselda 3798 . . . . . . . . . . . . . . 15 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
150 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntz‘𝐺)
15164, 150cntzi 17959 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
152149, 151sylan 571 . . . . . . . . . . . . . 14 (((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
153152anasss 454 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
15461, 64mndass 17503 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
155143, 154sylan 571 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15670ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ‘1))
1577ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴𝐵)
158157frnd 6259 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹𝐵)
159 simprr 780 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
160 isof1o 6793 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
161159, 160syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
162141oveq2d 6886 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
163 f1oeq2 6340 . . . . . . . . . . . . . . . . 17 ((1...𝑀) = (1...(♯‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
164162, 163syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
165161, 164mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
166 f1ocnv 6361 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:ran 𝐻1-1-onto→(1...𝑀))
167165, 166syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻1-1-onto→(1...𝑀))
16815ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
169 f1oco 6371 . . . . . . . . . . . . . 14 ((𝑓:ran 𝐻1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
170167, 168, 169syl2anc 575 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
171 ffn 6252 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
172 dffn4 6333 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
173171, 172sylib 209 . . . . . . . . . . . . . . . 16 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
174 fof 6327 . . . . . . . . . . . . . . . 16 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
175157, 173, 1743syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
176 f1of 6349 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...𝑀)⟶ran 𝐻)
177165, 176syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
178110ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻𝐴)
179177, 178fssd 6266 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
180 fco 6269 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ran 𝐹𝑓:(1...𝑀)⟶𝐴) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
181175, 179, 180syl2anc 575 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
182181ffvelrnda 6577 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝑓)‘𝑥) ∈ ran 𝐹)
183 f1ococnv2 6375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓𝑓) = ( I ↾ ran 𝐻))
184165, 183syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝑓) = ( I ↾ ran 𝐻))
185184coeq1d 5485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
186 f1of 6349 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:(1...𝑀)⟶ran 𝐻)
187 fcoi2 6290 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
188168, 186, 1873syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
189185, 188eqtr2d 2841 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓𝑓) ∘ 𝐻))
190 coass 5868 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑓) ∘ 𝐻) = (𝑓 ∘ (𝑓𝐻))
191189, 190syl6eq 2856 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (𝑓𝐻)))
192191coeq2d 5486 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻))))
193 coass 5868 . . . . . . . . . . . . . . . . 17 ((𝐹𝑓) ∘ (𝑓𝐻)) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻)))
194192, 193syl6eqr 2858 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = ((𝐹𝑓) ∘ (𝑓𝐻)))
195194fveq1d 6406 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
196195adantr 468 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
197 f1of 6349 . . . . . . . . . . . . . . . . 17 (𝑓:ran 𝐻1-1-onto→(1...𝑀) → 𝑓:ran 𝐻⟶(1...𝑀))
198165, 166, 1973syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻⟶(1...𝑀))
199168, 186syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
200 fco 6269 . . . . . . . . . . . . . . . 16 ((𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
201198, 199, 200syl2anc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
202 fvco3 6492 . . . . . . . . . . . . . . 15 (((𝑓𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
203201, 202sylan 571 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
204196, 203eqtrd 2840 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
205146, 153, 155, 156, 158, 170, 182, 204seqf1o 13061 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹𝑓))‘𝑀))
20661, 64, 3mndlid 17512 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
207143, 206sylan 571 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
20861, 64, 3mndrid 17513 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
209143, 208sylan 571 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
210143, 62syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 0𝐵)
211 fdm 6260 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
21210, 11, 2113syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = (1...𝑀))
213 eluzfz1 12567 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
214 ne0i 4122 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
21570, 213, 2143syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ≠ ∅)
216212, 215eqnetrd 3045 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐻 ≠ ∅)
217 dm0rn0 5543 . . . . . . . . . . . . . . . 16 (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
218217necon3bii 3030 . . . . . . . . . . . . . . 15 (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
219216, 218sylib 209 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻 ≠ ∅)
220219ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
221112adantrr 699 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
222 simprl 778 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
223222eleq2d 2871 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥𝐴𝑥 ∈ (𝑚...𝑛)))
224223biimpar 465 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥𝐴)
225157ffvelrnda 6577 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
226224, 225syldan 581 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹𝑥) ∈ 𝐵)
227222difeq1d 3926 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
228227eleq2d 2871 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
229228biimpar 465 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
230 simpll 774 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝜑)
231230, 51sylan 571 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
232229, 231syldan 581 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
233 f1of 6349 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
234159, 160, 2333syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
235 fvco3 6492 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
236234, 235sylan 571 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
237207, 209, 146, 210, 159, 220, 221, 226, 232, 236seqcoll2 13462 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
238142, 205, 2373eqtr4d 2850 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
239238expr 446 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
240239exlimdv 2024 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
241133, 240mpd 15 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
242108, 241eqtr4d 2843 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
243242ex 399 . . . . . 6 ((𝜑𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
244243rexlimdvw 3222 . . . . 5 ((𝜑𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
245244rexlimdvw 3222 . . . 4 ((𝜑𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
24681, 245syl5bi 233 . . 3 ((𝜑𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
247 suppssdm 7538 . . . . . . . . . . 11 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
24832, 247eqsstri 3832 . . . . . . . . . 10 𝑊 ⊆ dom (𝐹𝐻)
249248, 30fssdm 6268 . . . . . . . . 9 (𝜑𝑊 ⊆ (1...𝑀))
250 fzssuz 12601 . . . . . . . . . . 11 (1...𝑀) ⊆ (ℤ‘1)
251250, 69sseqtr4i 3835 . . . . . . . . . 10 (1...𝑀) ⊆ ℕ
252 nnssre 11305 . . . . . . . . . 10 ℕ ⊆ ℝ
253251, 252sstri 3807 . . . . . . . . 9 (1...𝑀) ⊆ ℝ
254249, 253syl6ss 3810 . . . . . . . 8 (𝜑𝑊 ⊆ ℝ)
255 soss 5250 . . . . . . . 8 (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
256254, 119, 255mpisyl 21 . . . . . . 7 (𝜑 → < Or 𝑊)
257 ssfi 8415 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
258122, 249, 257sylancr 577 . . . . . . 7 (𝜑𝑊 ∈ Fin)
259 fz1iso 13459 . . . . . . 7 (( < Or 𝑊𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
260256, 258, 259syl2anc 575 . . . . . 6 (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
261260ad2antrr 708 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
26261, 3, 64, 150, 1, 2, 7, 147, 68, 10, 49, 32gsumval3lem2 18504 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
2631ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
264263, 206sylan 571 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
265263, 208sylan 571 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
266263, 145sylan 571 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
267263, 62syl 17 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0𝐵)
268 simprr 780 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
269 simplr 776 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
270249ad2antrr 708 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
27130ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹𝐻):(1...𝑀)⟶𝐵)
272271ffvelrnda 6577 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) ∈ 𝐵)
27333a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
274 ovexd 6904 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
27536a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
276271, 273, 274, 275suppssr 7557 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
277 coass 5868 . . . . . . . . . . 11 ((𝐹𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻𝑓))
278277fveq1i 6405 . . . . . . . . . 10 (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻𝑓))‘𝑦)
279 isof1o 6793 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)
280 f1of 6349 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))⟶𝑊)
281268, 279, 2803syl 18 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
282 fvco3 6492 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))⟶𝑊𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
283281, 282sylan 571 . . . . . . . . . 10 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
284278, 283syl5eqr 2854 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻𝑓))‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
285264, 265, 266, 267, 268, 269, 270, 272, 276, 284seqcoll2 13462 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
286262, 285eqtr4d 2843 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
287286expr 446 . . . . . 6 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
288287exlimdv 2024 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
289261, 288mpd 15 . . . 4 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
290289ex 399 . . 3 ((𝜑𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
291246, 290pm2.61d 171 . 2 ((𝜑𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
29277, 291pm2.61dane 3065 1 (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  wne 2978  wrex 3097  Vcvv 3391  cdif 3766  wss 3769  c0 4116  𝒫 cpw 4351  {csn 4370   class class class wbr 4844  cmpt 4923   I cid 5218   Or wor 5231   × cxp 5309  ccnv 5310  dom cdm 5311  ran crn 5312  cres 5313  ccom 5315  Rel wrel 5316   Fn wfn 6092  wf 6093  1-1wf1 6094  ontowfo 6095  1-1-ontowf1o 6096  cfv 6097   Isom wiso 6098  (class class class)co 6870   supp csupp 7525  cen 8185  Fincfn 8188  cr 10216  1c1 10218   < clt 10355  cn 11301  0cn0 11555  cz 11639  cuz 11900  ...cfz 12545  seqcseq 13020  chash 13333  Basecbs 16064  +gcplusg 16149  0gc0g 16301   Σg cgsu 16302  Mndcmnd 17495  Cntzccntz 17945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-oi 8650  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-n0 11556  df-z 11640  df-uz 11901  df-fz 12546  df-fzo 12686  df-seq 13021  df-hash 13334  df-0g 16303  df-gsum 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-cntz 17947
This theorem is referenced by:  gsumzres  18507  gsumzcl2  18508  gsumzf1o  18510  gsumzaddlem  18518  gsumconst  18531  gsumzmhm  18534  gsumzoppg  18541  gsumfsum  20017  wilthlem3  25009
  Copyright terms: Public domain W3C validator