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 ) )