This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgnn0gsum

Description: Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in Lang p. 6, second formula. (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 mulgnn0gsum 
|- ( ( N e. NN0 /\ 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 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5 1 2 3 mulgnngsum 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )
6 5 ex 
 |-  ( N e. NN -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
7 oveq1 
 |-  ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 1 8 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
10 7 9 sylan9eq 
 |-  ( ( N = 0 /\ X e. B ) -> ( N .x. X ) = ( 0g ` G ) )
11 oveq2 
 |-  ( N = 0 -> ( 1 ... N ) = ( 1 ... 0 ) )
12 fz10 
 |-  ( 1 ... 0 ) = (/)
13 11 12 eqtrdi 
 |-  ( N = 0 -> ( 1 ... N ) = (/) )
14 eqidd 
 |-  ( N = 0 -> X = X )
15 13 14 mpteq12dv 
 |-  ( N = 0 -> ( x e. ( 1 ... N ) |-> X ) = ( x e. (/) |-> X ) )
16 mpt0 
 |-  ( x e. (/) |-> X ) = (/)
17 15 16 eqtrdi 
 |-  ( N = 0 -> ( x e. ( 1 ... N ) |-> X ) = (/) )
18 3 17 eqtrid 
 |-  ( N = 0 -> F = (/) )
19 18 adantr 
 |-  ( ( N = 0 /\ X e. B ) -> F = (/) )
20 19 oveq2d 
 |-  ( ( N = 0 /\ X e. B ) -> ( G gsum F ) = ( G gsum (/) ) )
21 8 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
22 20 21 eqtrdi 
 |-  ( ( N = 0 /\ X e. B ) -> ( G gsum F ) = ( 0g ` G ) )
23 10 22 eqtr4d 
 |-  ( ( N = 0 /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )
24 23 ex 
 |-  ( N = 0 -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
25 6 24 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
26 4 25 sylbi 
 |-  ( N e. NN0 -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
27 26 imp 
 |-  ( ( N e. NN0 /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )