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) (Proof shortened by AV, 6-Nov-2024)

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 eqtrid
 |-  ( 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 eqtrid
 |-  ( -. I e. _V -> M = (/) )
33 32 fveq2d
 |-  ( -. I e. _V -> ( +g ` M ) = ( +g ` (/) ) )
34 3 33 eqtrid
 |-  ( -. I e. _V -> .+ = ( +g ` (/) ) )
35 res0
 |-  ( ++ |` (/) ) = (/)
36 plusgid
 |-  +g = Slot ( +g ` ndx )
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 ) )