# Metamath Proof Explorer

## Theorem frmdmnd

Description: A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypothesis frmdmnd.m ${⊢}{M}=\mathrm{freeMnd}\left({I}\right)$
Assertion frmdmnd ${⊢}{I}\in {V}\to {M}\in \mathrm{Mnd}$

### Proof

Step Hyp Ref Expression
1 frmdmnd.m ${⊢}{M}=\mathrm{freeMnd}\left({I}\right)$
2 eqidd ${⊢}{I}\in {V}\to {\mathrm{Base}}_{{M}}={\mathrm{Base}}_{{M}}$
3 eqidd ${⊢}{I}\in {V}\to {+}_{{M}}={+}_{{M}}$
4 eqid ${⊢}{\mathrm{Base}}_{{M}}={\mathrm{Base}}_{{M}}$
5 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
6 1 4 5 frmdadd ${⊢}\left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}{y}={x}\mathrm{++}{y}$
7 1 4 frmdelbas ${⊢}{x}\in {\mathrm{Base}}_{{M}}\to {x}\in \mathrm{Word}{I}$
8 1 4 frmdelbas ${⊢}{y}\in {\mathrm{Base}}_{{M}}\to {y}\in \mathrm{Word}{I}$
9 ccatcl ${⊢}\left({x}\in \mathrm{Word}{I}\wedge {y}\in \mathrm{Word}{I}\right)\to {x}\mathrm{++}{y}\in \mathrm{Word}{I}$
10 7 8 9 syl2an ${⊢}\left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {x}\mathrm{++}{y}\in \mathrm{Word}{I}$
11 6 10 eqeltrd ${⊢}\left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}{y}\in \mathrm{Word}{I}$
12 11 3adant1 ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}{y}\in \mathrm{Word}{I}$
13 1 4 frmdbas ${⊢}{I}\in {V}\to {\mathrm{Base}}_{{M}}=\mathrm{Word}{I}$
14 13 3ad2ant1 ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {\mathrm{Base}}_{{M}}=\mathrm{Word}{I}$
15 12 14 eleqtrrd ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}{y}\in {\mathrm{Base}}_{{M}}$
16 simpr1 ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}\in {\mathrm{Base}}_{{M}}$
17 16 7 syl ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}\in \mathrm{Word}{I}$
18 simpr2 ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {y}\in {\mathrm{Base}}_{{M}}$
19 18 8 syl ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {y}\in \mathrm{Word}{I}$
20 simpr3 ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {z}\in {\mathrm{Base}}_{{M}}$
21 1 4 frmdelbas ${⊢}{z}\in {\mathrm{Base}}_{{M}}\to {z}\in \mathrm{Word}{I}$
22 20 21 syl ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {z}\in \mathrm{Word}{I}$
23 ccatass ${⊢}\left({x}\in \mathrm{Word}{I}\wedge {y}\in \mathrm{Word}{I}\wedge {z}\in \mathrm{Word}{I}\right)\to \left({x}\mathrm{++}{y}\right)\mathrm{++}{z}={x}\mathrm{++}\left({y}\mathrm{++}{z}\right)$
24 17 19 22 23 syl3anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to \left({x}\mathrm{++}{y}\right)\mathrm{++}{z}={x}\mathrm{++}\left({y}\mathrm{++}{z}\right)$
25 16 18 10 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}\mathrm{++}{y}\in \mathrm{Word}{I}$
26 13 adantr ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {\mathrm{Base}}_{{M}}=\mathrm{Word}{I}$
27 25 26 eleqtrrd ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}\mathrm{++}{y}\in {\mathrm{Base}}_{{M}}$
28 1 4 5 frmdadd ${⊢}\left({x}\mathrm{++}{y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\to \left({x}\mathrm{++}{y}\right){+}_{{M}}{z}=\left({x}\mathrm{++}{y}\right)\mathrm{++}{z}$
29 27 20 28 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to \left({x}\mathrm{++}{y}\right){+}_{{M}}{z}=\left({x}\mathrm{++}{y}\right)\mathrm{++}{z}$
30 ccatcl ${⊢}\left({y}\in \mathrm{Word}{I}\wedge {z}\in \mathrm{Word}{I}\right)\to {y}\mathrm{++}{z}\in \mathrm{Word}{I}$
31 19 22 30 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {y}\mathrm{++}{z}\in \mathrm{Word}{I}$
32 31 26 eleqtrrd ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {y}\mathrm{++}{z}\in {\mathrm{Base}}_{{M}}$
33 1 4 5 frmdadd ${⊢}\left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\mathrm{++}{z}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}\left({y}\mathrm{++}{z}\right)={x}\mathrm{++}\left({y}\mathrm{++}{z}\right)$
34 16 32 33 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}{+}_{{M}}\left({y}\mathrm{++}{z}\right)={x}\mathrm{++}\left({y}\mathrm{++}{z}\right)$
35 24 29 34 3eqtr4d ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to \left({x}\mathrm{++}{y}\right){+}_{{M}}{z}={x}{+}_{{M}}\left({y}\mathrm{++}{z}\right)$
36 16 18 6 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}{+}_{{M}}{y}={x}\mathrm{++}{y}$
37 36 oveq1d ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to \left({x}{+}_{{M}}{y}\right){+}_{{M}}{z}=\left({x}\mathrm{++}{y}\right){+}_{{M}}{z}$
38 1 4 5 frmdadd ${⊢}\left({y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\to {y}{+}_{{M}}{z}={y}\mathrm{++}{z}$
39 18 20 38 syl2anc ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {y}{+}_{{M}}{z}={y}\mathrm{++}{z}$
40 39 oveq2d ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to {x}{+}_{{M}}\left({y}{+}_{{M}}{z}\right)={x}{+}_{{M}}\left({y}\mathrm{++}{z}\right)$
41 35 37 40 3eqtr4d ${⊢}\left({I}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{M}}\wedge {y}\in {\mathrm{Base}}_{{M}}\wedge {z}\in {\mathrm{Base}}_{{M}}\right)\right)\to \left({x}{+}_{{M}}{y}\right){+}_{{M}}{z}={x}{+}_{{M}}\left({y}{+}_{{M}}{z}\right)$
42 wrd0 ${⊢}\varnothing \in \mathrm{Word}{I}$
43 42 13 eleqtrrid ${⊢}{I}\in {V}\to \varnothing \in {\mathrm{Base}}_{{M}}$
44 1 4 5 frmdadd ${⊢}\left(\varnothing \in {\mathrm{Base}}_{{M}}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to \varnothing {+}_{{M}}{x}=\varnothing \mathrm{++}{x}$
45 43 44 sylan ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to \varnothing {+}_{{M}}{x}=\varnothing \mathrm{++}{x}$
46 7 adantl ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to {x}\in \mathrm{Word}{I}$
47 ccatlid ${⊢}{x}\in \mathrm{Word}{I}\to \varnothing \mathrm{++}{x}={x}$
48 46 47 syl ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to \varnothing \mathrm{++}{x}={x}$
49 45 48 eqtrd ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to \varnothing {+}_{{M}}{x}={x}$
50 1 4 5 frmdadd ${⊢}\left({x}\in {\mathrm{Base}}_{{M}}\wedge \varnothing \in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}\varnothing ={x}\mathrm{++}\varnothing$
51 50 ancoms ${⊢}\left(\varnothing \in {\mathrm{Base}}_{{M}}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}\varnothing ={x}\mathrm{++}\varnothing$
52 43 51 sylan ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}\varnothing ={x}\mathrm{++}\varnothing$
53 ccatrid ${⊢}{x}\in \mathrm{Word}{I}\to {x}\mathrm{++}\varnothing ={x}$
54 46 53 syl ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to {x}\mathrm{++}\varnothing ={x}$
55 52 54 eqtrd ${⊢}\left({I}\in {V}\wedge {x}\in {\mathrm{Base}}_{{M}}\right)\to {x}{+}_{{M}}\varnothing ={x}$
56 2 3 15 41 43 49 55 ismndd ${⊢}{I}\in {V}\to {M}\in \mathrm{Mnd}$