Step |
Hyp |
Ref |
Expression |
1 |
|
f1f |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A -> F : ( 0 ..^ ( # ` F ) ) --> A ) |
2 |
|
iswrdi |
|- ( F : ( 0 ..^ ( # ` F ) ) --> A -> F e. Word A ) |
3 |
1 2
|
syl |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A -> F e. Word A ) |
4 |
|
cshwf |
|- ( ( F e. Word A /\ S e. ZZ ) -> ( F cyclShift S ) : ( 0 ..^ ( # ` F ) ) --> A ) |
5 |
4
|
3adant1 |
|- ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) -> ( F cyclShift S ) : ( 0 ..^ ( # ` F ) ) --> A ) |
6 |
5
|
adantr |
|- ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> ( F cyclShift S ) : ( 0 ..^ ( # ` F ) ) --> A ) |
7 |
|
feq1 |
|- ( G = ( F cyclShift S ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A <-> ( F cyclShift S ) : ( 0 ..^ ( # ` F ) ) --> A ) ) |
8 |
7
|
adantl |
|- ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A <-> ( F cyclShift S ) : ( 0 ..^ ( # ` F ) ) --> A ) ) |
9 |
6 8
|
mpbird |
|- ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> G : ( 0 ..^ ( # ` F ) ) --> A ) |
10 |
|
dff13 |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A <-> ( F : ( 0 ..^ ( # ` F ) ) --> A /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) |
11 |
|
fveq1 |
|- ( G = ( F cyclShift S ) -> ( G ` i ) = ( ( F cyclShift S ) ` i ) ) |
12 |
11
|
3ad2ant1 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( G ` i ) = ( ( F cyclShift S ) ` i ) ) |
13 |
12
|
adantr |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( G ` i ) = ( ( F cyclShift S ) ` i ) ) |
14 |
|
cshwidxmod |
|- ( ( F e. Word A /\ S e. ZZ /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) |
15 |
14
|
3expia |
|- ( ( F e. Word A /\ S e. ZZ ) -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) ) |
16 |
15
|
3adant1 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) ) |
17 |
16
|
com12 |
|- ( i e. ( 0 ..^ ( # ` F ) ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) ) |
18 |
17
|
adantr |
|- ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) ) |
19 |
18
|
impcom |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( F cyclShift S ) ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) |
20 |
13 19
|
eqtrd |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( G ` i ) = ( F ` ( ( i + S ) mod ( # ` F ) ) ) ) |
21 |
|
fveq1 |
|- ( G = ( F cyclShift S ) -> ( G ` j ) = ( ( F cyclShift S ) ` j ) ) |
22 |
21
|
3ad2ant1 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( G ` j ) = ( ( F cyclShift S ) ` j ) ) |
23 |
22
|
adantr |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( G ` j ) = ( ( F cyclShift S ) ` j ) ) |
24 |
|
cshwidxmod |
|- ( ( F e. Word A /\ S e. ZZ /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
25 |
24
|
3expia |
|- ( ( F e. Word A /\ S e. ZZ ) -> ( j e. ( 0 ..^ ( # ` F ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
26 |
25
|
3adant1 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( j e. ( 0 ..^ ( # ` F ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
27 |
26
|
adantld |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
28 |
27
|
imp |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
29 |
23 28
|
eqtrd |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( G ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
30 |
20 29
|
eqeq12d |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( G ` i ) = ( G ` j ) <-> ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
31 |
30
|
adantlr |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( G ` i ) = ( G ` j ) <-> ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
32 |
|
elfzo0 |
|- ( i e. ( 0 ..^ ( # ` F ) ) <-> ( i e. NN0 /\ ( # ` F ) e. NN /\ i < ( # ` F ) ) ) |
33 |
|
nn0z |
|- ( i e. NN0 -> i e. ZZ ) |
34 |
33
|
adantr |
|- ( ( i e. NN0 /\ ( # ` F ) e. NN ) -> i e. ZZ ) |
35 |
34
|
adantl |
|- ( ( S e. ZZ /\ ( i e. NN0 /\ ( # ` F ) e. NN ) ) -> i e. ZZ ) |
36 |
|
simpl |
|- ( ( S e. ZZ /\ ( i e. NN0 /\ ( # ` F ) e. NN ) ) -> S e. ZZ ) |
37 |
35 36
|
zaddcld |
|- ( ( S e. ZZ /\ ( i e. NN0 /\ ( # ` F ) e. NN ) ) -> ( i + S ) e. ZZ ) |
38 |
|
simpr |
|- ( ( i e. NN0 /\ ( # ` F ) e. NN ) -> ( # ` F ) e. NN ) |
39 |
38
|
adantl |
|- ( ( S e. ZZ /\ ( i e. NN0 /\ ( # ` F ) e. NN ) ) -> ( # ` F ) e. NN ) |
40 |
37 39
|
jca |
|- ( ( S e. ZZ /\ ( i e. NN0 /\ ( # ` F ) e. NN ) ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) |
41 |
40
|
ex |
|- ( S e. ZZ -> ( ( i e. NN0 /\ ( # ` F ) e. NN ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
42 |
41
|
3ad2ant3 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i e. NN0 /\ ( # ` F ) e. NN ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
43 |
42
|
com12 |
|- ( ( i e. NN0 /\ ( # ` F ) e. NN ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
44 |
43
|
3adant3 |
|- ( ( i e. NN0 /\ ( # ` F ) e. NN /\ i < ( # ` F ) ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
45 |
32 44
|
sylbi |
|- ( i e. ( 0 ..^ ( # ` F ) ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
46 |
45
|
adantr |
|- ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
47 |
46
|
impcom |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) ) |
48 |
|
zmodfzo |
|- ( ( ( i + S ) e. ZZ /\ ( # ` F ) e. NN ) -> ( ( i + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) ) |
49 |
47 48
|
syl |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( i + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) ) |
50 |
|
elfzo0 |
|- ( j e. ( 0 ..^ ( # ` F ) ) <-> ( j e. NN0 /\ ( # ` F ) e. NN /\ j < ( # ` F ) ) ) |
51 |
|
nn0z |
|- ( j e. NN0 -> j e. ZZ ) |
52 |
51
|
adantr |
|- ( ( j e. NN0 /\ ( # ` F ) e. NN ) -> j e. ZZ ) |
53 |
52
|
adantl |
|- ( ( S e. ZZ /\ ( j e. NN0 /\ ( # ` F ) e. NN ) ) -> j e. ZZ ) |
54 |
|
simpl |
|- ( ( S e. ZZ /\ ( j e. NN0 /\ ( # ` F ) e. NN ) ) -> S e. ZZ ) |
55 |
53 54
|
zaddcld |
|- ( ( S e. ZZ /\ ( j e. NN0 /\ ( # ` F ) e. NN ) ) -> ( j + S ) e. ZZ ) |
56 |
|
simpr |
|- ( ( j e. NN0 /\ ( # ` F ) e. NN ) -> ( # ` F ) e. NN ) |
57 |
56
|
adantl |
|- ( ( S e. ZZ /\ ( j e. NN0 /\ ( # ` F ) e. NN ) ) -> ( # ` F ) e. NN ) |
58 |
55 57
|
jca |
|- ( ( S e. ZZ /\ ( j e. NN0 /\ ( # ` F ) e. NN ) ) -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) |
59 |
58
|
expcom |
|- ( ( j e. NN0 /\ ( # ` F ) e. NN ) -> ( S e. ZZ -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
60 |
59
|
3adant3 |
|- ( ( j e. NN0 /\ ( # ` F ) e. NN /\ j < ( # ` F ) ) -> ( S e. ZZ -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
61 |
50 60
|
sylbi |
|- ( j e. ( 0 ..^ ( # ` F ) ) -> ( S e. ZZ -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
62 |
61
|
com12 |
|- ( S e. ZZ -> ( j e. ( 0 ..^ ( # ` F ) ) -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
63 |
62
|
3ad2ant3 |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( j e. ( 0 ..^ ( # ` F ) ) -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
64 |
63
|
adantld |
|- ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) -> ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) ) |
65 |
64
|
imp |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) ) |
66 |
|
zmodfzo |
|- ( ( ( j + S ) e. ZZ /\ ( # ` F ) e. NN ) -> ( ( j + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) ) |
67 |
65 66
|
syl |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( j + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) ) |
68 |
|
fveqeq2 |
|- ( x = ( ( i + S ) mod ( # ` F ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` y ) ) ) |
69 |
|
eqeq1 |
|- ( x = ( ( i + S ) mod ( # ` F ) ) -> ( x = y <-> ( ( i + S ) mod ( # ` F ) ) = y ) ) |
70 |
68 69
|
imbi12d |
|- ( x = ( ( i + S ) mod ( # ` F ) ) -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` y ) -> ( ( i + S ) mod ( # ` F ) ) = y ) ) ) |
71 |
|
fveq2 |
|- ( y = ( ( j + S ) mod ( # ` F ) ) -> ( F ` y ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
72 |
71
|
eqeq2d |
|- ( y = ( ( j + S ) mod ( # ` F ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` y ) <-> ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) ) |
73 |
|
eqeq2 |
|- ( y = ( ( j + S ) mod ( # ` F ) ) -> ( ( ( i + S ) mod ( # ` F ) ) = y <-> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) |
74 |
72 73
|
imbi12d |
|- ( y = ( ( j + S ) mod ( # ` F ) ) -> ( ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` y ) -> ( ( i + S ) mod ( # ` F ) ) = y ) <-> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) ) |
75 |
70 74
|
rspc2v |
|- ( ( ( ( i + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) /\ ( ( j + S ) mod ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) ) |
76 |
49 67 75
|
syl2anc |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) ) |
77 |
|
simpr |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) /\ ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) |
78 |
|
addmodlteq |
|- ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) /\ S e. ZZ ) -> ( ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) <-> i = j ) ) |
79 |
78
|
3expa |
|- ( ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) /\ S e. ZZ ) -> ( ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) <-> i = j ) ) |
80 |
79
|
ancoms |
|- ( ( S e. ZZ /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) <-> i = j ) ) |
81 |
80
|
bicomd |
|- ( ( S e. ZZ /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( i = j <-> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) |
82 |
81
|
3ad2antl3 |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( i = j <-> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) |
83 |
82
|
adantr |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) /\ ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) -> ( i = j <-> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) |
84 |
77 83
|
sylibrd |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) /\ ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> i = j ) ) |
85 |
84
|
ex |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> ( ( i + S ) mod ( # ` F ) ) = ( ( j + S ) mod ( # ` F ) ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> i = j ) ) ) |
86 |
76 85
|
syld |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> i = j ) ) ) |
87 |
86
|
impancom |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) -> ( ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> i = j ) ) ) |
88 |
87
|
imp |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( F ` ( ( i + S ) mod ( # ` F ) ) ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) -> i = j ) ) |
89 |
31 88
|
sylbid |
|- ( ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) /\ ( i e. ( 0 ..^ ( # ` F ) ) /\ j e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( G ` i ) = ( G ` j ) -> i = j ) ) |
90 |
89
|
ralrimivva |
|- ( ( ( G = ( F cyclShift S ) /\ F e. Word A /\ S e. ZZ ) /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) |
91 |
90
|
3exp1 |
|- ( G = ( F cyclShift S ) -> ( F e. Word A -> ( S e. ZZ -> ( A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) |
92 |
91
|
com14 |
|- ( A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) -> ( F e. Word A -> ( S e. ZZ -> ( G = ( F cyclShift S ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) |
93 |
92
|
adantl |
|- ( ( F : ( 0 ..^ ( # ` F ) ) --> A /\ A. x e. ( 0 ..^ ( # ` F ) ) A. y e. ( 0 ..^ ( # ` F ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) -> ( F e. Word A -> ( S e. ZZ -> ( G = ( F cyclShift S ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) |
94 |
10 93
|
sylbi |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A -> ( F e. Word A -> ( S e. ZZ -> ( G = ( F cyclShift S ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) |
95 |
94
|
3imp1 |
|- ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) |
96 |
9 95
|
jca |
|- ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ F e. Word A /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) |
97 |
96
|
3exp1 |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A -> ( F e. Word A -> ( S e. ZZ -> ( G = ( F cyclShift S ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) ) |
98 |
3 97
|
mpd |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A -> ( S e. ZZ -> ( G = ( F cyclShift S ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) ) ) |
99 |
98
|
3imp |
|- ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ S e. ZZ /\ G = ( F cyclShift S ) ) -> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) |
100 |
|
dff13 |
|- ( G : ( 0 ..^ ( # ` F ) ) -1-1-> A <-> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ A. i e. ( 0 ..^ ( # ` F ) ) A. j e. ( 0 ..^ ( # ` F ) ) ( ( G ` i ) = ( G ` j ) -> i = j ) ) ) |
101 |
99 100
|
sylibr |
|- ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ S e. ZZ /\ G = ( F cyclShift S ) ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> A ) |