Metamath Proof Explorer

Theorem efgs1b

Description: Every extension sequence ending in an irreducible word is trivial. (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 efgs1b 
|- ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )

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 eldifn 
 |-  ( ( S ` A ) e. ( W \ U_ x e. W ran ( T ` x ) ) -> -. ( S ` A ) e. U_ x e. W ran ( T ` x ) )
8 7 5 eleq2s 
 |-  ( ( S ` A ) e. D -> -. ( S ` A ) e. U_ x e. W ran ( T ` x ) )
9 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. a e. ( 1 ..^ ( # ` A ) ) ( A ` a ) e. ran ( T ` ( A ` ( a - 1 ) ) ) ) )
10 9 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
11 eldifsn 
 |-  ( A e. ( Word W \ { (/) } ) <-> ( A e. Word W /\ A =/= (/) ) )
12 lennncl 
 |-  ( ( A e. Word W /\ A =/= (/) ) -> ( # ` A ) e. NN )
13 11 12 sylbi 
 |-  ( A e. ( Word W \ { (/) } ) -> ( # ` A ) e. NN )
14 10 13 syl 
 |-  ( A e. dom S -> ( # ` A ) e. NN )
15 elnn1uz2 
 |-  ( ( # ` A ) e. NN <-> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
16 14 15 sylib 
 |-  ( A e. dom S -> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
17 16 ord 
 |-  ( A e. dom S -> ( -. ( # ` A ) = 1 -> ( # ` A ) e. ( ZZ>= ` 2 ) ) )
18 10 eldifad 
 |-  ( A e. dom S -> A e. Word W )
19 18 adantr 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> A e. Word W )
20 wrdf 
 |-  ( A e. Word W -> A : ( 0 ..^ ( # ` A ) ) --> W )
21 19 20 syl 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> A : ( 0 ..^ ( # ` A ) ) --> W )
22 1z 
 |-  1 e. ZZ
23 simpr 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( # ` A ) e. ( ZZ>= ` 2 ) )
24 df-2 
 |-  2 = ( 1 + 1 )
25 24 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
26 23 25 eleqtrdi 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( # ` A ) e. ( ZZ>= ` ( 1 + 1 ) ) )
27 eluzp1m1 
 |-  ( ( 1 e. ZZ /\ ( # ` A ) e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( # ` A ) - 1 ) e. ( ZZ>= ` 1 ) )
28 22 26 27 sylancr 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` A ) - 1 ) e. ( ZZ>= ` 1 ) )
29 nnuz 
 |-  NN = ( ZZ>= ` 1 )
30 28 29 eleqtrrdi 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` A ) - 1 ) e. NN )
31 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) <-> ( ( # ` A ) - 1 ) e. NN )
32 30 31 sylibr 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
33 fzoend 
 |-  ( 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
34 elfzofz 
 |-  ( ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` A ) - 1 ) ) )
35 32 33 34 3syl 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` A ) - 1 ) ) )
36 eluzelz 
 |-  ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( # ` A ) e. ZZ )
37 36 adantl 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( # ` A ) e. ZZ )
38 fzoval 
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
39 37 38 syl 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
40 35 39 eleqtrrd 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( # ` A ) ) )
41 21 40 ffvelrnd 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. W )
42 uz2m1nn 
 |-  ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( ( # ` A ) - 1 ) e. NN )
43 1 2 3 4 5 6 efgsdmi 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. NN ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
44 42 43 sylan2 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
45 fveq2 
 |-  ( a = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) -> ( T ` a ) = ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
46 45 rneqd 
 |-  ( a = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) -> ran ( T ` a ) = ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
47 46 eliuni 
 |-  ( ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. W /\ ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) -> ( S ` A ) e. U_ a e. W ran ( T ` a ) )
48 41 44 47 syl2anc 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( S ` A ) e. U_ a e. W ran ( T ` a ) )
49 fveq2 
 |-  ( a = x -> ( T ` a ) = ( T ` x ) )
50 49 rneqd 
 |-  ( a = x -> ran ( T ` a ) = ran ( T ` x ) )
51 50 cbviunv 
 |-  U_ a e. W ran ( T ` a ) = U_ x e. W ran ( T ` x )
52 48 51 eleqtrdi 
 |-  ( ( A e. dom S /\ ( # ` A ) e. ( ZZ>= ` 2 ) ) -> ( S ` A ) e. U_ x e. W ran ( T ` x ) )
53 52 ex 
 |-  ( A e. dom S -> ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( S ` A ) e. U_ x e. W ran ( T ` x ) ) )
54 17 53 syld 
 |-  ( A e. dom S -> ( -. ( # ` A ) = 1 -> ( S ` A ) e. U_ x e. W ran ( T ` x ) ) )
55 54 con1d 
 |-  ( A e. dom S -> ( -. ( S ` A ) e. U_ x e. W ran ( T ` x ) -> ( # ` A ) = 1 ) )
56 8 55 syl5 
 |-  ( A e. dom S -> ( ( S ` A ) e. D -> ( # ` A ) = 1 ) )
57 9 simp2bi 
 |-  ( A e. dom S -> ( A ` 0 ) e. D )
58 oveq1 
 |-  ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = ( 1 - 1 ) )
59 1m1e0 
 |-  ( 1 - 1 ) = 0
60 58 59 eqtrdi 
 |-  ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = 0 )
61 60 fveq2d 
 |-  ( ( # ` A ) = 1 -> ( A ` ( ( # ` A ) - 1 ) ) = ( A ` 0 ) )
62 61 eleq1d 
 |-  ( ( # ` A ) = 1 -> ( ( A ` ( ( # ` A ) - 1 ) ) e. D <-> ( A ` 0 ) e. D ) )
63 57 62 syl5ibrcom 
 |-  ( A e. dom S -> ( ( # ` A ) = 1 -> ( A ` ( ( # ` A ) - 1 ) ) e. D ) )
64 1 2 3 4 5 6 efgsval 
 |-  ( A e. dom S -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
65 64 eleq1d 
 |-  ( A e. dom S -> ( ( S ` A ) e. D <-> ( A ` ( ( # ` A ) - 1 ) ) e. D ) )
66 63 65 sylibrd 
 |-  ( A e. dom S -> ( ( # ` A ) = 1 -> ( S ` A ) e. D ) )
67 56 66 impbid 
 |-  ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )