Metamath Proof Explorer


Theorem gsummptnn0fz

Description: A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses gsummptnn0fz.b 𝐵 = ( Base ‘ 𝐺 )
gsummptnn0fz.0 0 = ( 0g𝐺 )
gsummptnn0fz.g ( 𝜑𝐺 ∈ CMnd )
gsummptnn0fz.f ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶𝐵 )
gsummptnn0fz.s ( 𝜑𝑆 ∈ ℕ0 )
gsummptnn0fz.u ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘𝐶 = 0 ) )
Assertion gsummptnn0fz ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptnn0fz.b 𝐵 = ( Base ‘ 𝐺 )
2 gsummptnn0fz.0 0 = ( 0g𝐺 )
3 gsummptnn0fz.g ( 𝜑𝐺 ∈ CMnd )
4 gsummptnn0fz.f ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶𝐵 )
5 gsummptnn0fz.s ( 𝜑𝑆 ∈ ℕ0 )
6 gsummptnn0fz.u ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘𝐶 = 0 ) )
7 nfv 𝑥 ( 𝑆 < 𝑘𝐶 = 0 )
8 nfv 𝑘 𝑆 < 𝑥
9 nfcsb1v 𝑘 𝑥 / 𝑘 𝐶
10 9 nfeq1 𝑘 𝑥 / 𝑘 𝐶 = 0
11 8 10 nfim 𝑘 ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 )
12 breq2 ( 𝑘 = 𝑥 → ( 𝑆 < 𝑘𝑆 < 𝑥 ) )
13 csbeq1a ( 𝑘 = 𝑥𝐶 = 𝑥 / 𝑘 𝐶 )
14 13 eqeq1d ( 𝑘 = 𝑥 → ( 𝐶 = 0 𝑥 / 𝑘 𝐶 = 0 ) )
15 12 14 imbi12d ( 𝑘 = 𝑥 → ( ( 𝑆 < 𝑘𝐶 = 0 ) ↔ ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 ) ) )
16 7 11 15 cbvralw ( ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘𝐶 = 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 ) )
17 6 16 sylib ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 ) )
18 simpr ( ( 𝜑𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
19 4 anim1ci ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶𝐵 ) )
20 rspcsbela ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶𝐵 ) → 𝑥 / 𝑘 𝐶𝐵 )
21 19 20 syl ( ( 𝜑𝑥 ∈ ℕ0 ) → 𝑥 / 𝑘 𝐶𝐵 )
22 18 21 jca ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ℕ0 𝑥 / 𝑘 𝐶𝐵 ) )
23 22 adantr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑥 / 𝑘 𝐶 = 0 ) → ( 𝑥 ∈ ℕ0 𝑥 / 𝑘 𝐶𝐵 ) )
24 eqid ( 𝑘 ∈ ℕ0𝐶 ) = ( 𝑘 ∈ ℕ0𝐶 )
25 24 fvmpts ( ( 𝑥 ∈ ℕ0 𝑥 / 𝑘 𝐶𝐵 ) → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 𝑥 / 𝑘 𝐶 )
26 23 25 syl ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑥 / 𝑘 𝐶 = 0 ) → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 𝑥 / 𝑘 𝐶 )
27 simpr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑥 / 𝑘 𝐶 = 0 ) → 𝑥 / 𝑘 𝐶 = 0 )
28 26 27 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑥 / 𝑘 𝐶 = 0 ) → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 )
29 28 ex ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑥 / 𝑘 𝐶 = 0 → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 ) )
30 29 imim2d ( ( 𝜑𝑥 ∈ ℕ0 ) → ( ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 ) → ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 ) ) )
31 30 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 𝑥 / 𝑘 𝐶 = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 ) ) )
32 17 31 mpd ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 ) )
33 24 fmpt ( ∀ 𝑘 ∈ ℕ0 𝐶𝐵 ↔ ( 𝑘 ∈ ℕ0𝐶 ) : ℕ0𝐵 )
34 4 33 sylib ( 𝜑 → ( 𝑘 ∈ ℕ0𝐶 ) : ℕ0𝐵 )
35 1 fvexi 𝐵 ∈ V
36 nn0ex 0 ∈ V
37 35 36 pm3.2i ( 𝐵 ∈ V ∧ ℕ0 ∈ V )
38 elmapg ( ( 𝐵 ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑘 ∈ ℕ0𝐶 ) ∈ ( 𝐵m0 ) ↔ ( 𝑘 ∈ ℕ0𝐶 ) : ℕ0𝐵 ) )
39 37 38 mp1i ( 𝜑 → ( ( 𝑘 ∈ ℕ0𝐶 ) ∈ ( 𝐵m0 ) ↔ ( 𝑘 ∈ ℕ0𝐶 ) : ℕ0𝐵 ) )
40 34 39 mpbird ( 𝜑 → ( 𝑘 ∈ ℕ0𝐶 ) ∈ ( 𝐵m0 ) )
41 fz0ssnn0 ( 0 ... 𝑆 ) ⊆ ℕ0
42 resmpt ( ( 0 ... 𝑆 ) ⊆ ℕ0 → ( ( 𝑘 ∈ ℕ0𝐶 ) ↾ ( 0 ... 𝑆 ) ) = ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) )
43 41 42 ax-mp ( ( 𝑘 ∈ ℕ0𝐶 ) ↾ ( 0 ... 𝑆 ) ) = ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 )
44 43 eqcomi ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) = ( ( 𝑘 ∈ ℕ0𝐶 ) ↾ ( 0 ... 𝑆 ) )
45 1 2 3 40 5 44 fsfnn0gsumfsffz ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0𝐶 ) ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg ( 𝑘 ∈ ℕ0𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) ) )
46 32 45 mpd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) )