Metamath Proof Explorer

Theorem efgcpbllema

Description: Lemma for efgrelex . Define an auxiliary equivalence relation L such that A L B if there are sequences from A to B passing through the same reduced word. (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 ) ) )
efgcpbllem.1 
|- L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
Assertion efgcpbllema 
|- ( X L Y <-> ( X e. W /\ Y e. W /\ ( ( 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 efgcpbllem.1 
 |-  L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
8 oveq2 
 |-  ( i = X -> ( A ++ i ) = ( A ++ X ) )
9 8 oveq1d 
 |-  ( i = X -> ( ( A ++ i ) ++ B ) = ( ( A ++ X ) ++ B ) )
10 oveq2 
 |-  ( j = Y -> ( A ++ j ) = ( A ++ Y ) )
11 10 oveq1d 
 |-  ( j = Y -> ( ( A ++ j ) ++ B ) = ( ( A ++ Y ) ++ B ) )
12 9 11 breqan12d 
 |-  ( ( i = X /\ j = Y ) -> ( ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) <-> ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) )
13 vex 
 |-  i e. _V
14 vex 
 |-  j e. _V
15 13 14 prss 
 |-  ( ( i e. W /\ j e. W ) <-> { i , j } C_ W )
16 15 anbi1i 
 |-  ( ( ( i e. W /\ j e. W ) /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) <-> ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) )
17 16 opabbii 
 |-  { <. i , j >. | ( ( i e. W /\ j e. W ) /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) } = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
18 7 17 eqtr4i 
 |-  L = { <. i , j >. | ( ( i e. W /\ j e. W ) /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
19 12 18 brab2a 
 |-  ( X L Y <-> ( ( X e. W /\ Y e. W ) /\ ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) )
20 df-3an 
 |-  ( ( X e. W /\ Y e. W /\ ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) <-> ( ( X e. W /\ Y e. W ) /\ ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) )
21 19 20 bitr4i 
 |-  ( X L Y <-> ( X e. W /\ Y e. W /\ ( ( A ++ X ) ++ B ) .~ ( ( A ++ Y ) ++ B ) ) )