This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgcpbl

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 efgcpbl 
|- ( ( A e. W /\ B e. W /\ X .~ Y ) -> ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) )

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 eqid 
 |-  { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
8 1 2 3 4 5 6 7 efgcpbllemb 
 |-  ( ( A e. W /\ B e. W ) -> .~ C_ { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } )
9 8 ssbrd 
 |-  ( ( A e. W /\ B e. W ) -> ( X .~ Y -> X { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } Y ) )
10 9 3impia 
 |-  ( ( A e. W /\ B e. W /\ X .~ Y ) -> X { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } Y )
11 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( X { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } Y <-> ( X e. W /\ Y e. W /\ ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) )
12 11 simp3bi 
 |-  ( X { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } Y -> ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) )
13 10 12 syl 
 |-  ( ( A e. W /\ B e. W /\ X .~ Y ) -> ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) )