Metamath Proof Explorer

Theorem frgpcpbl

Description: Compatibility of the group operation with the free group equivalence relation. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frgpval.m 
|- G = ( freeGrp ` I )
frgpval.b 
|- M = ( freeMnd ` ( I X. 2o ) )
frgpval.r 
|- .~ = ( ~FG ` I )
frgpcpbl.p 
|- .+ = ( +g ` M )
Assertion frgpcpbl 
|- ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) )

Proof

Step Hyp Ref Expression
1 frgpval.m 
 |-  G = ( freeGrp ` I )
2 frgpval.b 
 |-  M = ( freeMnd ` ( I X. 2o ) )
3 frgpval.r 
 |-  .~ = ( ~FG ` I )
4 frgpcpbl.p 
 |-  .+ = ( +g ` M )
5 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
6 eqid 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
7 eqid 
 |-  ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) = ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) )
8 eqid 
 |-  ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` x ) ) = ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` x ) )
9 eqid 
 |-  ( m e. { t e. ( Word ( _I ` Word ( I X. 2o ) ) \ { (/) } ) | ( ( t ` 0 ) e. ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` x ) ) /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) ) = ( m e. { t e. ( Word ( _I ` Word ( I X. 2o ) ) \ { (/) } ) | ( ( t ` 0 ) e. ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` x ) ) /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
10 5 3 6 7 8 9 efgcpbl2 
 |-  ( ( A .~ C /\ B .~ D ) -> ( A ++ B ) .~ ( C ++ D ) )
11 5 3 efger 
 |-  .~ Er ( _I ` Word ( I X. 2o ) )
12 11 a1i 
 |-  ( ( A .~ C /\ B .~ D ) -> .~ Er ( _I ` Word ( I X. 2o ) ) )
13 simpl 
 |-  ( ( A .~ C /\ B .~ D ) -> A .~ C )
14 12 13 ercl 
 |-  ( ( A .~ C /\ B .~ D ) -> A e. ( _I ` Word ( I X. 2o ) ) )
15 5 efgrcl 
 |-  ( A e. ( _I ` Word ( I X. 2o ) ) -> ( I e. _V /\ ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) ) )
16 14 15 syl 
 |-  ( ( A .~ C /\ B .~ D ) -> ( I e. _V /\ ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) ) )
17 16 simprd 
 |-  ( ( A .~ C /\ B .~ D ) -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
18 16 simpld 
 |-  ( ( A .~ C /\ B .~ D ) -> I e. _V )
19 2on 
 |-  2o e. On
20 xpexg 
 |-  ( ( I e. _V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
21 18 19 20 sylancl 
 |-  ( ( A .~ C /\ B .~ D ) -> ( I X. 2o ) e. _V )
22 eqid 
 |-  ( Base ` M ) = ( Base ` M )
23 2 22 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` M ) = Word ( I X. 2o ) )
24 21 23 syl 
 |-  ( ( A .~ C /\ B .~ D ) -> ( Base ` M ) = Word ( I X. 2o ) )
25 17 24 eqtr4d 
 |-  ( ( A .~ C /\ B .~ D ) -> ( _I ` Word ( I X. 2o ) ) = ( Base ` M ) )
26 14 25 eleqtrd 
 |-  ( ( A .~ C /\ B .~ D ) -> A e. ( Base ` M ) )
27 simpr 
 |-  ( ( A .~ C /\ B .~ D ) -> B .~ D )
28 12 27 ercl 
 |-  ( ( A .~ C /\ B .~ D ) -> B e. ( _I ` Word ( I X. 2o ) ) )
29 28 25 eleqtrd 
 |-  ( ( A .~ C /\ B .~ D ) -> B e. ( Base ` M ) )
30 2 22 4 frmdadd 
 |-  ( ( A e. ( Base ` M ) /\ B e. ( Base ` M ) ) -> ( A .+ B ) = ( A ++ B ) )
31 26 29 30 syl2anc 
 |-  ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) = ( A ++ B ) )
32 12 13 ercl2 
 |-  ( ( A .~ C /\ B .~ D ) -> C e. ( _I ` Word ( I X. 2o ) ) )
33 32 25 eleqtrd 
 |-  ( ( A .~ C /\ B .~ D ) -> C e. ( Base ` M ) )
34 12 27 ercl2 
 |-  ( ( A .~ C /\ B .~ D ) -> D e. ( _I ` Word ( I X. 2o ) ) )
35 34 25 eleqtrd 
 |-  ( ( A .~ C /\ B .~ D ) -> D e. ( Base ` M ) )
36 2 22 4 frmdadd 
 |-  ( ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) -> ( C .+ D ) = ( C ++ D ) )
37 33 35 36 syl2anc 
 |-  ( ( A .~ C /\ B .~ D ) -> ( C .+ D ) = ( C ++ D ) )
38 10 31 37 3brtr4d 
 |-  ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) )