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 ∈ V ⟼ Base ndx Word i + ndx ++ ↾ Word i × Word i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrmd class freeMnd
1 vi setvar i
2 cvv class V
3 cbs class Base
4 cnx class ndx
5 4 3 cfv class Base ndx
6 1 cv setvar i
7 6 cword class Word i
8 5 7 cop class Base ndx Word i
9 cplusg class + 𝑔
10 4 9 cfv class + ndx
11 cconcat class ++
12 7 7 cxp class Word i × Word i
13 11 12 cres class ++ ↾ Word i × Word i
14 10 13 cop class + ndx ++ ↾ Word i × Word i
15 8 14 cpr class Base ndx Word i + ndx ++ ↾ Word i × Word i
16 1 2 15 cmpt class i ∈ V ⟼ Base ndx Word i + ndx ++ ↾ Word i × Word i
17 0 16 wceq wff freeMnd = i ∈ V ⟼ Base ndx Word i + ndx ++ ↾ Word i × Word i