MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mulg Unicode version

Definition df-mulg 14487
Description: Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)
Assertion
Ref Expression
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 ) ,  ( ( inv g `  g ) `
 ( s `  -u n ) ) ) ) ) )
Distinct variable group:    g, n, s, x

Detailed syntax breakdown of Definition df-mulg
StepHypRef Expression
1 cmg 14361 . 2  class .g
2 vg . . 3  set  g
3 cvv 2790 . . 3  class  _V
4 vn . . . 4  set  n
5 vx . . . 4  set  x
6 cz 10020 . . . 4  class  ZZ
72cv 1623 . . . . 5  class  g
8 cbs 13143 . . . . 5  class  Base
97, 8cfv 5222 . . . 4  class  ( Base `  g )
104cv 1623 . . . . . 6  class  n
11 cc0 8733 . . . . . 6  class  0
1210, 11wceq 1624 . . . . 5  wff  n  =  0
13 c0g 13395 . . . . . 6  class  0g
147, 13cfv 5222 . . . . 5  class  ( 0g
`  g )
15 vs . . . . . 6  set  s
16 cplusg 13203 . . . . . . . 8  class  +g
177, 16cfv 5222 . . . . . . 7  class  ( +g  `  g )
18 cn 9742 . . . . . . . 8  class  NN
195cv 1623 . . . . . . . . 9  class  x
2019csn 3642 . . . . . . . 8  class  { x }
2118, 20cxp 4687 . . . . . . 7  class  ( NN 
X.  { x }
)
22 c1 8734 . . . . . . 7  class  1
2317, 21, 22cseq 11041 . . . . . 6  class  seq  1
( ( +g  `  g
) ,  ( NN 
X.  { x }
) )
24 clt 8863 . . . . . . . 8  class  <
2511, 10, 24wbr 4025 . . . . . . 7  wff  0  <  n
2615cv 1623 . . . . . . . 8  class  s
2710, 26cfv 5222 . . . . . . 7  class  ( s `
 n )
2810cneg 9034 . . . . . . . . 9  class  -u n
2928, 26cfv 5222 . . . . . . . 8  class  ( s `
 -u n )
30 cminusg 14358 . . . . . . . . 9  class  inv g
317, 30cfv 5222 . . . . . . . 8  class  ( inv g `  g )
3229, 31cfv 5222 . . . . . . 7  class  ( ( inv g `  g
) `  ( s `  -u n ) )
3325, 27, 32cif 3567 . . . . . 6  class  if ( 0  <  n ,  ( s `  n
) ,  ( ( inv g `  g
) `  ( s `  -u n ) ) )
3415, 23, 33csb 3083 . . . . 5  class  [_  seq  1 ( ( +g  `  g ) ,  ( NN  X.  { x } ) )  / 
s ]_ if ( 0  <  n ,  ( s `  n ) ,  ( ( inv g `  g ) `
 ( s `  -u n ) ) )
3512, 14, 34cif 3567 . . . 4  class  if ( n  =  0 ,  ( 0g `  g
) ,  [_  seq  1 ( ( +g  `  g ) ,  ( NN  X.  { x } ) )  / 
s ]_ if ( 0  <  n ,  ( s `  n ) ,  ( ( inv g `  g ) `
 ( s `  -u n ) ) ) )
364, 5, 6, 9, 35cmpt2 5822 . . 3  class  ( 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 ) ,  ( ( inv g `  g ) `  (
s `  -u n ) ) ) ) )
372, 3, 36cmpt 4079 . 2  class  ( 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 ) ,  ( ( inv g `  g ) `  (
s `  -u n ) ) ) ) ) )
381, 37wceq 1624 1  wff .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 ) ,  ( ( inv g `  g ) `
 ( s `  -u n ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  mulgfval  14563
  Copyright terms: Public domain W3C validator