Metamath Proof Explorer

Theorem efgredlemb

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-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 ) ) )
efgredlem.1 
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
efgredlem.2 
|- ( ph -> A e. dom S )
efgredlem.3 
|- ( ph -> B e. dom S )
efgredlem.4 
|- ( ph -> ( S ` A ) = ( S ` B ) )
efgredlem.5 
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
efgredlemb.k 
|- K = ( ( ( # ` A ) - 1 ) - 1 )
efgredlemb.l 
|- L = ( ( ( # ` B ) - 1 ) - 1 )
efgredlemb.p 
|- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
efgredlemb.q 
|- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
efgredlemb.u 
|- ( ph -> U e. ( I X. 2o ) )
efgredlemb.v 
|- ( ph -> V e. ( I X. 2o ) )
efgredlemb.6 
|- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
efgredlemb.7 
|- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
efgredlemb.8 
|- ( ph -> -. ( A ` K ) = ( B ` L ) )
Assertion efgredlemb 
|- -. ph

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 efgredlem.1 
 |-  ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
8 efgredlem.2 
 |-  ( ph -> A e. dom S )
9 efgredlem.3 
 |-  ( ph -> B e. dom S )
10 efgredlem.4 
 |-  ( ph -> ( S ` A ) = ( S ` B ) )
11 efgredlem.5 
 |-  ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
12 efgredlemb.k 
 |-  K = ( ( ( # ` A ) - 1 ) - 1 )
13 efgredlemb.l 
 |-  L = ( ( ( # ` B ) - 1 ) - 1 )
14 efgredlemb.p 
 |-  ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
15 efgredlemb.q 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
16 efgredlemb.u 
 |-  ( ph -> U e. ( I X. 2o ) )
17 efgredlemb.v 
 |-  ( ph -> V e. ( I X. 2o ) )
18 efgredlemb.6 
 |-  ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
19 efgredlemb.7 
 |-  ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
20 efgredlemb.8 
 |-  ( ph -> -. ( A ` K ) = ( B ` L ) )
21 fveq2 
 |-  ( ( S ` A ) = ( S ` B ) -> ( # ` ( S ` A ) ) = ( # ` ( S ` B ) ) )
22 21 breq2d 
 |-  ( ( S ` A ) = ( S ` B ) -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) <-> ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) ) )
23 22 imbi1d 
 |-  ( ( S ` A ) = ( S ` B ) -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
24 23 2ralbidv 
 |-  ( ( S ` A ) = ( S ` B ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
25 10 24 syl 
 |-  ( ph -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
26 7 25 mpbid 
 |-  ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
27 10 eqcomd 
 |-  ( ph -> ( S ` B ) = ( S ` A ) )
28 eqcom 
 |-  ( ( A ` 0 ) = ( B ` 0 ) <-> ( B ` 0 ) = ( A ` 0 ) )
29 11 28 sylnib 
 |-  ( ph -> -. ( B ` 0 ) = ( A ` 0 ) )
30 eqcom 
 |-  ( ( A ` K ) = ( B ` L ) <-> ( B ` L ) = ( A ` K ) )
31 20 30 sylnib 
 |-  ( ph -> -. ( B ` L ) = ( A ` K ) )
32 1 2 3 4 5 6 26 9 8 27 29 13 12 15 14 17 16 19 18 31 efgredlemc 
 |-  ( ph -> ( Q e. ( ZZ>= ` P ) -> ( B ` 0 ) = ( A ` 0 ) ) )
33 32 28 syl6ibr 
 |-  ( ph -> ( Q e. ( ZZ>= ` P ) -> ( A ` 0 ) = ( B ` 0 ) ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 efgredlemc 
 |-  ( ph -> ( P e. ( ZZ>= ` Q ) -> ( A ` 0 ) = ( B ` 0 ) ) )
35 elfzelz 
 |-  ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ZZ )
36 14 35 syl 
 |-  ( ph -> P e. ZZ )
37 elfzelz 
 |-  ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) -> Q e. ZZ )
38 15 37 syl 
 |-  ( ph -> Q e. ZZ )
39 uztric 
 |-  ( ( P e. ZZ /\ Q e. ZZ ) -> ( Q e. ( ZZ>= ` P ) \/ P e. ( ZZ>= ` Q ) ) )
40 36 38 39 syl2anc 
 |-  ( ph -> ( Q e. ( ZZ>= ` P ) \/ P e. ( ZZ>= ` Q ) ) )
41 33 34 40 mpjaod 
 |-  ( ph -> ( A ` 0 ) = ( B ` 0 ) )
42 41 11 pm2.65i 
 |-  -. ph