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