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

Definition df-gx 20862
Description: Define a function that maps a group operation to the group's power operation. (Contributed by Paul Chapman, 17-Apr-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-gx  |-  ^g  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g ,  y  e.  ZZ  |->  if ( y  =  0 ,  (GId
`  g ) ,  if ( 0  < 
y ,  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 y ) ,  ( ( inv `  g
) `  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y ) ) ) ) ) )
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-gx
StepHypRef Expression
1 cgx 20857 . 2  class  ^g
2 vg . . 3  set  g
3 cgr 20853 . . 3  class  GrpOp
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . 5  class  g
76crn 4690 . . . 4  class  ran  g
8 cz 10024 . . . 4  class  ZZ
95cv 1622 . . . . . 6  class  y
10 cc0 8737 . . . . . 6  class  0
119, 10wceq 1623 . . . . 5  wff  y  =  0
12 cgi 20854 . . . . . 6  class GId
136, 12cfv 5255 . . . . 5  class  (GId `  g )
14 clt 8867 . . . . . . 7  class  <
1510, 9, 14wbr 4023 . . . . . 6  wff  0  <  y
16 cn 9746 . . . . . . . . 9  class  NN
174cv 1622 . . . . . . . . . 10  class  x
1817csn 3640 . . . . . . . . 9  class  { x }
1916, 18cxp 4687 . . . . . . . 8  class  ( NN 
X.  { x }
)
20 c1 8738 . . . . . . . 8  class  1
216, 19, 20cseq 11046 . . . . . . 7  class  seq  1
( g ,  ( NN  X.  { x } ) )
229, 21cfv 5255 . . . . . 6  class  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 y )
239cneg 9038 . . . . . . . 8  class  -u y
2423, 21cfv 5255 . . . . . . 7  class  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y )
25 cgn 20855 . . . . . . . 8  class  inv
266, 25cfv 5255 . . . . . . 7  class  ( inv `  g )
2724, 26cfv 5255 . . . . . 6  class  ( ( inv `  g ) `
 (  seq  1
( g ,  ( NN  X.  { x } ) ) `  -u y ) )
2815, 22, 27cif 3565 . . . . 5  class  if ( 0  <  y ,  (  seq  1 ( g ,  ( NN 
X.  { x }
) ) `  y
) ,  ( ( inv `  g ) `
 (  seq  1
( g ,  ( NN  X.  { x } ) ) `  -u y ) ) )
2911, 13, 28cif 3565 . . . 4  class  if ( y  =  0 ,  (GId `  g ) ,  if ( 0  < 
y ,  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 y ) ,  ( ( inv `  g
) `  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y ) ) ) )
304, 5, 7, 8, 29cmpt2 5860 . . 3  class  ( x  e.  ran  g ,  y  e.  ZZ  |->  if ( y  =  0 ,  (GId `  g
) ,  if ( 0  <  y ,  (  seq  1 ( g ,  ( NN 
X.  { x }
) ) `  y
) ,  ( ( inv `  g ) `
 (  seq  1
( g ,  ( NN  X.  { x } ) ) `  -u y ) ) ) ) )
312, 3, 30cmpt 4077 . 2  class  ( g  e.  GrpOp  |->  ( x  e. 
ran  g ,  y  e.  ZZ  |->  if ( y  =  0 ,  (GId `  g ) ,  if ( 0  < 
y ,  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 y ) ,  ( ( inv `  g
) `  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y ) ) ) ) ) )
321, 31wceq 1623 1  wff  ^g  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g ,  y  e.  ZZ  |->  if ( y  =  0 ,  (GId
`  g ) ,  if ( 0  < 
y ,  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 y ) ,  ( ( inv `  g
) `  (  seq  1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  gxfval  20924
  Copyright terms: Public domain W3C validator