Metamath Proof Explorer

Definition df-mulg

Description: Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Assertion df-mulg 
|- .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmg 
 |-  .g
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vn 
 |-  n
4 cz 
 |-  ZZ
5 vx 
 |-  x
6 cbs 
 |-  Base
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Base ` g )
9 3 cv 
 |-  n
10 cc0 
 |-  0
11 9 10 wceq 
 |-  n = 0
12 c0g 
 |-  0g
13 7 12 cfv 
 |-  ( 0g ` g )
14 c1 
 |-  1
15 cplusg 
 |-  +g
16 7 15 cfv 
 |-  ( +g ` g )
17 cn 
 |-  NN
18 5 cv 
 |-  x
19 18 csn 
 |-  { x }
20 17 19 cxp 
 |-  ( NN X. { x } )
21 16 20 14 cseq 
 |-  seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
22 vs 
 |-  s
23 clt 
 |-  <
24 10 9 23 wbr 
 |-  0 < n
25 22 cv 
 |-  s
26 9 25 cfv 
 |-  ( s ` n )
27 cminusg 
 |-  invg
28 7 27 cfv 
 |-  ( invg ` g )
29 9 cneg 
 |-  -u n
30 29 25 cfv 
 |-  ( s ` -u n )
31 30 28 cfv 
 |-  ( ( invg ` g ) ` ( s ` -u n ) )
32 24 26 31 cif 
 |-  if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
33 22 21 32 csb 
 |-  [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34 11 13 33 cif 
 |-  if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) )
35 3 5 4 8 34 cmpo 
 |-  ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) )
36 1 2 35 cmpt 
 |-  ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )
37 0 36 wceq 
 |-  .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )