Metamath Proof Explorer

Theorem efgrelexlema

Description: If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A , b ends at B , and a and B have the same starting point. (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 ) ) )
efgrelexlem.1 
|- L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }
Assertion efgrelexlema 
|- ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) )

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 efgrelexlem.1 
 |-  L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }
8 7 bropaex12 
 |-  ( A L B -> ( A e. _V /\ B e. _V ) )
9 n0i 
 |-  ( a e. ( `' S " { A } ) -> -. ( `' S " { A } ) = (/) )
10 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
11 imaeq2 
 |-  ( { A } = (/) -> ( `' S " { A } ) = ( `' S " (/) ) )
12 10 11 sylbi 
 |-  ( -. A e. _V -> ( `' S " { A } ) = ( `' S " (/) ) )
13 ima0 
 |-  ( `' S " (/) ) = (/)
14 12 13 eqtrdi 
 |-  ( -. A e. _V -> ( `' S " { A } ) = (/) )
15 9 14 nsyl2 
 |-  ( a e. ( `' S " { A } ) -> A e. _V )
16 n0i 
 |-  ( b e. ( `' S " { B } ) -> -. ( `' S " { B } ) = (/) )
17 snprc 
 |-  ( -. B e. _V <-> { B } = (/) )
18 imaeq2 
 |-  ( { B } = (/) -> ( `' S " { B } ) = ( `' S " (/) ) )
19 17 18 sylbi 
 |-  ( -. B e. _V -> ( `' S " { B } ) = ( `' S " (/) ) )
20 19 13 eqtrdi 
 |-  ( -. B e. _V -> ( `' S " { B } ) = (/) )
21 16 20 nsyl2 
 |-  ( b e. ( `' S " { B } ) -> B e. _V )
22 15 21 anim12i 
 |-  ( ( a e. ( `' S " { A } ) /\ b e. ( `' S " { B } ) ) -> ( A e. _V /\ B e. _V ) )
23 22 a1d 
 |-  ( ( a e. ( `' S " { A } ) /\ b e. ( `' S " { B } ) ) -> ( ( a ` 0 ) = ( b ` 0 ) -> ( A e. _V /\ B e. _V ) ) )
24 23 rexlimivv 
 |-  ( E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) -> ( A e. _V /\ B e. _V ) )
25 fveq1 
 |-  ( c = a -> ( c ` 0 ) = ( a ` 0 ) )
26 25 eqeq1d 
 |-  ( c = a -> ( ( c ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( d ` 0 ) ) )
27 fveq1 
 |-  ( d = b -> ( d ` 0 ) = ( b ` 0 ) )
28 27 eqeq2d 
 |-  ( d = b -> ( ( a ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( b ` 0 ) ) )
29 26 28 cbvrex2vw 
 |-  ( E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) <-> E. a e. ( `' S " { i } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) )
30 sneq 
 |-  ( i = A -> { i } = { A } )
31 30 imaeq2d 
 |-  ( i = A -> ( `' S " { i } ) = ( `' S " { A } ) )
32 31 rexeqdv 
 |-  ( i = A -> ( E. a e. ( `' S " { i } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) ) )
33 29 32 bitrid 
 |-  ( i = A -> ( E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) ) )
34 sneq 
 |-  ( j = B -> { j } = { B } )
35 34 imaeq2d 
 |-  ( j = B -> ( `' S " { j } ) = ( `' S " { B } ) )
36 35 rexeqdv 
 |-  ( j = B -> ( E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) )
37 36 rexbidv 
 |-  ( j = B -> ( E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) )
38 33 37 7 brabg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) )
39 8 24 38 pm5.21nii 
 |-  ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) )