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 25493
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 25492 . 2  class  FreeSemiGrp
2 vg . . . . . 6  set  g
32cv 1631 . . . . 5  class  g
4 vx . . . . . . . 8  set  x
54cv 1631 . . . . . . 7  class  x
63, 5cop 3656 . . . . . 6  class  <. g ,  x >.
7 csbsgrg 25488 . . . . . 6  class  subSemiGrpGen
86, 7cfv 5271 . . . . 5  class  (  subSemiGrpGen  `  <. g ,  x >. )
93, 8wceq 1632 . . . 4  wff  g  =  ( 
subSemiGrpGen  `  <. g ,  x >. )
10 vu . . . . . . . . . 10  set  u
1110cv 1631 . . . . . . . . 9  class  u
1211, 5cres 4707 . . . . . . . 8  class  ( u  |`  x )
13 va . . . . . . . . 9  set  a
1413cv 1631 . . . . . . . 8  class  a
1512, 14wceq 1632 . . . . . . 7  wff  ( u  |`  x )  =  a
16 vh . . . . . . . . . 10  set  h
1716cv 1631 . . . . . . . . 9  class  h
183, 17cop 3656 . . . . . . . 8  class  <. g ,  h >.
19 csmhom 25490 . . . . . . . 8  class  SemiGrpHom
2018, 19cfv 5271 . . . . . . 7  class  ( SemiGrpHom `  <. g ,  h >. )
2115, 10, 20wrex 2557 . . . . . 6  wff  E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a
2217cdm 4705 . . . . . . . 8  class  dom  h
2322cdm 4705 . . . . . . 7  class  dom  dom  h
24 cmap 6788 . . . . . . 7  class  ^m
2523, 5, 24co 5874 . . . . . 6  class  ( dom 
dom  h  ^m  x
)
2621, 13, 25wral 2556 . . . . 5  wff  A. a  e.  ( dom  dom  h  ^m  x ) E. u  e.  ( SemiGrpHom `  <. g ,  h >. ) ( u  |`  x )  =  a
27 csem 21013 . . . . 5  class  SemiGrp
2826, 16, 27wral 2556 . . . 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 4092 . 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 1632 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