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. is used in df-gx 20878 here I used because the inverse is not defined in a monoid. (Contributed by FL, 2-Sep-2013.)
Assertion
Ref Expression
df-expsg MndOp GId
Distinct variable group:   ,,

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