# 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 ${⊢}{B}={\mathrm{Base}}_{{G}}$
nn0gsumfz.0
nn0gsumfz.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
nn0gsumfz.f ${⊢}{\phi }\to {F}\in \left({{B}}^{{ℕ}_{0}}\right)$
nn0gsumfz.y
Assertion nn0gsumfz

### Proof

Step Hyp Ref Expression
1 nn0gsumfz.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 nn0gsumfz.0
3 nn0gsumfz.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 nn0gsumfz.f ${⊢}{\phi }\to {F}\in \left({{B}}^{{ℕ}_{0}}\right)$
5 nn0gsumfz.y
6 2 fvexi
7 4 6 jctir
8 fsuppmapnn0ub
9 7 5 8 sylc
10 eqidd
11 simpr
12 3 adantr ${⊢}\left({\phi }\wedge {s}\in {ℕ}_{0}\right)\to {G}\in \mathrm{CMnd}$
13 4 adantr ${⊢}\left({\phi }\wedge {s}\in {ℕ}_{0}\right)\to {F}\in \left({{B}}^{{ℕ}_{0}}\right)$
14 simpr ${⊢}\left({\phi }\wedge {s}\in {ℕ}_{0}\right)\to {s}\in {ℕ}_{0}$
15 eqid ${⊢}{{F}↾}_{\left(0\dots {s}\right)}={{F}↾}_{\left(0\dots {s}\right)}$
16 1 2 12 13 14 15 fsfnn0gsumfsffz
17 16 imp
19 fz0ssnn0 ${⊢}\left(0\dots {s}\right)\subseteq {ℕ}_{0}$
20 elmapssres ${⊢}\left({F}\in \left({{B}}^{{ℕ}_{0}}\right)\wedge \left(0\dots {s}\right)\subseteq {ℕ}_{0}\right)\to {{F}↾}_{\left(0\dots {s}\right)}\in \left({{B}}^{\left(0\dots {s}\right)}\right)$
22 eqeq1 ${⊢}{f}={{F}↾}_{\left(0\dots {s}\right)}\to \left({f}={{F}↾}_{\left(0\dots {s}\right)}↔{{F}↾}_{\left(0\dots {s}\right)}={{F}↾}_{\left(0\dots {s}\right)}\right)$
23 oveq2 ${⊢}{f}={{F}↾}_{\left(0\dots {s}\right)}\to {\sum }_{{G}}{f}={\sum }_{{G}}\left({{F}↾}_{\left(0\dots {s}\right)}\right)$
24 23 eqeq2d ${⊢}{f}={{F}↾}_{\left(0\dots {s}\right)}\to \left({\sum }_{{G}}{F}={\sum }_{{G}}{f}↔{\sum }_{{G}}{F}={\sum }_{{G}}\left({{F}↾}_{\left(0\dots {s}\right)}\right)\right)$