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 + ˙ = + M
Assertion frmdplusg + ˙ = ++ B × B

Proof

Step Hyp Ref Expression
1 frmdbas.m M = freeMnd I
2 frmdbas.b B = Base M
3 frmdplusg.p + ˙ = + M
4 1 2 frmdbas I V B = Word I
5 eqid ++ B × B = ++ B × B
6 1 4 5 frmdval I V M = Base ndx B + ndx ++ B × B
7 6 fveq2d I V + M = + Base ndx B + ndx ++ B × B
8 3 7 eqtrid I V + ˙ = + Base ndx B + ndx ++ B × B
9 wrdexg I V Word I V
10 ccatfn ++ Fn V × V
11 xpss B × B V × V
12 fnssres ++ Fn V × V B × B V × V ++ B × B Fn B × B
13 10 11 12 mp2an ++ B × B Fn B × B
14 ovres x B y B x ++ B × B y = x ++ y
15 1 2 frmdelbas x B x Word I
16 1 2 frmdelbas y B y Word I
17 ccatcl x Word I y Word I x ++ y Word I
18 15 16 17 syl2an x B y B x ++ y Word I
19 14 18 eqeltrd x B y B x ++ B × B y Word I
20 19 rgen2 x B y B x ++ B × B y Word I
21 ffnov ++ B × B : B × B Word I ++ B × B Fn B × B x B y B x ++ B × B y Word I
22 13 20 21 mpbir2an ++ B × B : B × B Word I
23 2 fvexi B V
24 23 23 xpex B × B V
25 fex2 ++ B × B : B × B Word I B × B V Word I V ++ B × B V
26 22 24 25 mp3an12 Word I V ++ B × B V
27 eqid Base ndx B + ndx ++ B × B = Base ndx B + ndx ++ B × B
28 27 grpplusg ++ B × B V ++ B × B = + Base ndx B + ndx ++ B × B
29 9 26 28 3syl I V ++ B × B = + Base ndx B + ndx ++ B × B
30 8 29 eqtr4d I V + ˙ = ++ B × B
31 fvprc ¬ I V freeMnd I =
32 1 31 eqtrid ¬ I V M =
33 32 fveq2d ¬ I V + M = +
34 3 33 eqtrid ¬ I V + ˙ = +
35 res0 ++ =
36 plusgid + 𝑔 = Slot + ndx
37 36 str0 = +
38 35 37 eqtr2i + = ++
39 34 38 eqtrdi ¬ I V + ˙ = ++
40 32 fveq2d ¬ I V Base M = Base
41 base0 = Base
42 40 2 41 3eqtr4g ¬ I V B =
43 42 xpeq2d ¬ I V B × B = B ×
44 xp0 B × =
45 43 44 eqtrdi ¬ I V B × B =
46 45 reseq2d ¬ I V ++ B × B = ++
47 39 46 eqtr4d ¬ I V + ˙ = ++ B × B
48 30 47 pm2.61i + ˙ = ++ B × B