Theorem gsummptnn0fzfv

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

	Ref	Expression
Hypotheses	gsummptnn0fzfv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptnn0fzfv.0	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptnn0fzfv.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptnn0fzfv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
	gsummptnn0fzfv.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	gsummptnn0fzfv.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
Assertion	gsummptnn0fzfv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptnn0fzfv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptnn0fzfv.0	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummptnn0fzfv.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptnn0fzfv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
5		gsummptnn0fzfv.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
6		gsummptnn0fzfv.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
7		elmapi	⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → 𝐹 : ℕ0 ⟶ 𝐵 )
8		ffvelrn	⊢ ( ( 𝐹 : ℕ0 ⟶ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
9	8	ex	⊢ ( 𝐹 : ℕ0 ⟶ 𝐵 → ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
10	4 7 9	3syl	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
11	10	ralrimiv	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
12		breq2	⊢ ( 𝑥 = 𝑘 → ( 𝑆 < 𝑥 ↔ 𝑆 < 𝑘 ) )
13		fveqeq2	⊢ ( 𝑥 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑘 ) = 0 ) )
14	12 13	imbi12d	⊢ ( 𝑥 = 𝑘 → ( ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) ) )
15	14	cbvralvw	⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) )
16	6 15	sylib	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) )
17	1 2 3 11 5 16	gsummptnn0fz	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )