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

Definition df-frmd 14471
Description: Define a free monoid over a set  i of generators, defined as the set of finite strings on  I with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
Assertion
Ref Expression
df-frmd  |- freeMnd  =  ( i  e.  _V  |->  {
<. ( Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word  i ) ) >. } )

Detailed syntax breakdown of Definition df-frmd
StepHypRef Expression
1 cfrmd 14469 . 2  class freeMnd
2 vi . . 3  set  i
3 cvv 2788 . . 3  class  _V
4 cnx 13145 . . . . . 6  class  ndx
5 cbs 13148 . . . . . 6  class  Base
64, 5cfv 5255 . . . . 5  class  ( Base `  ndx )
72cv 1622 . . . . . 6  class  i
87cword 11403 . . . . 5  class Word  i
96, 8cop 3643 . . . 4  class  <. ( Base `  ndx ) , Word  i >.
10 cplusg 13208 . . . . . 6  class  +g
114, 10cfv 5255 . . . . 5  class  ( +g  ` 
ndx )
12 cconcat 11404 . . . . . 6  class concat
138, 8cxp 4687 . . . . . 6  class  (Word  i  X. Word  i )
1412, 13cres 4691 . . . . 5  class  ( concat  |`  (Word  i  X. Word  i ) )
1511, 14cop 3643 . . . 4  class  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >.
169, 15cpr 3641 . . 3  class  { <. (
Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >. }
172, 3, 16cmpt 4077 . 2  class  ( i  e.  _V  |->  { <. (
Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >. } )
181, 17wceq 1623 1  wff freeMnd  =  ( i  e.  _V  |->  {
<. ( Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word  i ) ) >. } )
Colors of variables: wff set class
This definition is referenced by:  frmdval  14473
  Copyright terms: Public domain W3C validator