Metamath Proof Explorer

Theorem mulgnngsum

Description: Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023)

Ref Expression
Hypotheses mulgnngsum.b 
|- B = ( Base ` G )
mulgnngsum.t 
|- .x. = ( .g ` G )
mulgnngsum.f 
|- F = ( x e. ( 1 ... N ) |-> X )
Assertion mulgnngsum 
|- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )

Proof

Step Hyp Ref Expression
1 mulgnngsum.b 
 |-  B = ( Base ` G )
2 mulgnngsum.t 
 |-  .x. = ( .g ` G )
3 mulgnngsum.f 
 |-  F = ( x e. ( 1 ... N ) |-> X )
4 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
5 4 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
6 5 adantr 
 |-  ( ( N e. NN /\ X e. B ) -> N e. ( ZZ>= ` 1 ) )
7 3 a1i 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> F = ( x e. ( 1 ... N ) |-> X ) )
8 eqidd 
 |-  ( ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) /\ x = i ) -> X = X )
9 simpr 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> i e. ( 1 ... N ) )
10 simpr 
 |-  ( ( N e. NN /\ X e. B ) -> X e. B )
11 10 adantr 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> X e. B )
12 7 8 9 11 fvmptd 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) = X )
13 elfznn 
 |-  ( i e. ( 1 ... N ) -> i e. NN )
14 fvconst2g 
 |-  ( ( X e. B /\ i e. NN ) -> ( ( NN X. { X } ) ` i ) = X )
15 10 13 14 syl2an 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` i ) = X )
16 12 15 eqtr4d 
 |-  ( ( ( N e. NN /\ X e. B ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) = ( ( NN X. { X } ) ` i ) )
17 6 16 seqfveq 
 |-  ( ( N e. NN /\ X e. B ) -> ( seq 1 ( ( +g ` G ) , F ) ` N ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
18 eqid 
 |-  ( +g ` G ) = ( +g ` G )
19 elfvex 
 |-  ( X e. ( Base ` G ) -> G e. _V )
20 19 1 eleq2s 
 |-  ( X e. B -> G e. _V )
21 20 adantl 
 |-  ( ( N e. NN /\ X e. B ) -> G e. _V )
22 10 adantr 
 |-  ( ( ( N e. NN /\ X e. B ) /\ x e. ( 1 ... N ) ) -> X e. B )
23 22 3 fmptd 
 |-  ( ( N e. NN /\ X e. B ) -> F : ( 1 ... N ) --> B )
24 1 18 21 6 23 gsumval2 
 |-  ( ( N e. NN /\ X e. B ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , F ) ` N ) )
25 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
26 1 18 2 25 mulgnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
27 17 24 26 3eqtr4rd 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )