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

Definition df-mulg 14807
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 14681 . 2  class .g
2 vg . . 3  set  g
3 cvv 2948 . . 3  class  _V
4 vn . . . 4  set  n
5 vx . . . 4  set  x
6 cz 10274 . . . 4  class  ZZ
72cv 1651 . . . . 5  class  g
8 cbs 13461 . . . . 5  class  Base
97, 8cfv 5446 . . . 4  class  ( Base `  g )
104cv 1651 . . . . . 6  class  n
11 cc0 8982 . . . . . 6  class  0
1210, 11wceq 1652 . . . . 5  wff  n  =  0
13 c0g 13715 . . . . . 6  class  0g
147, 13cfv 5446 . . . . 5  class  ( 0g
`  g )
15 vs . . . . . 6  set  s
16 cplusg 13521 . . . . . . . 8  class  +g
177, 16cfv 5446 . . . . . . 7  class  ( +g  `  g )
18 cn 9992 . . . . . . . 8  class  NN
195cv 1651 . . . . . . . . 9  class  x
2019csn 3806 . . . . . . . 8  class  { x }
2118, 20cxp 4868 . . . . . . 7  class  ( NN 
X.  { x }
)
22 c1 8983 . . . . . . 7  class  1
2317, 21, 22cseq 11315 . . . . . 6  class  seq  1
( ( +g  `  g
) ,  ( NN 
X.  { x }
) )
24 clt 9112 . . . . . . . 8  class  <
2511, 10, 24wbr 4204 . . . . . . 7  wff  0  <  n
2615cv 1651 . . . . . . . 8  class  s
2710, 26cfv 5446 . . . . . . 7  class  ( s `
 n )
2810cneg 9284 . . . . . . . . 9  class  -u n
2928, 26cfv 5446 . . . . . . . 8  class  ( s `
 -u n )
30 cminusg 14678 . . . . . . . . 9  class  inv g
317, 30cfv 5446 . . . . . . . 8  class  ( inv g `  g )
3229, 31cfv 5446 . . . . . . 7  class  ( ( inv g `  g
) `  ( s `  -u n ) )
3325, 27, 32cif 3731 . . . . . 6  class  if ( 0  <  n ,  ( s `  n
) ,  ( ( inv g `  g
) `  ( s `  -u n ) ) )
3415, 23, 33csb 3243 . . . . 5  class  [_  seq  1 ( ( +g  `  g ) ,  ( NN  X.  { x } ) )  / 
s ]_ if ( 0  <  n ,  ( s `  n ) ,  ( ( inv g `  g ) `
 ( s `  -u n ) ) )
3512, 14, 34cif 3731 . . . 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 6075 . . 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 4258 . 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 1652 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  14883
  Copyright terms: Public domain W3C validator