This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑓 ) )