# Metamath Proof Explorer

## Theorem frmdval

Description: Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdval.m ${⊢}{M}=\mathrm{freeMnd}\left({I}\right)$
frmdval.b ${⊢}{I}\in {V}\to {B}=\mathrm{Word}{I}$
frmdval.p
Assertion frmdval

### Proof

Step Hyp Ref Expression
1 frmdval.m ${⊢}{M}=\mathrm{freeMnd}\left({I}\right)$
2 frmdval.b ${⊢}{I}\in {V}\to {B}=\mathrm{Word}{I}$
3 frmdval.p
4 df-frmd ${⊢}\mathrm{freeMnd}=\left({i}\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}⟩\right\}\right)$
5 wrdeq ${⊢}{i}={I}\to \mathrm{Word}{i}=\mathrm{Word}{I}$
6 2 eqcomd ${⊢}{I}\in {V}\to \mathrm{Word}{I}={B}$
7 5 6 sylan9eqr ${⊢}\left({I}\in {V}\wedge {i}={I}\right)\to \mathrm{Word}{i}={B}$
8 7 opeq2d ${⊢}\left({I}\in {V}\wedge {i}={I}\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}{i}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩$
9 7 sqxpeqd ${⊢}\left({I}\in {V}\wedge {i}={I}\right)\to \mathrm{Word}{i}×\mathrm{Word}{i}={B}×{B}$
10 9 reseq2d ${⊢}\left({I}\in {V}\wedge {i}={I}\right)\to {\mathrm{++}↾}_{\left(\mathrm{Word}{i}×\mathrm{Word}{i}\right)}={\mathrm{++}↾}_{\left({B}×{B}\right)}$
11 10 3 eqtr4di
12 11 opeq2d
13 8 12 preq12d
14 elex ${⊢}{I}\in {V}\to {I}\in \mathrm{V}$
15 prex
16 15 a1i
17 4 13 14 16 fvmptd2
18 1 17 syl5eq