Theorem nn0gsumfz0

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	nn0gsumfz0	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 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	1 2 3 4 5	nn0gsumfz	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) )
7		simp3	⊢ ( ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
8	7	reximi	⊢ ( ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) → ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
9	8	reximi	⊢ ( ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝑓 = ( 𝐹 ↾ ( 0 ... 𝑠 ) ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
10	6 9	syl	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )