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 18664
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 18662 . 2 class freeMnd
2 vi . . 3 setvar 𝑖
3 cvv 3444 . . 3 class V
4 cnx 17070 . . . . . 6 class ndx
5 cbs 17088 . . . . . 6 class Base
64, 5cfv 6497 . . . . 5 class (Baseβ€˜ndx)
72cv 1541 . . . . . 6 class 𝑖
87cword 14408 . . . . 5 class Word 𝑖
96, 8cop 4593 . . . 4 class ⟨(Baseβ€˜ndx), Word π‘–βŸ©
10 cplusg 17138 . . . . . 6 class +g
114, 10cfv 6497 . . . . 5 class (+gβ€˜ndx)
12 cconcat 14464 . . . . . 6 class ++
138, 8cxp 5632 . . . . . 6 class (Word 𝑖 Γ— Word 𝑖)
1412, 13cres 5636 . . . . 5 class ( ++ β†Ύ (Word 𝑖 Γ— Word 𝑖))
1511, 14cop 4593 . . . 4 class ⟨(+gβ€˜ndx), ( ++ β†Ύ (Word 𝑖 Γ— Word 𝑖))⟩
169, 15cpr 4589 . . 3 class {⟨(Baseβ€˜ndx), Word π‘–βŸ©, ⟨(+gβ€˜ndx), ( ++ β†Ύ (Word 𝑖 Γ— Word 𝑖))⟩}
172, 3, 16cmpt 5189 . 2 class (𝑖 ∈ V ↦ {⟨(Baseβ€˜ndx), Word π‘–βŸ©, ⟨(+gβ€˜ndx), ( ++ β†Ύ (Word 𝑖 Γ— Word 𝑖))⟩})
181, 17wceq 1542 1 wff freeMnd = (𝑖 ∈ V ↦ {⟨(Baseβ€˜ndx), Word π‘–βŸ©, ⟨(+gβ€˜ndx), ( ++ β†Ύ (Word 𝑖 Γ— Word 𝑖))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  frmdval  18666
  Copyright terms: Public domain W3C validator