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 = ( Base ` G )
gsummptfzcl.g 
|- ( ph -> G e. Mnd )
gsummptfzcl.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
gsummptfzcl.i 
|- ( ph -> I = ( M ... N ) )
gsummptfzcl.e 
|- ( ph -> A. i e. I X e. B )
Assertion gsummptfzcl 
|- ( ph -> ( G gsum ( i e. I |-> X ) ) e. B )

Proof

Step Hyp Ref Expression
1 gsummptfzcl.b 
 |-  B = ( Base ` G )
2 gsummptfzcl.g 
 |-  ( ph -> G e. Mnd )
3 gsummptfzcl.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 gsummptfzcl.i 
 |-  ( ph -> I = ( M ... N ) )
5 gsummptfzcl.e 
 |-  ( ph -> A. i e. I X e. B )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 eqid 
 |-  ( i e. I |-> X ) = ( i e. I |-> X )
8 7 fmpt 
 |-  ( A. i e. I X e. B <-> ( i e. I |-> X ) : I --> B )
9 4 feq2d 
 |-  ( ph -> ( ( i e. I |-> X ) : I --> B <-> ( i e. I |-> X ) : ( M ... N ) --> B ) )
10 8 9 bitrid 
 |-  ( ph -> ( A. i e. I X e. B <-> ( i e. I |-> X ) : ( M ... N ) --> B ) )
11 5 10 mpbid 
 |-  ( ph -> ( i e. I |-> X ) : ( M ... N ) --> B )
12 1 6 2 3 11 gsumval2 
 |-  ( ph -> ( G gsum ( i e. I |-> X ) ) = ( seq M ( ( +g ` G ) , ( i e. I |-> X ) ) ` N ) )
13 5 adantr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> A. i e. I X e. B )
14 13 8 sylib 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( i e. I |-> X ) : I --> B )
15 4 eqcomd 
 |-  ( ph -> ( M ... N ) = I )
16 15 eleq2d 
 |-  ( ph -> ( x e. ( M ... N ) <-> x e. I ) )
17 16 biimpa 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. I )
18 14 17 ffvelcdmd 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( i e. I |-> X ) ` x ) e. B )
19 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> G e. Mnd )
20 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
21 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
22 1 6 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B )
24 3 18 23 seqcl 
 |-  ( ph -> ( seq M ( ( +g ` G ) , ( i e. I |-> X ) ) ` N ) e. B )
25 12 24 eqeltrd 
 |-  ( ph -> ( G gsum ( i e. I |-> X ) ) e. B )