This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 freeMnd = ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrmd ⊢ freeMnd
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 cbs ⊢ Base
4 cnx ⊢ ndx
5 4 3 cfv ⊢ ( Base ‘ ndx )
6 1 cv ⊢ 𝑖
7 6 cword ⊢ Word 𝑖
8 5 7 cop ⊢ ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩
9 cplusg ⊢ +g
10 4 9 cfv ⊢ ( +g ‘ ndx )
11 cconcat ⊢ ++
12 7 7 cxp ⊢ ( Word 𝑖 × Word 𝑖 )
13 11 12 cres ⊢ ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) )
14 10 13 cop ⊢ ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩
15 8 14 cpr ⊢ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ }
16 1 2 15 cmpt ⊢ ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )
17 0 16 wceq ⊢ freeMnd = ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )