Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-expsg Unicode version

Definition df-expsg 25465
Description: Define the exponentiation of an element of a monoid. Experimental. I define exponentiation on a monoid (and not on a semi-group or a magma ) because I need an identity element for the basis hypothesis and associativity for interesting properties such as the composite of two exponentiated elements.  ZZ is used in df-gx 20878 here I used  NN0 because the inverse is not defined in a monoid. (Contributed by FL, 2-Sep-2013.)
Assertion
Ref Expression
df-expsg  |-  ^ md  =  ( g  e. MndOp  |->  ( x  e.  ran  g ,  y  e.  NN0  |->  if ( y  =  0 ,  (GId `  g ) ,  (  seq  1 ( g ,  ( NN  x.  { x } ) ) `  y ) ) ) )
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-expsg
StepHypRef Expression
1 clsg 25464 . 2  class  ^ md
2 vg . . 3  set  g
3 cmndo 21020 . . 3  class MndOp
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1631 . . . . 5  class  g
76crn 4706 . . . 4  class  ran  g
8 cn0 9981 . . . 4  class  NN0
95cv 1631 . . . . . 6  class  y
10 cc0 8753 . . . . . 6  class  0
119, 10wceq 1632 . . . . 5  wff  y  =  0
12 cgi 20870 . . . . . 6  class GId
136, 12cfv 5271 . . . . 5  class  (GId `  g )
14 cn 9762 . . . . . . . 8  class  NN
154cv 1631 . . . . . . . . 9  class  x
1615csn 3653 . . . . . . . 8  class  { x }
17 cmul 8758 . . . . . . . 8  class  x.
1814, 16, 17co 5874 . . . . . . 7  class  ( NN  x.  { x }
)
19 c1 8754 . . . . . . 7  class  1
206, 18, 19cseq 11062 . . . . . 6  class  seq  1
( g ,  ( NN  x.  { x } ) )
219, 20cfv 5271 . . . . 5  class  (  seq  1 ( g ,  ( NN  x.  {
x } ) ) `
 y )
2211, 13, 21cif 3578 . . . 4  class  if ( y  =  0 ,  (GId `  g ) ,  (  seq  1
( g ,  ( NN  x.  { x } ) ) `  y ) )
234, 5, 7, 8, 22cmpt2 5876 . . 3  class  ( x  e.  ran  g ,  y  e.  NN0  |->  if ( y  =  0 ,  (GId `  g ) ,  (  seq  1
( g ,  ( NN  x.  { x } ) ) `  y ) ) )
242, 3, 23cmpt 4093 . 2  class  ( g  e. MndOp  |->  ( x  e. 
ran  g ,  y  e.  NN0  |->  if ( y  =  0 ,  (GId `  g ) ,  (  seq  1
( g ,  ( NN  x.  { x } ) ) `  y ) ) ) )
251, 24wceq 1632 1  wff  ^ md  =  ( g  e. MndOp  |->  ( x  e.  ran  g ,  y  e.  NN0  |->  if ( y  =  0 ,  (GId `  g ) ,  (  seq  1 ( g ,  ( NN  x.  { x } ) ) `  y ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator