# Metamath Proof Explorer

## Theorem gsummptfzcl

Description: Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018)

Ref Expression
Hypotheses gsummptfzcl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsummptfzcl.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
gsummptfzcl.n ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
gsummptfzcl.i ${⊢}{\phi }\to {I}=\left({M}\dots {N}\right)$
gsummptfzcl.e ${⊢}{\phi }\to \forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{X}\in {B}$
Assertion gsummptfzcl ${⊢}{\phi }\to \underset{{i}\in {I}}{{\sum }_{{G}}}{X}\in {B}$

### Proof

Step Hyp Ref Expression
1 gsummptfzcl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsummptfzcl.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
3 gsummptfzcl.n ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
4 gsummptfzcl.i ${⊢}{\phi }\to {I}=\left({M}\dots {N}\right)$
5 gsummptfzcl.e ${⊢}{\phi }\to \forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{X}\in {B}$
6 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
7 eqid ${⊢}\left({i}\in {I}⟼{X}\right)=\left({i}\in {I}⟼{X}\right)$
8 7 fmpt ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{X}\in {B}↔\left({i}\in {I}⟼{X}\right):{I}⟶{B}$
9 4 feq2d ${⊢}{\phi }\to \left(\left({i}\in {I}⟼{X}\right):{I}⟶{B}↔\left({i}\in {I}⟼{X}\right):\left({M}\dots {N}\right)⟶{B}\right)$
10 8 9 syl5bb ${⊢}{\phi }\to \left(\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{X}\in {B}↔\left({i}\in {I}⟼{X}\right):\left({M}\dots {N}\right)⟶{B}\right)$
11 5 10 mpbid ${⊢}{\phi }\to \left({i}\in {I}⟼{X}\right):\left({M}\dots {N}\right)⟶{B}$
12 1 6 2 3 11 gsumval2 ${⊢}{\phi }\to \underset{{i}\in {I}}{{\sum }_{{G}}}{X}=seq{M}\left({+}_{{G}},\left({i}\in {I}⟼{X}\right)\right)\left({N}\right)$
13 5 adantr ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to \forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{X}\in {B}$
14 13 8 sylib ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({i}\in {I}⟼{X}\right):{I}⟶{B}$
15 4 eqcomd ${⊢}{\phi }\to \left({M}\dots {N}\right)={I}$
16 15 eleq2d ${⊢}{\phi }\to \left({x}\in \left({M}\dots {N}\right)↔{x}\in {I}\right)$
17 16 biimpa ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {x}\in {I}$
18 14 17 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({i}\in {I}⟼{X}\right)\left({x}\right)\in {B}$
19 2 adantr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {G}\in \mathrm{Mnd}$
20 simprl ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}\in {B}$
21 simprr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {y}\in {B}$
22 1 6 mndcl ${⊢}\left({G}\in \mathrm{Mnd}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {x}{+}_{{G}}{y}\in {B}$
23 19 20 21 22 syl3anc ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{G}}{y}\in {B}$
24 3 18 23 seqcl ${⊢}{\phi }\to seq{M}\left({+}_{{G}},\left({i}\in {I}⟼{X}\right)\right)\left({N}\right)\in {B}$
25 12 24 eqeltrd ${⊢}{\phi }\to \underset{{i}\in {I}}{{\sum }_{{G}}}{X}\in {B}$