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

Metamath Proof Explorer

Theorem telgsumfz0

Description: Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum . (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses telgsumfz0.k ⊢ 𝐾 = ( Base ‘ 𝐺 )
telgsumfz0.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
telgsumfz0.m ⊢ − = ( -g ‘ 𝐺 )
telgsumfz0.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
telgsumfz0.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐴 ∈ 𝐾 )
telgsumfz0.a ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐵 )
telgsumfz0.c ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐶 )
telgsumfz0.d ⊢ ( 𝑘 = 0 → 𝐴 = 𝐷 )
telgsumfz0.e ⊢ ( 𝑘 = ( 𝑆 + 1 ) → 𝐴 = 𝐸 )
Assertion telgsumfz0 ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐵 − 𝐶 ) ) ) = ( 𝐷 − 𝐸 ) )

Proof

Step Hyp Ref Expression
1 telgsumfz0.k ⊢ 𝐾 = ( Base ‘ 𝐺 )
2 telgsumfz0.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsumfz0.m ⊢ − = ( -g ‘ 𝐺 )
4 telgsumfz0.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
5 telgsumfz0.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐴 ∈ 𝐾 )
6 telgsumfz0.a ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐵 )
7 telgsumfz0.c ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐶 )
8 telgsumfz0.d ⊢ ( 𝑘 = 0 → 𝐴 = 𝐷 )
9 telgsumfz0.e ⊢ ( 𝑘 = ( 𝑆 + 1 ) → 𝐴 = 𝐸 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → 𝑖 ∈ ( 0 ... 𝑆 ) )
11 6 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) ∧ 𝑘 = 𝑖 ) → 𝐴 = 𝐵 )
12 10 11 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐴 = 𝐵 )
13 12 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
14 ovexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → ( 𝑖 + 1 ) ∈ V )
15 7 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) ∧ 𝑘 = ( 𝑖 + 1 ) ) → 𝐴 = 𝐶 )
16 14 15 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐶 )
17 16 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → 𝐶 = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 )
18 13 17 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑆 ) ) → ( 𝐵 − 𝐶 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐵 − 𝐶 ) ) = ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
20 19 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐵 − 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) )
21 1 2 3 4 5 telgsumfz0s ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) = ( ⦋ 0 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐴 ) )
22 c0ex ⊢ 0 ∈ V
23 22 a1i ⊢ ( 𝜑 → 0 ∈ V )
24 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → 𝐴 = 𝐷 )
25 23 24 csbied ⊢ ( 𝜑 → ⦋ 0 / 𝑘 ⦌ 𝐴 = 𝐷 )
26 ovexd ⊢ ( 𝜑 → ( 𝑆 + 1 ) ∈ V )
27 9 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = ( 𝑆 + 1 ) ) → 𝐴 = 𝐸 )
28 26 27 csbied ⊢ ( 𝜑 → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐸 )
29 25 28 oveq12d ⊢ ( 𝜑 → ( ⦋ 0 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐴 ) = ( 𝐷 − 𝐸 ) )
30 20 21 29 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐵 − 𝐶 ) ) ) = ( 𝐷 − 𝐸 ) )