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

Theorem gsumval3 18508
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 573 . . . 4 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
65adantr 466 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
7 gsumval3.f . . . . . . 7 (𝜑𝐹:𝐴𝐵)
87feqmptd 6389 . . . . . 6 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
98adantr 466 . . . . 5 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
10 gsumval3.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...𝑀)–1-1𝐴)
11 f1f 6239 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)⟶𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (𝜑𝐻:(1...𝑀)⟶𝐴)
1312ad2antrr 705 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14 f1f1orn 6287 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1615adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17 f1ocnv 6288 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:ran 𝐻1-1-onto→(1...𝑀))
18 f1of 6276 . . . . . . . . . . . . . 14 (𝐻:ran 𝐻1-1-onto→(1...𝑀) → 𝐻:ran 𝐻⟶(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 𝐻:ran 𝐻⟶(1...𝑀))
2019ffvelrnda 6500 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ (1...𝑀))
21 fvco3 6415 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟶𝐴 ∧ (𝐻𝑥) ∈ (1...𝑀)) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
2213, 20, 21syl2anc 573 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
23 simpr 471 . . . . . . . . . . . . . . . 16 ((𝜑𝑊 = ∅) → 𝑊 = ∅)
2423difeq2d 3879 . . . . . . . . . . . . . . 15 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25 dif0 4097 . . . . . . . . . . . . . . 15 ((1...𝑀) ∖ ∅) = (1...𝑀)
2624, 25syl6eq 2821 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2726adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2820, 27eleqtrrd 2853 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29 fco 6196 . . . . . . . . . . . . . . 15 ((𝐹:𝐴𝐵𝐻:(1...𝑀)⟶𝐴) → (𝐹𝐻):(1...𝑀)⟶𝐵)
307, 12, 29syl2anc 573 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻):(1...𝑀)⟶𝐵)
3130adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (𝐹𝐻):(1...𝑀)⟶𝐵)
32 gsumval3.w . . . . . . . . . . . . . . 15 𝑊 = ((𝐹𝐻) supp 0 )
3332eqimss2i 3809 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ 𝑊
3433a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
35 ovexd 6823 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (1...𝑀) ∈ V)
363fvexi 6341 . . . . . . . . . . . . . 14 0 ∈ V
3736a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 0 ∈ V)
3831, 34, 35, 37suppssr 7476 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
3928, 38syldan 579 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
40 f1ocnvfv2 6674 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4116, 40sylan 569 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4241fveq2d 6334 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(𝐻𝑥))) = (𝐹𝑥))
4322, 39, 423eqtr3rd 2814 . . . . . . . . . 10 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) = 0 )
44 fvex 6340 . . . . . . . . . . 11 (𝐹𝑥) ∈ V
4544elsn 4331 . . . . . . . . . 10 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
4643, 45sylibr 224 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
4746adantlr 694 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
48 eldif 3733 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49 gsumval3.n . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
5036a1i 11 . . . . . . . . . . . . 13 (𝜑0 ∈ V)
517, 49, 2, 50suppssr 7476 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
5251, 45sylibr 224 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5348, 52sylan2br 582 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5453adantlr 694 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5554anassrs 453 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
5647, 55pm2.61dan 814 . . . . . . 7 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ { 0 })
5756, 45sylib 208 . . . . . 6 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) = 0 )
5857mpteq2dva 4878 . . . . 5 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴0 ))
599, 58eqtrd 2805 . . . 4 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
6059oveq2d 6807 . . 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 573 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
6766adantr 466 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
68 gsumval3.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
69 nnuz 11923 . . . . . 6 ℕ = (ℤ‘1)
7068, 69syl6eleq 2860 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
7170adantr 466 . . . 4 ((𝜑𝑊 = ∅) → 𝑀 ∈ (ℤ‘1))
7226eleq2d 2836 . . . . . 6 ((𝜑𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
7372biimpar 463 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
7431, 34, 35, 37suppssr 7476 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
7573, 74syldan 579 . . . 4 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) = 0 )
7667, 71, 75seqid3 13045 . . 3 ((𝜑𝑊 = ∅) → (seq1( + , (𝐹𝐻))‘𝑀) = 0 )
776, 60, 763eqtr4d 2815 . 2 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
78 fzf 12530 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
79 ffn 6183 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
80 ovelrn 6955 . . . . 5 (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
8178, 79, 80mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
821ad2antrr 705 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
83 simpr 471 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
84 frel 6188 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → Rel 𝐹)
85 reldm0 5479 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
867, 84, 853syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
87 fdm 6189 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
887, 87syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
8988eqeq1d 2773 . . . . . . . . . . . . . . . 16 (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
9086, 89bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
91 coeq1 5416 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ∅ → (𝐹𝐻) = (∅ ∘ 𝐻))
92 co01 5792 . . . . . . . . . . . . . . . . . . 19 (∅ ∘ 𝐻) = ∅
9391, 92syl6eq 2821 . . . . . . . . . . . . . . . . . 18 (𝐹 = ∅ → (𝐹𝐻) = ∅)
9493oveq1d 6806 . . . . . . . . . . . . . . . . 17 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = (∅ supp 0 ))
95 supp0 7449 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V → (∅ supp 0 ) = ∅)
9636, 95ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ supp 0 ) = ∅
9794, 96syl6eq 2821 . . . . . . . . . . . . . . . 16 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = ∅)
9832, 97syl5eq 2817 . . . . . . . . . . . . . . 15 (𝐹 = ∅ → 𝑊 = ∅)
9990, 98syl6bir 244 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
10099necon3d 2964 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
101100imp 393 . . . . . . . . . . . 12 ((𝜑𝑊 ≠ ∅) → 𝐴 ≠ ∅)
102101adantr 466 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
10383, 102eqnetrrd 3011 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
104 fzn0 12555 . . . . . . . . . 10 ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ𝑚))
105103, 104sylib 208 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ𝑚))
1067ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴𝐵)
10783feq2d 6169 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴𝐵𝐹:(𝑚...𝑛)⟶𝐵))
108106, 107mpbid 222 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
10961, 64, 82, 105, 108gsumval2 17481 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
110 frn 6191 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻𝐴)
11110, 11, 1103syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻𝐴)
112111ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻𝐴)
113112, 83sseqtrd 3790 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
114 fzssuz 12582 . . . . . . . . . . . . 13 (𝑚...𝑛) ⊆ (ℤ𝑚)
115 uzssz 11906 . . . . . . . . . . . . . 14 (ℤ𝑚) ⊆ ℤ
116 zssre 11584 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
117115, 116sstri 3761 . . . . . . . . . . . . 13 (ℤ𝑚) ⊆ ℝ
118114, 117sstri 3761 . . . . . . . . . . . 12 (𝑚...𝑛) ⊆ ℝ
119113, 118syl6ss 3764 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
120 ltso 10318 . . . . . . . . . . 11 < Or ℝ
121 soss 5188 . . . . . . . . . . 11 (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
122119, 120, 121mpisyl 21 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
123 fzfi 12972 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
124123a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑀) ∈ Fin)
125 fex2 7266 . . . . . . . . . . . . . . 15 ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴𝑉) → 𝐻 ∈ V)
12612, 124, 2, 125syl3anc 1476 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ V)
127 f1oen3g 8123 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
128126, 15, 127syl2anc 573 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ≈ ran 𝐻)
129 enfi 8330 . . . . . . . . . . . . 13 ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
130128, 129syl 17 . . . . . . . . . . . 12 (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
131123, 130mpbii 223 . . . . . . . . . . 11 (𝜑 → ran 𝐻 ∈ Fin)
132131ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
133 fz1iso 13441 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
134122, 132, 133syl2anc 573 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
13568nnnn0d 11551 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ0)
136 hashfz1 13331 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
137135, 136syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
138 hashen 13332 . . . . . . . . . . . . . . . . 17 (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
139123, 131, 138sylancr 575 . . . . . . . . . . . . . . . 16 (𝜑 → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
140128, 139mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
141137, 140eqtr3d 2807 . . . . . . . . . . . . . 14 (𝜑𝑀 = (♯‘ran 𝐻))
142141ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
143142fveq2d 6334 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝑓))‘𝑀) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
1441ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
14561, 64mndcl 17502 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
1461453expb 1113 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
147144, 146sylan 569 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
148 gsumval3.c . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
149148ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
150149sselda 3752 . . . . . . . . . . . . . . 15 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
151 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntz‘𝐺)
15264, 151cntzi 17962 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
153150, 152sylan 569 . . . . . . . . . . . . . 14 (((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
154153anasss 452 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
15561, 64mndass 17503 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
156144, 155sylan 569 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15770ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ‘1))
1587ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴𝐵)
159 frn 6191 . . . . . . . . . . . . . 14 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
160158, 159syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹𝐵)
161 simprr 756 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
162 isof1o 6714 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
163161, 162syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
164142oveq2d 6807 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
165 f1oeq2 6267 . . . . . . . . . . . . . . . . 17 ((1...𝑀) = (1...(♯‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
166164, 165syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
167163, 166mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
168 f1ocnv 6288 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:ran 𝐻1-1-onto→(1...𝑀))
169167, 168syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻1-1-onto→(1...𝑀))
17015ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
171 f1oco 6298 . . . . . . . . . . . . . 14 ((𝑓:ran 𝐻1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
172169, 170, 171syl2anc 573 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
173 ffn 6183 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
174 dffn4 6260 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
175173, 174sylib 208 . . . . . . . . . . . . . . . 16 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
176 fof 6254 . . . . . . . . . . . . . . . 16 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
177158, 175, 1763syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
178 f1of 6276 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...𝑀)⟶ran 𝐻)
179167, 178syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
180111ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻𝐴)
181179, 180fssd 6195 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
182 fco 6196 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ran 𝐹𝑓:(1...𝑀)⟶𝐴) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
183177, 181, 182syl2anc 573 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
184183ffvelrnda 6500 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝑓)‘𝑥) ∈ ran 𝐹)
185 f1ococnv2 6302 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓𝑓) = ( I ↾ ran 𝐻))
186167, 185syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝑓) = ( I ↾ ran 𝐻))
187186coeq1d 5420 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
188 f1of 6276 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:(1...𝑀)⟶ran 𝐻)
189 fcoi2 6217 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
190170, 188, 1893syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
191187, 190eqtr2d 2806 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓𝑓) ∘ 𝐻))
192 coass 5796 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑓) ∘ 𝐻) = (𝑓 ∘ (𝑓𝐻))
193191, 192syl6eq 2821 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (𝑓𝐻)))
194193coeq2d 5421 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻))))
195 coass 5796 . . . . . . . . . . . . . . . . 17 ((𝐹𝑓) ∘ (𝑓𝐻)) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻)))
196194, 195syl6eqr 2823 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = ((𝐹𝑓) ∘ (𝑓𝐻)))
197196fveq1d 6332 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
198197adantr 466 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
199 f1of 6276 . . . . . . . . . . . . . . . . 17 (𝑓:ran 𝐻1-1-onto→(1...𝑀) → 𝑓:ran 𝐻⟶(1...𝑀))
200167, 168, 1993syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻⟶(1...𝑀))
201170, 188syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
202 fco 6196 . . . . . . . . . . . . . . . 16 ((𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
203200, 201, 202syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
204 fvco3 6415 . . . . . . . . . . . . . . 15 (((𝑓𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
205203, 204sylan 569 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
206198, 205eqtrd 2805 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
207147, 154, 156, 157, 160, 172, 184, 206seqf1o 13042 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹𝑓))‘𝑀))
20861, 64, 3mndlid 17512 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
209144, 208sylan 569 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
21061, 64, 3mndrid 17513 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
211144, 210sylan 569 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
212144, 62syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 0𝐵)
213 fdm 6189 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
21410, 11, 2133syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = (1...𝑀))
215 eluzfz1 12548 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
216 ne0i 4069 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
21770, 215, 2163syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ≠ ∅)
218214, 217eqnetrd 3010 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐻 ≠ ∅)
219 dm0rn0 5478 . . . . . . . . . . . . . . . 16 (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
220219necon3bii 2995 . . . . . . . . . . . . . . 15 (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
221218, 220sylib 208 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻 ≠ ∅)
222221ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
223113adantrr 696 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
224 simprl 754 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
225224eleq2d 2836 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥𝐴𝑥 ∈ (𝑚...𝑛)))
226225biimpar 463 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥𝐴)
227158ffvelrnda 6500 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
228226, 227syldan 579 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹𝑥) ∈ 𝐵)
229224difeq1d 3878 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
230229eleq2d 2836 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
231230biimpar 463 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
232 simpll 750 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝜑)
233232, 51sylan 569 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
234231, 233syldan 579 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
235 f1of 6276 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
236161, 162, 2353syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
237 fvco3 6415 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
238236, 237sylan 569 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
239209, 211, 147, 212, 161, 222, 223, 228, 234, 238seqcoll2 13444 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
240143, 207, 2393eqtr4d 2815 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
241240expr 444 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
242241exlimdv 2013 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
243134, 242mpd 15 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
244109, 243eqtr4d 2808 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
245244ex 397 . . . . . 6 ((𝜑𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
246245rexlimdvw 3182 . . . . 5 ((𝜑𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
247246rexlimdvw 3182 . . . 4 ((𝜑𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
24881, 247syl5bi 232 . . 3 ((𝜑𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
249 suppssdm 7457 . . . . . . . . . . 11 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
25032, 249eqsstri 3784 . . . . . . . . . 10 𝑊 ⊆ dom (𝐹𝐻)
251 fdm 6189 . . . . . . . . . . 11 ((𝐹𝐻):(1...𝑀)⟶𝐵 → dom (𝐹𝐻) = (1...𝑀))
25230, 251syl 17 . . . . . . . . . 10 (𝜑 → dom (𝐹𝐻) = (1...𝑀))
253250, 252syl5sseq 3802 . . . . . . . . 9 (𝜑𝑊 ⊆ (1...𝑀))
254 fzssuz 12582 . . . . . . . . . . 11 (1...𝑀) ⊆ (ℤ‘1)
255254, 69sseqtr4i 3787 . . . . . . . . . 10 (1...𝑀) ⊆ ℕ
256 nnssre 11224 . . . . . . . . . 10 ℕ ⊆ ℝ
257255, 256sstri 3761 . . . . . . . . 9 (1...𝑀) ⊆ ℝ
258253, 257syl6ss 3764 . . . . . . . 8 (𝜑𝑊 ⊆ ℝ)
259 soss 5188 . . . . . . . 8 (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
260258, 120, 259mpisyl 21 . . . . . . 7 (𝜑 → < Or 𝑊)
261 ssfi 8334 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
262123, 253, 261sylancr 575 . . . . . . 7 (𝜑𝑊 ∈ Fin)
263 fz1iso 13441 . . . . . . 7 (( < Or 𝑊𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
264260, 262, 263syl2anc 573 . . . . . 6 (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
265264ad2antrr 705 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
26661, 3, 64, 151, 1, 2, 7, 148, 68, 10, 49, 32gsumval3lem2 18507 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
2671ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
268267, 208sylan 569 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
269267, 210sylan 569 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
270267, 146sylan 569 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
271267, 62syl 17 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0𝐵)
272 simprr 756 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
273 simplr 752 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
274253ad2antrr 705 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
27530ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹𝐻):(1...𝑀)⟶𝐵)
276275ffvelrnda 6500 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) ∈ 𝐵)
27733a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
278 ovexd 6823 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
27936a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
280275, 277, 278, 279suppssr 7476 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
281 coass 5796 . . . . . . . . . . 11 ((𝐹𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻𝑓))
282281fveq1i 6331 . . . . . . . . . 10 (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻𝑓))‘𝑦)
283 isof1o 6714 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)
284 f1of 6276 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))⟶𝑊)
285272, 283, 2843syl 18 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
286 fvco3 6415 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))⟶𝑊𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
287285, 286sylan 569 . . . . . . . . . 10 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
288282, 287syl5eqr 2819 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻𝑓))‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
289268, 269, 270, 271, 272, 273, 274, 276, 280, 288seqcoll2 13444 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
290266, 289eqtr4d 2808 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
291290expr 444 . . . . . 6 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
292291exlimdv 2013 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
293265, 292mpd 15 . . . 4 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
294293ex 397 . . 3 ((𝜑𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
295248, 294pm2.61d 171 . 2 ((𝜑𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
29677, 295pm2.61dane 3030 1 (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wrex 3062  Vcvv 3351  cdif 3720  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   class class class wbr 4786  cmpt 4863   I cid 5156   Or wor 5169   × cxp 5247  ccnv 5248  dom cdm 5249  ran crn 5250  cres 5251  ccom 5253  Rel wrel 5254   Fn wfn 6024  wf 6025  1-1wf1 6026  ontowfo 6027  1-1-ontowf1o 6028  cfv 6029   Isom wiso 6030  (class class class)co 6791   supp csupp 7444  cen 8104  Fincfn 8107  cr 10135  1c1 10137   < clt 10274  cn 11220  0cn0 11492  cz 11577  cuz 11886  ...cfz 12526  seqcseq 13001  chash 13314  Basecbs 16057  +gcplusg 16142  0gc0g 16301   Σg cgsu 16302  Mndcmnd 17495  Cntzccntz 17948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-isom 6038  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-supp 7445  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-oadd 7715  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-oi 8569  df-card 8963  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-nn 11221  df-n0 11493  df-z 11578  df-uz 11887  df-fz 12527  df-fzo 12667  df-seq 13002  df-hash 13315  df-0g 16303  df-gsum 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-cntz 17950
This theorem is referenced by:  gsumzres  18510  gsumzcl2  18511  gsumzf1o  18513  gsumzaddlem  18521  gsumconst  18534  gsumzmhm  18537  gsumzoppg  18544  gsumfsum  20021  wilthlem3  25010
  Copyright terms: Public domain W3C validator