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

Metamath Proof Explorer

Theorem cshf1

Description: Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021)

Ref Expression
Assertion cshf1 
|- ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ S e. ZZ /\ G = ( F cyclShift S ) ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> A )

Proof

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 )