Metamath Proof Explorer

Theorem mulgval

Description: Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgval.b 
|- B = ( Base ` G )
mulgval.p 
|- .+ = ( +g ` G )
mulgval.o 
|- .0. = ( 0g ` G )
mulgval.i 
|- I = ( invg ` G )
mulgval.t 
|- .x. = ( .g ` G )
mulgval.s 
|- S = seq 1 ( .+ , ( NN X. { X } ) )
Assertion mulgval 
|- ( ( N e. ZZ /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , .0. , if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulgval.b 
 |-  B = ( Base ` G )
2 mulgval.p 
 |-  .+ = ( +g ` G )
3 mulgval.o 
 |-  .0. = ( 0g ` G )
4 mulgval.i 
 |-  I = ( invg ` G )
5 mulgval.t 
 |-  .x. = ( .g ` G )
6 mulgval.s 
 |-  S = seq 1 ( .+ , ( NN X. { X } ) )
7 simpl 
 |-  ( ( n = N /\ x = X ) -> n = N )
8 7 eqeq1d 
 |-  ( ( n = N /\ x = X ) -> ( n = 0 <-> N = 0 ) )
9 7 breq2d 
 |-  ( ( n = N /\ x = X ) -> ( 0 < n <-> 0 < N ) )
10 simpr 
 |-  ( ( n = N /\ x = X ) -> x = X )
11 10 sneqd 
 |-  ( ( n = N /\ x = X ) -> { x } = { X } )
12 11 xpeq2d 
 |-  ( ( n = N /\ x = X ) -> ( NN X. { x } ) = ( NN X. { X } ) )
13 12 seqeq3d 
 |-  ( ( n = N /\ x = X ) -> seq 1 ( .+ , ( NN X. { x } ) ) = seq 1 ( .+ , ( NN X. { X } ) ) )
14 13 6 eqtr4di 
 |-  ( ( n = N /\ x = X ) -> seq 1 ( .+ , ( NN X. { x } ) ) = S )
15 14 7 fveq12d 
 |-  ( ( n = N /\ x = X ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) = ( S ` N ) )
16 7 negeqd 
 |-  ( ( n = N /\ x = X ) -> -u n = -u N )
17 14 16 fveq12d 
 |-  ( ( n = N /\ x = X ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) = ( S ` -u N ) )
18 17 fveq2d 
 |-  ( ( n = N /\ x = X ) -> ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) = ( I ` ( S ` -u N ) ) )
19 9 15 18 ifbieq12d 
 |-  ( ( n = N /\ x = X ) -> if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) = if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) )
20 8 19 ifbieq2d 
 |-  ( ( n = N /\ x = X ) -> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) = if ( N = 0 , .0. , if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) )
21 1 2 3 4 5 mulgfval 
 |-  .x. = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )
22 3 fvexi 
 |-  .0. e. _V
23 fvex 
 |-  ( S ` N ) e. _V
24 fvex 
 |-  ( I ` ( S ` -u N ) ) e. _V
25 23 24 ifex 
 |-  if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) e. _V
26 22 25 ifex 
 |-  if ( N = 0 , .0. , if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) e. _V
27 20 21 26 ovmpoa 
 |-  ( ( N e. ZZ /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , .0. , if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) )