# 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 𝑀 = ( freeMnd ‘ 𝐼 )
Assertion frmdmnd ( 𝐼𝑉𝑀 ∈ Mnd )

### Proof

Step Hyp Ref Expression
1 frmdmnd.m 𝑀 = ( freeMnd ‘ 𝐼 )
2 eqidd ( 𝐼𝑉 → ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) )
3 eqidd ( 𝐼𝑉 → ( +g𝑀 ) = ( +g𝑀 ) )
4 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 eqid ( +g𝑀 ) = ( +g𝑀 )
6 1 4 5 frmdadd ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
7 1 4 frmdelbas ( 𝑥 ∈ ( Base ‘ 𝑀 ) → 𝑥 ∈ Word 𝐼 )
8 1 4 frmdelbas ( 𝑦 ∈ ( Base ‘ 𝑀 ) → 𝑦 ∈ Word 𝐼 )
9 ccatcl ( ( 𝑥 ∈ Word 𝐼𝑦 ∈ Word 𝐼 ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐼 )
10 7 8 9 syl2an ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐼 )
11 6 10 eqeltrd ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ Word 𝐼 )
12 11 3adant1 ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ Word 𝐼 )
13 1 4 frmdbas ( 𝐼𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
14 13 3ad2ant1 ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
15 12 14 eleqtrrd ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
16 simpr1 ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
17 16 7 syl ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ Word 𝐼 )
18 simpr2 ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
19 18 8 syl ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ Word 𝐼 )
20 simpr3 ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑀 ) )
21 1 4 frmdelbas ( 𝑧 ∈ ( Base ‘ 𝑀 ) → 𝑧 ∈ Word 𝐼 )
22 20 21 syl ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑧 ∈ Word 𝐼 )
23 ccatass ( ( 𝑥 ∈ Word 𝐼𝑦 ∈ Word 𝐼𝑧 ∈ Word 𝐼 ) → ( ( 𝑥 ++ 𝑦 ) ++ 𝑧 ) = ( 𝑥 ++ ( 𝑦 ++ 𝑧 ) ) )
24 17 19 22 23 syl3anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ++ 𝑦 ) ++ 𝑧 ) = ( 𝑥 ++ ( 𝑦 ++ 𝑧 ) ) )
25 16 18 10 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐼 )
26 13 adantr ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
27 25 26 eleqtrrd ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ++ 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
28 1 4 5 frmdadd ( ( ( 𝑥 ++ 𝑦 ) ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ++ 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( ( 𝑥 ++ 𝑦 ) ++ 𝑧 ) )
29 27 20 28 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ++ 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( ( 𝑥 ++ 𝑦 ) ++ 𝑧 ) )
30 ccatcl ( ( 𝑦 ∈ Word 𝐼𝑧 ∈ Word 𝐼 ) → ( 𝑦 ++ 𝑧 ) ∈ Word 𝐼 )
31 19 22 30 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ++ 𝑧 ) ∈ Word 𝐼 )
32 31 26 eleqtrrd ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ++ 𝑧 ) ∈ ( Base ‘ 𝑀 ) )
33 1 4 5 frmdadd ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ( 𝑦 ++ 𝑧 ) ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) ( 𝑦 ++ 𝑧 ) ) = ( 𝑥 ++ ( 𝑦 ++ 𝑧 ) ) )
34 16 32 33 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g𝑀 ) ( 𝑦 ++ 𝑧 ) ) = ( 𝑥 ++ ( 𝑦 ++ 𝑧 ) ) )
35 24 29 34 3eqtr4d ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ++ 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ++ 𝑧 ) ) )
36 16 18 6 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
37 36 oveq1d ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( ( 𝑥 ++ 𝑦 ) ( +g𝑀 ) 𝑧 ) )
38 1 4 5 frmdadd ( ( 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( +g𝑀 ) 𝑧 ) = ( 𝑦 ++ 𝑧 ) )
39 18 20 38 syl2anc ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ( +g𝑀 ) 𝑧 ) = ( 𝑦 ++ 𝑧 ) )
40 39 oveq2d ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ++ 𝑧 ) ) )
41 35 37 40 3eqtr4d ( ( 𝐼𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( +g𝑀 ) 𝑧 ) = ( 𝑥 ( +g𝑀 ) ( 𝑦 ( +g𝑀 ) 𝑧 ) ) )
42 wrd0 ∅ ∈ Word 𝐼
43 42 13 eleqtrrid ( 𝐼𝑉 → ∅ ∈ ( Base ‘ 𝑀 ) )
44 1 4 5 frmdadd ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
45 43 44 sylan ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) )
46 7 adantl ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ Word 𝐼 )
47 ccatlid ( 𝑥 ∈ Word 𝐼 → ( ∅ ++ 𝑥 ) = 𝑥 )
48 46 47 syl ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ++ 𝑥 ) = 𝑥 )
49 45 48 eqtrd ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g𝑀 ) 𝑥 ) = 𝑥 )
50 1 4 5 frmdadd ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∅ ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
51 50 ancoms ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
52 43 51 sylan ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) )
53 ccatrid ( 𝑥 ∈ Word 𝐼 → ( 𝑥 ++ ∅ ) = 𝑥 )
54 46 53 syl ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ++ ∅ ) = 𝑥 )
55 52 54 eqtrd ( ( 𝐼𝑉𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g𝑀 ) ∅ ) = 𝑥 )
56 2 3 15 41 43 49 55 ismndd ( 𝐼𝑉𝑀 ∈ Mnd )