Theorem fsfnn0gsumfsffz

Description: Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019)

	Ref	Expression
Hypotheses	nn0gsumfz.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	nn0gsumfz.0	⊢ 0 = ( 0g ‘ 𝐺 )
	nn0gsumfz.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	nn0gsumfz.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
	fsfnn0gsumfsffz.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	fsfnn0gsumfsffz.h	⊢ 𝐻 = ( 𝐹 ↾ ( 0 ... 𝑆 ) )
Assertion	fsfnn0gsumfsffz	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0gsumfz.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		nn0gsumfz.0	⊢ 0 = ( 0g ‘ 𝐺 )
3		nn0gsumfz.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		nn0gsumfz.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
5		fsfnn0gsumfsffz.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
6		fsfnn0gsumfsffz.h	⊢ 𝐻 = ( 𝐹 ↾ ( 0 ... 𝑆 ) )
7	6	oveq2i	⊢ ( 𝐺 Σg 𝐻 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑆 ) ) )
8	3	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐺 ∈ CMnd )
9		nn0ex	⊢ ℕ0 ∈ V
10	9	a1i	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ℕ0 ∈ V )
11		elmapi	⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → 𝐹 : ℕ0 ⟶ 𝐵 )
12	4 11	syl	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝐵 )
13	12	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 : ℕ0 ⟶ 𝐵 )
14	2	fvexi	⊢ 0 ∈ V
15	14	a1i	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 0 ∈ V )
16	4	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
17	5	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑆 ∈ ℕ0 )
18		simpr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
19	15 16 17 18	suppssfz	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) )
20		elmapfun	⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → Fun 𝐹 )
21	4 20	syl	⊢ ( 𝜑 → Fun 𝐹 )
22	14	a1i	⊢ ( 𝜑 → 0 ∈ V )
23	4 21 22	3jca	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) ∧ Fun 𝐹 ∧ 0 ∈ V ) )
24		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑆 ) ∈ Fin )
25	24	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) → ( ( 0 ... 𝑆 ) ∈ Fin ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) )
26		suppssfifsupp	⊢ ( ( ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) ∧ Fun 𝐹 ∧ 0 ∈ V ) ∧ ( ( 0 ... 𝑆 ) ∈ Fin ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) ) → 𝐹 finSupp 0 )
27	23 25 26	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) → 𝐹 finSupp 0 )
28	19 27	syldan	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 finSupp 0 )
29	1 2 8 10 13 19 28	gsumres	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑆 ) ) ) = ( 𝐺 Σg 𝐹 ) )
30	7 29	syl5req	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) )
31	30	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ) )