This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) )
39 37 38 mp1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) )
40 34 39 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) )
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 ... 𝑆 ) ↦ 𝐶 ) ) )