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

Definition df-frsmgrp 25390
Description: Definition of a free semigroup. The definition is somewhat cryptic. Let's say it guarantees the elements of the semigroup can be decomposed into elementary components and that the decomposition is unique. As a consequence you define the elements of the semigroup with nice recursive function  h by giving the value  h ( x ) for every elementary component  x and the recursive equation  h ( x  +  y )  =  h ( x )  +  h ( y ). This is not true in every semigroup. For intance if you take the semigroup of strings generated by the elementary components "ab", "c", "a", "bc", the string "abc" is equal to "ab"  + "c" or to "a"  + "bc" and those beautiful recursive function can't exist. (See a nice explanation in Gallier p. 20.) Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-frsmgrp  |-  FreeSemiGrp  =  { <. g ,  x >.  |  (
g  =  (  subSemiGrpGen  `  <. g ,  x >. )  /\  A. h  e.  SemiGrp  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a ) }
Distinct variable group:    x, g, h, a, u

Detailed syntax breakdown of Definition df-frsmgrp
StepHypRef Expression
1 cfsm 25389 . 2  class  FreeSemiGrp
2 vg . . . . . 6  set  g
32cv 1622 . . . . 5  class  g
4 vx . . . . . . . 8  set  x
54cv 1622 . . . . . . 7  class  x
63, 5cop 3643 . . . . . 6  class  <. g ,  x >.
7 csbsgrg 25385 . . . . . 6  class  subSemiGrpGen
86, 7cfv 5255 . . . . 5  class  (  subSemiGrpGen  `  <. g ,  x >. )
93, 8wceq 1623 . . . 4  wff  g  =  ( 
subSemiGrpGen  `  <. g ,  x >. )
10 vu . . . . . . . . . 10  set  u
1110cv 1622 . . . . . . . . 9  class  u
1211, 5cres 4691 . . . . . . . 8  class  ( u  |`  x )
13 va . . . . . . . . 9  set  a
1413cv 1622 . . . . . . . 8  class  a
1512, 14wceq 1623 . . . . . . 7  wff  ( u  |`  x )  =  a
16 vh . . . . . . . . . 10  set  h
1716cv 1622 . . . . . . . . 9  class  h
183, 17cop 3643 . . . . . . . 8  class  <. g ,  h >.
19 csmhom 25387 . . . . . . . 8  class  SemiGrpHom
2018, 19cfv 5255 . . . . . . 7  class  ( SemiGrpHom `  <. g ,  h >. )
2115, 10, 20wrex 2544 . . . . . 6  wff  E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a
2217cdm 4689 . . . . . . . 8  class  dom  h
2322cdm 4689 . . . . . . 7  class  dom  dom  h
24 cmap 6772 . . . . . . 7  class  ^m
2523, 5, 24co 5858 . . . . . 6  class  ( dom 
dom  h  ^m  x
)
2621, 13, 25wral 2543 . . . . 5  wff  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a
27 csem 20997 . . . . 5  class  SemiGrp
2826, 16, 27wral 2543 . . . 4  wff  A. h  e.  SemiGrp  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a
299, 28wa 358 . . 3  wff  ( g  =  (  subSemiGrpGen  `  <. g ,  x >. )  /\  A. h  e.  SemiGrp  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a )
3029, 2, 4copab 4076 . 2  class  { <. g ,  x >.  |  ( g  =  (  subSemiGrpGen  `  <. g ,  x >. )  /\  A. h  e.  SemiGrp  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a ) }
311, 30wceq 1623 1  wff  FreeSemiGrp  =  { <. g ,  x >.  |  (
g  =  (  subSemiGrpGen  `  <. g ,  x >. )  /\  A. h  e.  SemiGrp  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator