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

Definition df-gx 23861
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 23856 . 2  class  ^g
2 vg . . 3  setvar  g
3 cgr 23852 . . 3  class  GrpOp
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1369 . . . . 5  class  g
76crn 4952 . . . 4  class  ran  g
8 cz 10761 . . . 4  class  ZZ
95cv 1369 . . . . . 6  class  y
10 cc0 9397 . . . . . 6  class  0
119, 10wceq 1370 . . . . 5  wff  y  =  0
12 cgi 23853 . . . . . 6  class GId
136, 12cfv 5529 . . . . 5  class  (GId `  g )
14 clt 9533 . . . . . . 7  class  <
1510, 9, 14wbr 4403 . . . . . 6  wff  0  <  y
16 cn 10437 . . . . . . . . 9  class  NN
174cv 1369 . . . . . . . . . 10  class  x
1817csn 3988 . . . . . . . . 9  class  { x }
1916, 18cxp 4949 . . . . . . . 8  class  ( NN 
X.  { x }
)
20 c1 9398 . . . . . . . 8  class  1
216, 19, 20cseq 11927 . . . . . . 7  class  seq 1
( g ,  ( NN  X.  { x } ) )
229, 21cfv 5529 . . . . . 6  class  (  seq 1 ( g ,  ( NN  X.  {
x } ) ) `
 y )
239cneg 9711 . . . . . . . 8  class  -u y
2423, 21cfv 5529 . . . . . . 7  class  (  seq 1 ( g ,  ( NN  X.  {
x } ) ) `
 -u y )
25 cgn 23854 . . . . . . . 8  class  inv
266, 25cfv 5529 . . . . . . 7  class  ( inv `  g )
2724, 26cfv 5529 . . . . . 6  class  ( ( inv `  g ) `
 (  seq 1
( g ,  ( NN  X.  { x } ) ) `  -u y ) )
2815, 22, 27cif 3902 . . . . 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 3902 . . . 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 6205 . . 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 4461 . 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 1370 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 setvar class
This definition is referenced by:  gxfval  23923
  Copyright terms: Public domain W3C validator