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

Metamath Proof Explorer

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