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 )