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 = ( freeMnd ` I )
Assertion frmdmnd 
|- ( I e. V -> M e. Mnd )

Proof

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