Metamath Proof Explorer

Theorem frgpadd

Description: Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgpadd.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpadd.g 
|- G = ( freeGrp ` I )
frgpadd.r 
|- .~ = ( ~FG ` I )
frgpadd.n 
|- .+ = ( +g ` G )
Assertion frgpadd 
|- ( ( A e. W /\ B e. W ) -> ( [ A ] .~ .+ [ B ] .~ ) = [ ( A ++ B ) ] .~ )

Proof

Step Hyp Ref Expression
1 frgpadd.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 frgpadd.g 
 |-  G = ( freeGrp ` I )
3 frgpadd.r 
 |-  .~ = ( ~FG ` I )
4 frgpadd.n 
 |-  .+ = ( +g ` G )
5 simpl 
 |-  ( ( A e. W /\ B e. W ) -> A e. W )
6 simpr 
 |-  ( ( A e. W /\ B e. W ) -> B e. W )
7 1 efgrcl 
 |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
8 7 adantr 
 |-  ( ( A e. W /\ B e. W ) -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
9 8 simpld 
 |-  ( ( A e. W /\ B e. W ) -> I e. _V )
10 eqid 
 |-  ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
11 2 10 3 frgpval 
 |-  ( I e. _V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
12 9 11 syl 
 |-  ( ( A e. W /\ B e. W ) -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
13 8 simprd 
 |-  ( ( A e. W /\ B e. W ) -> W = Word ( I X. 2o ) )
14 2on 
 |-  2o e. On
15 xpexg 
 |-  ( ( I e. _V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
16 9 14 15 sylancl 
 |-  ( ( A e. W /\ B e. W ) -> ( I X. 2o ) e. _V )
17 eqid 
 |-  ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) )
18 10 17 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
19 16 18 syl 
 |-  ( ( A e. W /\ B e. W ) -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
20 13 19 eqtr4d 
 |-  ( ( A e. W /\ B e. W ) -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
21 1 3 efger 
 |-  .~ Er W
22 21 a1i 
 |-  ( ( A e. W /\ B e. W ) -> .~ Er W )
23 10 frmdmnd 
 |-  ( ( I X. 2o ) e. _V -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
24 16 23 syl 
 |-  ( ( A e. W /\ B e. W ) -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
25 eqid 
 |-  ( +g ` ( freeMnd ` ( I X. 2o ) ) ) = ( +g ` ( freeMnd ` ( I X. 2o ) ) )
26 2 10 3 25 frgpcpbl 
 |-  ( ( a .~ b /\ c .~ d ) -> ( a ( +g ` ( freeMnd ` ( I X. 2o ) ) ) c ) .~ ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) )
27 26 a1i 
 |-  ( ( A e. W /\ B e. W ) -> ( ( a .~ b /\ c .~ d ) -> ( a ( +g ` ( freeMnd ` ( I X. 2o ) ) ) c ) .~ ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) ) )
28 24 adantr 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
29 simprl 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> b e. W )
30 20 adantr 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
31 29 30 eleqtrd 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> b e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
32 simprr 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> d e. W )
33 32 30 eleqtrd 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> d e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
34 17 25 mndcl 
 |-  ( ( ( freeMnd ` ( I X. 2o ) ) e. Mnd /\ b e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ d e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
35 28 31 33 34 syl3anc 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
36 35 30 eleqtrrd 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( b e. W /\ d e. W ) ) -> ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) e. W )
37 12 20 22 24 27 36 25 4 qusaddval 
 |-  ( ( ( A e. W /\ B e. W ) /\ A e. W /\ B e. W ) -> ( [ A ] .~ .+ [ B ] .~ ) = [ ( A ( +g ` ( freeMnd ` ( I X. 2o ) ) ) B ) ] .~ )
38 5 6 37 mpd3an23 
 |-  ( ( A e. W /\ B e. W ) -> ( [ A ] .~ .+ [ B ] .~ ) = [ ( A ( +g ` ( freeMnd ` ( I X. 2o ) ) ) B ) ] .~ )
39 5 20 eleqtrd 
 |-  ( ( A e. W /\ B e. W ) -> A e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
40 6 20 eleqtrd 
 |-  ( ( A e. W /\ B e. W ) -> B e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
41 10 17 25 frmdadd 
 |-  ( ( A e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ B e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( A ( +g ` ( freeMnd ` ( I X. 2o ) ) ) B ) = ( A ++ B ) )
42 39 40 41 syl2anc 
 |-  ( ( A e. W /\ B e. W ) -> ( A ( +g ` ( freeMnd ` ( I X. 2o ) ) ) B ) = ( A ++ B ) )
43 42 eceq1d 
 |-  ( ( A e. W /\ B e. W ) -> [ ( A ( +g ` ( freeMnd ` ( I X. 2o ) ) ) B ) ] .~ = [ ( A ++ B ) ] .~ )
44 38 43 eqtrd 
 |-  ( ( A e. W /\ B e. W ) -> ( [ A ] .~ .+ [ B ] .~ ) = [ ( A ++ B ) ] .~ )