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

Definition df-frmd 17558
Description: Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
Assertion
Ref Expression
df-frmd freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})

Detailed syntax breakdown of Definition df-frmd
StepHypRef Expression
1 cfrmd 17556 . 2 class freeMnd
2 vi . . 3 setvar 𝑖
3 cvv 3328 . . 3 class V
4 cnx 16027 . . . . . 6 class ndx
5 cbs 16030 . . . . . 6 class Base
64, 5cfv 6037 . . . . 5 class (Base‘ndx)
72cv 1619 . . . . . 6 class 𝑖
87cword 13448 . . . . 5 class Word 𝑖
96, 8cop 4315 . . . 4 class ⟨(Base‘ndx), Word 𝑖
10 cplusg 16114 . . . . . 6 class +g
114, 10cfv 6037 . . . . 5 class (+g‘ndx)
12 cconcat 13450 . . . . . 6 class ++
138, 8cxp 5252 . . . . . 6 class (Word 𝑖 × Word 𝑖)
1412, 13cres 5256 . . . . 5 class ( ++ ↾ (Word 𝑖 × Word 𝑖))
1511, 14cop 4315 . . . 4 class ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩
169, 15cpr 4311 . . 3 class {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩}
172, 3, 16cmpt 4869 . 2 class (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
181, 17wceq 1620 1 wff freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  frmdval  17560
  Copyright terms: Public domain W3C validator