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 )