Metamath Proof Explorer

Theorem efgredlema

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (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 ) ) )
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 ) )
Assertion efgredlema 
|- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )

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 1 2 3 4 5 6 efgsval 
 |-  ( B e. dom S -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
13 9 12 syl 
 |-  ( ph -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
14 1 2 3 4 5 6 efgsval 
 |-  ( A e. dom S -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
15 8 14 syl 
 |-  ( ph -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
16 10 15 eqtr3d 
 |-  ( ph -> ( S ` B ) = ( A ` ( ( # ` A ) - 1 ) ) )
17 13 16 eqtr3d 
 |-  ( ph -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` ( ( # ` A ) - 1 ) ) )
18 oveq1 
 |-  ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = ( 1 - 1 ) )
19 1m1e0 
 |-  ( 1 - 1 ) = 0
20 18 19 eqtrdi 
 |-  ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = 0 )
21 20 fveq2d 
 |-  ( ( # ` A ) = 1 -> ( A ` ( ( # ` A ) - 1 ) ) = ( A ` 0 ) )
22 17 21 sylan9eq 
 |-  ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` 0 ) )
23 10 eleq1d 
 |-  ( ph -> ( ( S ` A ) e. D <-> ( S ` B ) e. D ) )
24 1 2 3 4 5 6 efgs1b 
 |-  ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )
25 8 24 syl 
 |-  ( ph -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )
26 1 2 3 4 5 6 efgs1b 
 |-  ( B e. dom S -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) )
27 9 26 syl 
 |-  ( ph -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) )
28 23 25 27 3bitr3d 
 |-  ( ph -> ( ( # ` A ) = 1 <-> ( # ` B ) = 1 ) )
29 28 biimpa 
 |-  ( ( ph /\ ( # ` A ) = 1 ) -> ( # ` B ) = 1 )
30 oveq1 
 |-  ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = ( 1 - 1 ) )
31 30 19 eqtrdi 
 |-  ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = 0 )
32 31 fveq2d 
 |-  ( ( # ` B ) = 1 -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) )
33 29 32 syl 
 |-  ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) )
34 22 33 eqtr3d 
 |-  ( ( ph /\ ( # ` A ) = 1 ) -> ( A ` 0 ) = ( B ` 0 ) )
35 11 34 mtand 
 |-  ( ph -> -. ( # ` A ) = 1 )
36 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` A ) ) ( A ` u ) e. ran ( T ` ( A ` ( u - 1 ) ) ) ) )
37 36 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
38 eldifsn 
 |-  ( A e. ( Word W \ { (/) } ) <-> ( A e. Word W /\ A =/= (/) ) )
39 lennncl 
 |-  ( ( A e. Word W /\ A =/= (/) ) -> ( # ` A ) e. NN )
40 38 39 sylbi 
 |-  ( A e. ( Word W \ { (/) } ) -> ( # ` A ) e. NN )
41 8 37 40 3syl 
 |-  ( ph -> ( # ` A ) e. NN )
42 elnn1uz2 
 |-  ( ( # ` A ) e. NN <-> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
43 41 42 sylib 
 |-  ( ph -> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
44 43 ord 
 |-  ( ph -> ( -. ( # ` A ) = 1 -> ( # ` A ) e. ( ZZ>= ` 2 ) ) )
45 35 44 mpd 
 |-  ( ph -> ( # ` A ) e. ( ZZ>= ` 2 ) )
46 uz2m1nn 
 |-  ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( ( # ` A ) - 1 ) e. NN )
47 45 46 syl 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
48 35 28 mtbid 
 |-  ( ph -> -. ( # ` B ) = 1 )
49 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` B ) ) ( B ` u ) e. ran ( T ` ( B ` ( u - 1 ) ) ) ) )
50 49 simp1bi 
 |-  ( B e. dom S -> B e. ( Word W \ { (/) } ) )
51 eldifsn 
 |-  ( B e. ( Word W \ { (/) } ) <-> ( B e. Word W /\ B =/= (/) ) )
52 lennncl 
 |-  ( ( B e. Word W /\ B =/= (/) ) -> ( # ` B ) e. NN )
53 51 52 sylbi 
 |-  ( B e. ( Word W \ { (/) } ) -> ( # ` B ) e. NN )
54 9 50 53 3syl 
 |-  ( ph -> ( # ` B ) e. NN )
55 elnn1uz2 
 |-  ( ( # ` B ) e. NN <-> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
56 54 55 sylib 
 |-  ( ph -> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
57 56 ord 
 |-  ( ph -> ( -. ( # ` B ) = 1 -> ( # ` B ) e. ( ZZ>= ` 2 ) ) )
58 48 57 mpd 
 |-  ( ph -> ( # ` B ) e. ( ZZ>= ` 2 ) )
59 uz2m1nn 
 |-  ( ( # ` B ) e. ( ZZ>= ` 2 ) -> ( ( # ` B ) - 1 ) e. NN )
60 58 59 syl 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. NN )
61 47 60 jca 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )