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 ( 𝜑𝐹 ∈ ( 𝐵m0 ) )
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 ( 𝜑𝐹 ∈ ( 𝐵m0 ) )
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 ( 𝐹 ∈ ( 𝐵m0 ) → 𝐹 : ℕ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 ) ) → 𝐹 ∈ ( 𝐵m0 ) )
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 ( 𝐹 ∈ ( 𝐵m0 ) → Fun 𝐹 )
21 4 20 syl ( 𝜑 → Fun 𝐹 )
22 14 a1i ( 𝜑0 ∈ V )
23 4 21 22 3jca ( 𝜑 → ( 𝐹 ∈ ( 𝐵m0 ) ∧ Fun 𝐹0 ∈ V ) )
24 fzfid ( 𝜑 → ( 0 ... 𝑆 ) ∈ Fin )
25 24 anim1i ( ( 𝜑 ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) → ( ( 0 ... 𝑆 ) ∈ Fin ∧ ( 𝐹 supp 0 ) ⊆ ( 0 ... 𝑆 ) ) )
26 suppssfifsupp ( ( ( 𝐹 ∈ ( 𝐵m0 ) ∧ 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 𝐻 ) ) )