Metamath Proof Explorer

Theorem frmdplusg

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

Ref Expression
Hypotheses frmdbas.m 
|- M = ( freeMnd ` I )
frmdbas.b 
|- B = ( Base ` M )
frmdplusg.p 
|- .+ = ( +g ` M )
Assertion frmdplusg 
|- .+ = ( ++ |` ( B X. B ) )

Proof

Step Hyp Ref Expression
1 frmdbas.m 
 |-  M = ( freeMnd ` I )
2 frmdbas.b 
 |-  B = ( Base ` M )
3 frmdplusg.p 
 |-  .+ = ( +g ` M )
4 1 2 frmdbas 
 |-  ( I e. _V -> B = Word I )
5 eqid 
 |-  ( ++ |` ( B X. B ) ) = ( ++ |` ( B X. B ) )
6 1 4 5 frmdval 
 |-  ( I e. _V -> M = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } )
7 6 fveq2d 
 |-  ( I e. _V -> ( +g ` M ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } ) )
8 3 7 syl5eq 
 |-  ( I e. _V -> .+ = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } ) )
9 wrdexg 
 |-  ( I e. _V -> Word I e. _V )
10 ccatfn 
 |-  ++ Fn ( _V X. _V )
11 xpss 
 |-  ( B X. B ) C_ ( _V X. _V )
12 fnssres 
 |-  ( ( ++ Fn ( _V X. _V ) /\ ( B X. B ) C_ ( _V X. _V ) ) -> ( ++ |` ( B X. B ) ) Fn ( B X. B ) )
13 10 11 12 mp2an 
 |-  ( ++ |` ( B X. B ) ) Fn ( B X. B )
14 ovres 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( ++ |` ( B X. B ) ) y ) = ( x ++ y ) )
15 1 2 frmdelbas 
 |-  ( x e. B -> x e. Word I )
16 1 2 frmdelbas 
 |-  ( y e. B -> y e. Word I )
17 ccatcl 
 |-  ( ( x e. Word I /\ y e. Word I ) -> ( x ++ y ) e. Word I )
18 15 16 17 syl2an 
 |-  ( ( x e. B /\ y e. B ) -> ( x ++ y ) e. Word I )
19 14 18 eqeltrd 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( ++ |` ( B X. B ) ) y ) e. Word I )
20 19 rgen2 
 |-  A. x e. B A. y e. B ( x ( ++ |` ( B X. B ) ) y ) e. Word I
21 ffnov 
 |-  ( ( ++ |` ( B X. B ) ) : ( B X. B ) --> Word I <-> ( ( ++ |` ( B X. B ) ) Fn ( B X. B ) /\ A. x e. B A. y e. B ( x ( ++ |` ( B X. B ) ) y ) e. Word I ) )
22 13 20 21 mpbir2an 
 |-  ( ++ |` ( B X. B ) ) : ( B X. B ) --> Word I
23 2 fvexi 
 |-  B e. _V
24 23 23 xpex 
 |-  ( B X. B ) e. _V
25 fex2 
 |-  ( ( ( ++ |` ( B X. B ) ) : ( B X. B ) --> Word I /\ ( B X. B ) e. _V /\ Word I e. _V ) -> ( ++ |` ( B X. B ) ) e. _V )
26 22 24 25 mp3an12 
 |-  ( Word I e. _V -> ( ++ |` ( B X. B ) ) e. _V )
27 eqid 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. }
28 27 grpplusg 
 |-  ( ( ++ |` ( B X. B ) ) e. _V -> ( ++ |` ( B X. B ) ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } ) )
29 9 26 28 3syl 
 |-  ( I e. _V -> ( ++ |` ( B X. B ) ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( ++ |` ( B X. B ) ) >. } ) )
30 8 29 eqtr4d 
 |-  ( I e. _V -> .+ = ( ++ |` ( B X. B ) ) )
31 fvprc 
 |-  ( -. I e. _V -> ( freeMnd ` I ) = (/) )
32 1 31 syl5eq 
 |-  ( -. I e. _V -> M = (/) )
33 32 fveq2d 
 |-  ( -. I e. _V -> ( +g ` M ) = ( +g ` (/) ) )
34 3 33 syl5eq 
 |-  ( -. I e. _V -> .+ = ( +g ` (/) ) )
35 res0 
 |-  ( ++ |` (/) ) = (/)
36 df-plusg 
 |-  +g = Slot 2
37 36 str0 
 |-  (/) = ( +g ` (/) )
38 35 37 eqtr2i 
 |-  ( +g ` (/) ) = ( ++ |` (/) )
39 34 38 eqtrdi 
 |-  ( -. I e. _V -> .+ = ( ++ |` (/) ) )
40 32 fveq2d 
 |-  ( -. I e. _V -> ( Base ` M ) = ( Base ` (/) ) )
41 base0 
 |-  (/) = ( Base ` (/) )
42 40 2 41 3eqtr4g 
 |-  ( -. I e. _V -> B = (/) )
43 42 xpeq2d 
 |-  ( -. I e. _V -> ( B X. B ) = ( B X. (/) ) )
44 xp0 
 |-  ( B X. (/) ) = (/)
45 43 44 eqtrdi 
 |-  ( -. I e. _V -> ( B X. B ) = (/) )
46 45 reseq2d 
 |-  ( -. I e. _V -> ( ++ |` ( B X. B ) ) = ( ++ |` (/) ) )
47 39 46 eqtr4d 
 |-  ( -. I e. _V -> .+ = ( ++ |` ( B X. B ) ) )
48 30 47 pm2.61i 
 |-  .+ = ( ++ |` ( B X. B ) )