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 ... 𝑆 ) ↦ 𝐶 ) ) )