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
|
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 ) ) ) ) ) |
8 |
7
|
simp1bi |
|- ( F e. dom S -> F e. ( Word W \ { (/) } ) ) |
9 |
8
|
adantr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> F e. ( Word W \ { (/) } ) ) |
10 |
9
|
eldifad |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> F e. Word W ) |
11 |
|
fz1ssfz0 |
|- ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) |
12 |
|
simpr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. ( 1 ... ( # ` F ) ) ) |
13 |
11 12
|
sselid |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. ( 0 ... ( # ` F ) ) ) |
14 |
|
pfxres |
|- ( ( F e. Word W /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) ) |
15 |
10 13 14
|
syl2anc |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) ) |
16 |
|
pfxcl |
|- ( F e. Word W -> ( F prefix N ) e. Word W ) |
17 |
10 16
|
syl |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) e. Word W ) |
18 |
15 17
|
eqeltrrd |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. Word W ) |
19 |
|
pfxlen |
|- ( ( F e. Word W /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N ) |
20 |
10 13 19
|
syl2anc |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N ) |
21 |
|
elfznn |
|- ( N e. ( 1 ... ( # ` F ) ) -> N e. NN ) |
22 |
21
|
adantl |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. NN ) |
23 |
20 22
|
eqeltrd |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) e. NN ) |
24 |
|
wrdfin |
|- ( ( F prefix N ) e. Word W -> ( F prefix N ) e. Fin ) |
25 |
|
hashnncl |
|- ( ( F prefix N ) e. Fin -> ( ( # ` ( F prefix N ) ) e. NN <-> ( F prefix N ) =/= (/) ) ) |
26 |
17 24 25
|
3syl |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( # ` ( F prefix N ) ) e. NN <-> ( F prefix N ) =/= (/) ) ) |
27 |
23 26
|
mpbid |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) =/= (/) ) |
28 |
15 27
|
eqnetrrd |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) =/= (/) ) |
29 |
|
eldifsn |
|- ( ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) <-> ( ( F |` ( 0 ..^ N ) ) e. Word W /\ ( F |` ( 0 ..^ N ) ) =/= (/) ) ) |
30 |
18 28 29
|
sylanbrc |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) ) |
31 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ N ) <-> N e. NN ) |
32 |
22 31
|
sylibr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> 0 e. ( 0 ..^ N ) ) |
33 |
32
|
fvresd |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( F |` ( 0 ..^ N ) ) ` 0 ) = ( F ` 0 ) ) |
34 |
7
|
simp2bi |
|- ( F e. dom S -> ( F ` 0 ) e. D ) |
35 |
34
|
adantr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F ` 0 ) e. D ) |
36 |
33 35
|
eqeltrd |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( F |` ( 0 ..^ N ) ) ` 0 ) e. D ) |
37 |
|
elfzuz3 |
|- ( N e. ( 1 ... ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) ) |
38 |
37
|
adantl |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) ) |
39 |
|
fzoss2 |
|- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) ) |
40 |
38 39
|
syl |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) ) |
41 |
7
|
simp3bi |
|- ( F e. dom S -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) |
42 |
41
|
adantr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) |
43 |
|
ssralv |
|- ( ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) -> ( A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) -> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) ) |
44 |
40 42 43
|
sylc |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) |
45 |
|
fzo0ss1 |
|- ( 1 ..^ N ) C_ ( 0 ..^ N ) |
46 |
45
|
sseli |
|- ( i e. ( 1 ..^ N ) -> i e. ( 0 ..^ N ) ) |
47 |
46
|
fvresd |
|- ( i e. ( 1 ..^ N ) -> ( ( F |` ( 0 ..^ N ) ) ` i ) = ( F ` i ) ) |
48 |
|
elfzoel2 |
|- ( i e. ( 1 ..^ N ) -> N e. ZZ ) |
49 |
|
peano2zm |
|- ( N e. ZZ -> ( N - 1 ) e. ZZ ) |
50 |
48 49
|
syl |
|- ( i e. ( 1 ..^ N ) -> ( N - 1 ) e. ZZ ) |
51 |
|
uzid |
|- ( N e. ZZ -> N e. ( ZZ>= ` N ) ) |
52 |
48 51
|
syl |
|- ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` N ) ) |
53 |
48
|
zcnd |
|- ( i e. ( 1 ..^ N ) -> N e. CC ) |
54 |
|
ax-1cn |
|- 1 e. CC |
55 |
|
npcan |
|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N ) |
56 |
53 54 55
|
sylancl |
|- ( i e. ( 1 ..^ N ) -> ( ( N - 1 ) + 1 ) = N ) |
57 |
56
|
fveq2d |
|- ( i e. ( 1 ..^ N ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) ) |
58 |
52 57
|
eleqtrrd |
|- ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) |
59 |
|
peano2uzr |
|- ( ( ( N - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) -> N e. ( ZZ>= ` ( N - 1 ) ) ) |
60 |
50 58 59
|
syl2anc |
|- ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( N - 1 ) ) ) |
61 |
|
fzoss2 |
|- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) ) |
62 |
60 61
|
syl |
|- ( i e. ( 1 ..^ N ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) ) |
63 |
|
elfzo1elm1fzo0 |
|- ( i e. ( 1 ..^ N ) -> ( i - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) |
64 |
62 63
|
sseldd |
|- ( i e. ( 1 ..^ N ) -> ( i - 1 ) e. ( 0 ..^ N ) ) |
65 |
64
|
fvresd |
|- ( i e. ( 1 ..^ N ) -> ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) ) |
66 |
65
|
fveq2d |
|- ( i e. ( 1 ..^ N ) -> ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) = ( T ` ( F ` ( i - 1 ) ) ) ) |
67 |
66
|
rneqd |
|- ( i e. ( 1 ..^ N ) -> ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( i - 1 ) ) ) ) |
68 |
47 67
|
eleq12d |
|- ( i e. ( 1 ..^ N ) -> ( ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) ) |
69 |
68
|
ralbiia |
|- ( A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) |
70 |
44 69
|
sylibr |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) |
71 |
15
|
fveq2d |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = ( # ` ( F |` ( 0 ..^ N ) ) ) ) |
72 |
71 20
|
eqtr3d |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = N ) |
73 |
72
|
oveq2d |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) = ( 1 ..^ N ) ) |
74 |
73
|
raleqdv |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) ) |
75 |
70 74
|
mpbird |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) |
76 |
1 2 3 4 5 6
|
efgsdm |
|- ( ( F |` ( 0 ..^ N ) ) e. dom S <-> ( ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) /\ ( ( F |` ( 0 ..^ N ) ) ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) ) |
77 |
30 36 75 76
|
syl3anbrc |
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. dom S ) |