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

Definition df-frmd 15518
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 15516 . 2  class freeMnd
2 vi . . 3  setvar  i
3 cvv 2967 . . 3  class  _V
4 cnx 14163 . . . . . 6  class  ndx
5 cbs 14166 . . . . . 6  class  Base
64, 5cfv 5413 . . . . 5  class  ( Base `  ndx )
72cv 1368 . . . . . 6  class  i
87cword 12213 . . . . 5  class Word  i
96, 8cop 3878 . . . 4  class  <. ( Base `  ndx ) , Word  i >.
10 cplusg 14230 . . . . . 6  class  +g
114, 10cfv 5413 . . . . 5  class  ( +g  ` 
ndx )
12 cconcat 12215 . . . . . 6  class concat
138, 8cxp 4833 . . . . . 6  class  (Word  i  X. Word  i )
1412, 13cres 4837 . . . . 5  class  ( concat  |`  (Word  i  X. Word  i ) )
1511, 14cop 3878 . . . 4  class  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >.
169, 15cpr 3874 . . 3  class  { <. (
Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >. }
172, 3, 16cmpt 4345 . 2  class  ( i  e.  _V  |->  { <. (
Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word 
i ) ) >. } )
181, 17wceq 1369 1  wff freeMnd  =  ( i  e.  _V  |->  {
<. ( Base `  ndx ) , Word  i >. ,  <. ( +g  `  ndx ) ,  ( concat  |`  (Word  i  X. Word  i ) ) >. } )
Colors of variables: wff setvar class
This definition is referenced by:  frmdval  15520
  Copyright terms: Public domain W3C validator