Metamath Proof Explorer

Theorem mulgnn

Description: Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnn.b 
|- B = ( Base ` G )
mulgnn.p 
|- .+ = ( +g ` G )
mulgnn.t 
|- .x. = ( .g ` G )
mulgnn.s 
|- S = seq 1 ( .+ , ( NN X. { X } ) )
Assertion mulgnn 
|- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( S ` N ) )

Proof

Step Hyp Ref Expression
1 mulgnn.b 
 |-  B = ( Base ` G )
2 mulgnn.p 
 |-  .+ = ( +g ` G )
3 mulgnn.t 
 |-  .x. = ( .g ` G )
4 mulgnn.s 
 |-  S = seq 1 ( .+ , ( NN X. { X } ) )
5 nnz 
 |-  ( N e. NN -> N e. ZZ )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 eqid 
 |-  ( invg ` G ) = ( invg ` G )
8 1 2 6 7 3 4 mulgval 
 |-  ( ( N e. ZZ /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) ) )
9 5 8 sylan 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) ) )
10 nnne0 
 |-  ( N e. NN -> N =/= 0 )
11 10 neneqd 
 |-  ( N e. NN -> -. N = 0 )
12 11 iffalsed 
 |-  ( N e. NN -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) ) = if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) )
13 nngt0 
 |-  ( N e. NN -> 0 < N )
14 13 iftrued 
 |-  ( N e. NN -> if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) = ( S ` N ) )
15 12 14 eqtrd 
 |-  ( N e. NN -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) ) = ( S ` N ) )
16 15 adantr 
 |-  ( ( N e. NN /\ X e. B ) -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( S ` N ) , ( ( invg ` G ) ` ( S ` -u N ) ) ) ) = ( S ` N ) )
17 9 16 eqtrd 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( S ` N ) )