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

Metamath Proof Explorer

Theorem frmdbas

Description: The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frmdbas.m ⊢ M = freeMnd ⁡ I
frmdbas.b ⊢ B = Base M
Assertion frmdbas ⊢ I ∈ V → B = Word I

Proof

Step Hyp Ref Expression
1 frmdbas.m ⊢ M = freeMnd ⁡ I
2 frmdbas.b ⊢ B = Base M
3 eqidd ⊢ I ∈ V → Word I = Word I
4 eqid ⊢ ++ ↾ Word I × Word I = ++ ↾ Word I × Word I
5 1 3 4 frmdval ⊢ I ∈ V → M = Base ndx Word I + ndx ++ ↾ Word I × Word I
6 5 fveq2d ⊢ I ∈ V → Base M = Base Base ndx Word I + ndx ++ ↾ Word I × Word I
7 wrdexg ⊢ I ∈ V → Word I ∈ V
8 eqid ⊢ Base ndx Word I + ndx ++ ↾ Word I × Word I = Base ndx Word I + ndx ++ ↾ Word I × Word I
9 8 grpbase ⊢ Word I ∈ V → Word I = Base Base ndx Word I + ndx ++ ↾ Word I × Word I
10 7 9 syl ⊢ I ∈ V → Word I = Base Base ndx Word I + ndx ++ ↾ Word I × Word I
11 6 10 eqtr4d ⊢ I ∈ V → Base M = Word I
12 2 11 eqtrid ⊢ I ∈ V → B = Word I