Metamath Proof Explorer

Theorem efgred2

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 efgred2 
|- ( ( A e. dom S /\ B e. dom S ) -> ( ( S ` A ) .~ ( 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 1 2 3 4 5 6 efgsfo 
 |-  S : dom S -onto-> W
8 fof 
 |-  ( S : dom S -onto-> W -> S : dom S --> W )
9 7 8 ax-mp 
 |-  S : dom S --> W
10 9 ffvelrni 
 |-  ( B e. dom S -> ( S ` B ) e. W )
11 10 ad2antlr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( S ` B ) e. W )
12 1 2 3 4 5 6 efgredeu 
 |-  ( ( S ` B ) e. W -> E! d e. D d .~ ( S ` B ) )
13 reurmo 
 |-  ( E! d e. D d .~ ( S ` B ) -> E* d e. D d .~ ( S ` B ) )
14 11 12 13 3syl 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> E* d e. D d .~ ( S ` B ) )
15 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` A ) ) ( A ` i ) e. ran ( T ` ( A ` ( i - 1 ) ) ) ) )
16 15 simp2bi 
 |-  ( A e. dom S -> ( A ` 0 ) e. D )
17 16 ad2antrr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( A ` 0 ) e. D )
18 1 2 efger 
 |-  .~ Er W
19 18 a1i 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> .~ Er W )
20 1 2 3 4 5 6 efgsrel 
 |-  ( A e. dom S -> ( A ` 0 ) .~ ( S ` A ) )
21 20 ad2antrr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( A ` 0 ) .~ ( S ` A ) )
22 simpr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( S ` A ) .~ ( S ` B ) )
23 19 21 22 ertrd 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( A ` 0 ) .~ ( S ` B ) )
24 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` B ) ) ( B ` i ) e. ran ( T ` ( B ` ( i - 1 ) ) ) ) )
25 24 simp2bi 
 |-  ( B e. dom S -> ( B ` 0 ) e. D )
26 25 ad2antlr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( B ` 0 ) e. D )
27 1 2 3 4 5 6 efgsrel 
 |-  ( B e. dom S -> ( B ` 0 ) .~ ( S ` B ) )
28 27 ad2antlr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( B ` 0 ) .~ ( S ` B ) )
29 breq1 
 |-  ( d = ( A ` 0 ) -> ( d .~ ( S ` B ) <-> ( A ` 0 ) .~ ( S ` B ) ) )
30 breq1 
 |-  ( d = ( B ` 0 ) -> ( d .~ ( S ` B ) <-> ( B ` 0 ) .~ ( S ` B ) ) )
31 29 30 rmoi 
 |-  ( ( E* d e. D d .~ ( S ` B ) /\ ( ( A ` 0 ) e. D /\ ( A ` 0 ) .~ ( S ` B ) ) /\ ( ( B ` 0 ) e. D /\ ( B ` 0 ) .~ ( S ` B ) ) ) -> ( A ` 0 ) = ( B ` 0 ) )
32 14 17 23 26 28 31 syl122anc 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( S ` A ) .~ ( S ` B ) ) -> ( A ` 0 ) = ( B ` 0 ) )
33 18 a1i 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> .~ Er W )
34 20 ad2antrr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ` 0 ) .~ ( S ` A ) )
35 simpr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ` 0 ) = ( B ` 0 ) )
36 27 ad2antlr 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( B ` 0 ) .~ ( S ` B ) )
37 35 36 eqbrtrd 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ` 0 ) .~ ( S ` B ) )
38 33 34 37 ertr3d 
 |-  ( ( ( A e. dom S /\ B e. dom S ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( S ` A ) .~ ( S ` B ) )
39 32 38 impbida 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( ( S ` A ) .~ ( S ` B ) <-> ( A ` 0 ) = ( B ` 0 ) ) )