Theorem nn0gsumfz

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 ) )
	nn0gsumfz.y	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	nn0gsumfz	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ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		nn0gsumfz.y	⊢ ( 𝜑 → 𝐹 finSupp 0 )
6	2	fvexi	⊢ 0 ∈ V
7	4 6	jctir	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) ∧ 0 ∈ V ) )
8		fsuppmapnn0ub	⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) ∧ 0 ∈ V ) → ( 𝐹 finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
9	7 5 8	sylc	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
10		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → 𝐺 ∈ CMnd )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 )
15		eqid	⊢ ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) )
16	1 2 12 13 14 15	fsfnn0gsumfsffz	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) ) )
17	16	imp	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) )
18	13	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
19		fz0ssnn0	⊢ ( 0 ... 𝑠 ) ⊆ ℕ0
20		elmapssres	⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) ∧ ( 0 ... 𝑠 ) ⊆ ℕ0 ) → ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
21	18 19 20	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
22		eqeq1	⊢ ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) → ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ↔ ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) )
23		oveq2	⊢ ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) )
24	23	eqeq2d	⊢ ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) → ( ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ↔ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) ) )
25	22 24	3anbi13d	⊢ ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) → ( ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ↔ ( ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) ) ) )
26	25	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) ∧ 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) → ( ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ↔ ( ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) ) ) )
27	21 26	rspcedv	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( ( 𝐹 ↾ ( 0 ... 𝑠 ) ) = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ) ) → ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
28	10 11 17 27	mp3and	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) )
29	28	ex	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
30	29	reximdva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
31	9 30	mpd	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) )