This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgsdmi

Description: Property of the last link in the chain of extensions. (Contributed by Mario Carneiro, 29-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 ) ) )
Assertion efgsdmi 
|- ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( S ` F ) e. ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 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 1 2 3 4 5 6 efgsval 
 |-  ( F e. dom S -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
8 7 adantr 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
9 fveq2 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( F ` i ) = ( F ` ( ( # ` F ) - 1 ) ) )
10 fvoveq1 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( F ` ( i - 1 ) ) = ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) )
11 10 fveq2d 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( T ` ( F ` ( i - 1 ) ) ) = ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) )
12 11 rneqd 
 |-  ( i = ( ( # ` F ) - 1 ) -> ran ( T ` ( F ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) )
13 9 12 eleq12d 
 |-  ( i = ( ( # ` F ) - 1 ) -> ( ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) <-> ( F ` ( ( # ` F ) - 1 ) ) e. ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) ) )
14 1 2 3 4 5 6 efgsdm 
 |-  ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
15 14 simp3bi 
 |-  ( F e. dom S -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
16 15 adantr 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
17 simpr 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( ( # ` F ) - 1 ) e. NN )
18 nnuz 
 |-  NN = ( ZZ>= ` 1 )
19 17 18 eleqtrdi 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( ( # ` F ) - 1 ) e. ( ZZ>= ` 1 ) )
20 eluzfz1 
 |-  ( ( ( # ` F ) - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( ( # ` F ) - 1 ) ) )
21 19 20 syl 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> 1 e. ( 1 ... ( ( # ` F ) - 1 ) ) )
22 14 simp1bi 
 |-  ( F e. dom S -> F e. ( Word W \ { (/) } ) )
23 22 adantr 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> F e. ( Word W \ { (/) } ) )
24 23 eldifad 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> F e. Word W )
25 lencl 
 |-  ( F e. Word W -> ( # ` F ) e. NN0 )
26 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
27 fzoval 
 |-  ( ( # ` F ) e. ZZ -> ( 1 ..^ ( # ` F ) ) = ( 1 ... ( ( # ` F ) - 1 ) ) )
28 24 25 26 27 4syl 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( 1 ..^ ( # ` F ) ) = ( 1 ... ( ( # ` F ) - 1 ) ) )
29 21 28 eleqtrrd 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> 1 e. ( 1 ..^ ( # ` F ) ) )
30 fzoend 
 |-  ( 1 e. ( 1 ..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. ( 1 ..^ ( # ` F ) ) )
31 29 30 syl 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( ( # ` F ) - 1 ) e. ( 1 ..^ ( # ` F ) ) )
32 13 16 31 rspcdva 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( F ` ( ( # ` F ) - 1 ) ) e. ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) )
33 8 32 eqeltrd 
 |-  ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( S ` F ) e. ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) )