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 17992
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 17990 . 2 class freeMnd
2 vi . . 3 setvar 𝑖
3 cvv 3471 . . 3 class V
4 cnx 16458 . . . . . 6 class ndx
5 cbs 16461 . . . . . 6 class Base
64, 5cfv 6328 . . . . 5 class (Base‘ndx)
72cv 1537 . . . . . 6 class 𝑖
87cword 13845 . . . . 5 class Word 𝑖
96, 8cop 4546 . . . 4 class ⟨(Base‘ndx), Word 𝑖
10 cplusg 16543 . . . . . 6 class +g
114, 10cfv 6328 . . . . 5 class (+g‘ndx)
12 cconcat 13901 . . . . . 6 class ++
138, 8cxp 5526 . . . . . 6 class (Word 𝑖 × Word 𝑖)
1412, 13cres 5530 . . . . 5 class ( ++ ↾ (Word 𝑖 × Word 𝑖))
1511, 14cop 4546 . . . 4 class ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩
169, 15cpr 4542 . . 3 class {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩}
172, 3, 16cmpt 5119 . 2 class (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
181, 17wceq 1538 1 wff freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  frmdval  17994
  Copyright terms: Public domain W3C validator