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

Metamath Proof Explorer

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 eqtr2id ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) )
31 30 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ) )