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