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 ${⊢}\mathrm{freeMnd}=\left({i}\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩\right\}\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrmd ${class}\mathrm{freeMnd}$
1 vi ${setvar}{i}$
2 cvv ${class}\mathrm{V}$
3 cbs ${class}\mathrm{Base}$
4 cnx ${class}\mathrm{ndx}$
5 4 3 cfv ${class}{\mathrm{Base}}_{\mathrm{ndx}}$
6 1 cv ${setvar}{i}$
7 6 cword ${class}\mathrm{Word}{i}$
8 5 7 cop ${class}⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩$
9 cplusg ${class}{+}_{𝑔}$
10 4 9 cfv ${class}{+}_{\mathrm{ndx}}$
11 cconcat ${class}\mathrm{++}$
12 7 7 cxp ${class}\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)$
13 11 12 cres ${class}\left({\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}\right)$
14 10 13 cop ${class}⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩$
15 8 14 cpr ${class}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩\right\}$
16 1 2 15 cmpt ${class}\left({i}\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩\right\}\right)$
17 0 16 wceq ${wff}\mathrm{freeMnd}=\left({i}\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩\right\}\right)$