Metamath Proof Explorer

Theorem frmd0

Description: The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypothesis frmdmnd.m 
|- M = ( freeMnd ` I )
Assertion frmd0 
|- (/) = ( 0g ` M )

Proof

Step Hyp Ref Expression
1 frmdmnd.m 
 |-  M = ( freeMnd ` I )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
4 eqid 
 |-  ( +g ` M ) = ( +g ` M )
5 wrd0 
 |-  (/) e. Word I
6 1 2 frmdbas 
 |-  ( I e. _V -> ( Base ` M ) = Word I )
7 5 6 eleqtrrid 
 |-  ( I e. _V -> (/) e. ( Base ` M ) )
8 1 2 4 frmdadd 
 |-  ( ( (/) e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( (/) ( +g ` M ) x ) = ( (/) ++ x ) )
9 7 8 sylan 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( (/) ( +g ` M ) x ) = ( (/) ++ x ) )
10 1 2 frmdelbas 
 |-  ( x e. ( Base ` M ) -> x e. Word I )
11 10 adantl 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> x e. Word I )
12 ccatlid 
 |-  ( x e. Word I -> ( (/) ++ x ) = x )
13 11 12 syl 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( (/) ++ x ) = x )
14 9 13 eqtrd 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( (/) ( +g ` M ) x ) = x )
15 1 2 4 frmdadd 
 |-  ( ( x e. ( Base ` M ) /\ (/) e. ( Base ` M ) ) -> ( x ( +g ` M ) (/) ) = ( x ++ (/) ) )
16 15 ancoms 
 |-  ( ( (/) e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( x ( +g ` M ) (/) ) = ( x ++ (/) ) )
17 7 16 sylan 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( x ( +g ` M ) (/) ) = ( x ++ (/) ) )
18 ccatrid 
 |-  ( x e. Word I -> ( x ++ (/) ) = x )
19 11 18 syl 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( x ++ (/) ) = x )
20 17 19 eqtrd 
 |-  ( ( I e. _V /\ x e. ( Base ` M ) ) -> ( x ( +g ` M ) (/) ) = x )
21 2 3 4 7 14 20 ismgmid2 
 |-  ( I e. _V -> (/) = ( 0g ` M ) )
22 0g0 
 |-  (/) = ( 0g ` (/) )
23 fvprc 
 |-  ( -. I e. _V -> ( freeMnd ` I ) = (/) )
24 1 23 eqtrid 
 |-  ( -. I e. _V -> M = (/) )
25 24 fveq2d 
 |-  ( -. I e. _V -> ( 0g ` M ) = ( 0g ` (/) ) )
26 22 25 eqtr4id 
 |-  ( -. I e. _V -> (/) = ( 0g ` M ) )
27 21 26 pm2.61i 
 |-  (/) = ( 0g ` M )