Metamath Proof Explorer

Theorem efgcpbl2

Description: Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
Assertion efgcpbl2 
|- ( ( A .~ X /\ B .~ Y ) -> ( A ++ B ) .~ ( X ++ Y ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 1 2 efger 
 |-  .~ Er W
8 7 a1i 
 |-  ( ( A .~ X /\ B .~ Y ) -> .~ Er W )
9 simpl 
 |-  ( ( A .~ X /\ B .~ Y ) -> A .~ X )
10 8 9 ercl 
 |-  ( ( A .~ X /\ B .~ Y ) -> A e. W )
11 wrd0 
 |-  (/) e. Word ( I X. 2o )
12 1 efgrcl 
 |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
13 10 12 syl 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
14 13 simprd 
 |-  ( ( A .~ X /\ B .~ Y ) -> W = Word ( I X. 2o ) )
15 11 14 eleqtrrid 
 |-  ( ( A .~ X /\ B .~ Y ) -> (/) e. W )
16 simpr 
 |-  ( ( A .~ X /\ B .~ Y ) -> B .~ Y )
17 1 2 3 4 5 6 efgcpbl 
 |-  ( ( A e. W /\ (/) e. W /\ B .~ Y ) -> ( ( A ++ B ) ++ (/) ) .~ ( ( A ++ Y ) ++ (/) ) )
18 10 15 16 17 syl3anc 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( A ++ B ) ++ (/) ) .~ ( ( A ++ Y ) ++ (/) ) )
19 10 14 eleqtrd 
 |-  ( ( A .~ X /\ B .~ Y ) -> A e. Word ( I X. 2o ) )
20 8 16 ercl 
 |-  ( ( A .~ X /\ B .~ Y ) -> B e. W )
21 20 14 eleqtrd 
 |-  ( ( A .~ X /\ B .~ Y ) -> B e. Word ( I X. 2o ) )
22 ccatcl 
 |-  ( ( A e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( A ++ B ) e. Word ( I X. 2o ) )
23 19 21 22 syl2anc 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( A ++ B ) e. Word ( I X. 2o ) )
24 ccatrid 
 |-  ( ( A ++ B ) e. Word ( I X. 2o ) -> ( ( A ++ B ) ++ (/) ) = ( A ++ B ) )
25 23 24 syl 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( A ++ B ) ++ (/) ) = ( A ++ B ) )
26 8 16 ercl2 
 |-  ( ( A .~ X /\ B .~ Y ) -> Y e. W )
27 26 14 eleqtrd 
 |-  ( ( A .~ X /\ B .~ Y ) -> Y e. Word ( I X. 2o ) )
28 ccatcl 
 |-  ( ( A e. Word ( I X. 2o ) /\ Y e. Word ( I X. 2o ) ) -> ( A ++ Y ) e. Word ( I X. 2o ) )
29 19 27 28 syl2anc 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( A ++ Y ) e. Word ( I X. 2o ) )
30 ccatrid 
 |-  ( ( A ++ Y ) e. Word ( I X. 2o ) -> ( ( A ++ Y ) ++ (/) ) = ( A ++ Y ) )
31 29 30 syl 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( A ++ Y ) ++ (/) ) = ( A ++ Y ) )
32 18 25 31 3brtr3d 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( A ++ B ) .~ ( A ++ Y ) )
33 1 2 3 4 5 6 efgcpbl 
 |-  ( ( (/) e. W /\ Y e. W /\ A .~ X ) -> ( ( (/) ++ A ) ++ Y ) .~ ( ( (/) ++ X ) ++ Y ) )
34 15 26 9 33 syl3anc 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( (/) ++ A ) ++ Y ) .~ ( ( (/) ++ X ) ++ Y ) )
35 ccatlid 
 |-  ( A e. Word ( I X. 2o ) -> ( (/) ++ A ) = A )
36 19 35 syl 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( (/) ++ A ) = A )
37 36 oveq1d 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( (/) ++ A ) ++ Y ) = ( A ++ Y ) )
38 8 9 ercl2 
 |-  ( ( A .~ X /\ B .~ Y ) -> X e. W )
39 38 14 eleqtrd 
 |-  ( ( A .~ X /\ B .~ Y ) -> X e. Word ( I X. 2o ) )
40 ccatlid 
 |-  ( X e. Word ( I X. 2o ) -> ( (/) ++ X ) = X )
41 39 40 syl 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( (/) ++ X ) = X )
42 41 oveq1d 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( ( (/) ++ X ) ++ Y ) = ( X ++ Y ) )
43 34 37 42 3brtr3d 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( A ++ Y ) .~ ( X ++ Y ) )
44 8 32 43 ertrd 
 |-  ( ( A .~ X /\ B .~ Y ) -> ( A ++ B ) .~ ( X ++ Y ) )