This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-frmd

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)

Ref Expression
Assertion df-frmd 
|- freeMnd = ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrmd 
 |-  freeMnd
1 vi 
 |-  i
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 cnx 
 |-  ndx
5 4 3 cfv 
 |-  ( Base ` ndx )
6 1 cv 
 |-  i
7 6 cword 
 |-  Word i
8 5 7 cop 
 |-  <. ( Base ` ndx ) , Word i >.
9 cplusg 
 |-  +g
10 4 9 cfv 
 |-  ( +g ` ndx )
11 cconcat 
 |-  ++
12 7 7 cxp 
 |-  ( Word i X. Word i )
13 11 12 cres 
 |-  ( ++ |` ( Word i X. Word i ) )
14 10 13 cop 
 |-  <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >.
15 8 14 cpr 
 |-  { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. }
16 1 2 15 cmpt 
 |-  ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )
17 0 16 wceq 
 |-  freeMnd = ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )