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 17318
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 17316 . 2 class freeMnd
2 vi . . 3 setvar 𝑖
3 cvv 3189 . . 3 class V
4 cnx 15789 . . . . . 6 class ndx
5 cbs 15792 . . . . . 6 class Base
64, 5cfv 5852 . . . . 5 class (Base‘ndx)
72cv 1479 . . . . . 6 class 𝑖
87cword 13238 . . . . 5 class Word 𝑖
96, 8cop 4159 . . . 4 class ⟨(Base‘ndx), Word 𝑖
10 cplusg 15873 . . . . . 6 class +g
114, 10cfv 5852 . . . . 5 class (+g‘ndx)
12 cconcat 13240 . . . . . 6 class ++
138, 8cxp 5077 . . . . . 6 class (Word 𝑖 × Word 𝑖)
1412, 13cres 5081 . . . . 5 class ( ++ ↾ (Word 𝑖 × Word 𝑖))
1511, 14cop 4159 . . . 4 class ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩
169, 15cpr 4155 . . 3 class {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩}
172, 3, 16cmpt 4678 . 2 class (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
181, 17wceq 1480 1 wff freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  frmdval  17320
  Copyright terms: Public domain W3C validator