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

Metamath Proof Explorer

Theorem cshimadifsn0

Description: The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021)

Ref Expression
Assertion cshimadifsn0 
|- ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 cshimadifsn 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift J ) " ( 1 ..^ N ) ) )
2 elfzoel2 
 |-  ( J e. ( 0 ..^ N ) -> N e. ZZ )
3 elfzom1elp1fzo1 
 |-  ( ( N e. ZZ /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + 1 ) e. ( 1 ..^ N ) )
4 3 ex 
 |-  ( N e. ZZ -> ( y e. ( 0 ..^ ( N - 1 ) ) -> ( y + 1 ) e. ( 1 ..^ N ) ) )
5 2 4 syl 
 |-  ( J e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ ( N - 1 ) ) -> ( y + 1 ) e. ( 1 ..^ N ) ) )
6 5 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( y e. ( 0 ..^ ( N - 1 ) ) -> ( y + 1 ) e. ( 1 ..^ N ) ) )
7 6 imp 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + 1 ) e. ( 1 ..^ N ) )
8 elfzo1elm1fzo0 
 |-  ( x e. ( 1 ..^ N ) -> ( x - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
9 8 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( 1 ..^ N ) ) -> ( x - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
10 oveq1 
 |-  ( y = ( x - 1 ) -> ( y + 1 ) = ( ( x - 1 ) + 1 ) )
11 10 eqeq2d 
 |-  ( y = ( x - 1 ) -> ( x = ( y + 1 ) <-> x = ( ( x - 1 ) + 1 ) ) )
12 11 adantl 
 |-  ( ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( 1 ..^ N ) ) /\ y = ( x - 1 ) ) -> ( x = ( y + 1 ) <-> x = ( ( x - 1 ) + 1 ) ) )
13 elfzoelz 
 |-  ( x e. ( 1 ..^ N ) -> x e. ZZ )
14 13 zcnd 
 |-  ( x e. ( 1 ..^ N ) -> x e. CC )
15 npcan1 
 |-  ( x e. CC -> ( ( x - 1 ) + 1 ) = x )
16 14 15 syl 
 |-  ( x e. ( 1 ..^ N ) -> ( ( x - 1 ) + 1 ) = x )
17 16 eqcomd 
 |-  ( x e. ( 1 ..^ N ) -> x = ( ( x - 1 ) + 1 ) )
18 17 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( 1 ..^ N ) ) -> x = ( ( x - 1 ) + 1 ) )
19 9 12 18 rspcedvd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( 1 ..^ N ) ) -> E. y e. ( 0 ..^ ( N - 1 ) ) x = ( y + 1 ) )
20 fveq2 
 |-  ( x = ( y + 1 ) -> ( ( F cyclShift J ) ` x ) = ( ( F cyclShift J ) ` ( y + 1 ) ) )
21 20 3ad2ant3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) /\ x = ( y + 1 ) ) -> ( ( F cyclShift J ) ` x ) = ( ( F cyclShift J ) ` ( y + 1 ) ) )
22 elfzoelz 
 |-  ( y e. ( 0 ..^ ( N - 1 ) ) -> y e. ZZ )
23 22 zcnd 
 |-  ( y e. ( 0 ..^ ( N - 1 ) ) -> y e. CC )
24 23 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> y e. CC )
25 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
26 25 zcnd 
 |-  ( J e. ( 0 ..^ N ) -> J e. CC )
27 26 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> J e. CC )
28 27 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> J e. CC )
29 1cnd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> 1 e. CC )
30 add32r 
 |-  ( ( y e. CC /\ J e. CC /\ 1 e. CC ) -> ( y + ( J + 1 ) ) = ( ( y + 1 ) + J ) )
31 24 28 29 30 syl3anc 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + ( J + 1 ) ) = ( ( y + 1 ) + J ) )
32 31 fvoveq1d 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( F ` ( ( y + ( J + 1 ) ) mod ( # ` F ) ) ) = ( F ` ( ( ( y + 1 ) + J ) mod ( # ` F ) ) ) )
33 simpl1 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> F e. Word S )
34 25 peano2zd 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ZZ )
35 34 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( J + 1 ) e. ZZ )
36 35 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( J + 1 ) e. ZZ )
37 fzossrbm1 
 |-  ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
38 2 37 syl 
 |-  ( J e. ( 0 ..^ N ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
39 38 sseld 
 |-  ( J e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ ( N - 1 ) ) -> y e. ( 0 ..^ N ) ) )
40 39 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( y e. ( 0 ..^ ( N - 1 ) ) -> y e. ( 0 ..^ N ) ) )
41 40 imp 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> y e. ( 0 ..^ N ) )
42 oveq2 
 |-  ( N = ( # ` F ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
43 42 eleq2d 
 |-  ( N = ( # ` F ) -> ( y e. ( 0 ..^ N ) <-> y e. ( 0 ..^ ( # ` F ) ) ) )
44 43 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( y e. ( 0 ..^ N ) <-> y e. ( 0 ..^ ( # ` F ) ) ) )
45 44 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y e. ( 0 ..^ N ) <-> y e. ( 0 ..^ ( # ` F ) ) ) )
46 41 45 mpbid 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> y e. ( 0 ..^ ( # ` F ) ) )
47 cshwidxmod 
 |-  ( ( F e. Word S /\ ( J + 1 ) e. ZZ /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift ( J + 1 ) ) ` y ) = ( F ` ( ( y + ( J + 1 ) ) mod ( # ` F ) ) ) )
48 33 36 46 47 syl3anc 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( F cyclShift ( J + 1 ) ) ` y ) = ( F ` ( ( y + ( J + 1 ) ) mod ( # ` F ) ) ) )
49 25 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> J e. ZZ )
50 49 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> J e. ZZ )
51 fzo0ss1 
 |-  ( 1 ..^ N ) C_ ( 0 ..^ N )
52 2 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> N e. ZZ )
53 52 3 sylan 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + 1 ) e. ( 1 ..^ N ) )
54 51 53 sselid 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + 1 ) e. ( 0 ..^ N ) )
55 42 eleq2d 
 |-  ( N = ( # ` F ) -> ( ( y + 1 ) e. ( 0 ..^ N ) <-> ( y + 1 ) e. ( 0 ..^ ( # ` F ) ) ) )
56 55 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( y + 1 ) e. ( 0 ..^ N ) <-> ( y + 1 ) e. ( 0 ..^ ( # ` F ) ) ) )
57 56 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( y + 1 ) e. ( 0 ..^ N ) <-> ( y + 1 ) e. ( 0 ..^ ( # ` F ) ) ) )
58 54 57 mpbid 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( y + 1 ) e. ( 0 ..^ ( # ` F ) ) )
59 cshwidxmod 
 |-  ( ( F e. Word S /\ J e. ZZ /\ ( y + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift J ) ` ( y + 1 ) ) = ( F ` ( ( ( y + 1 ) + J ) mod ( # ` F ) ) ) )
60 33 50 58 59 syl3anc 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( F cyclShift J ) ` ( y + 1 ) ) = ( F ` ( ( ( y + 1 ) + J ) mod ( # ` F ) ) ) )
61 32 48 60 3eqtr4rd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( F cyclShift J ) ` ( y + 1 ) ) = ( ( F cyclShift ( J + 1 ) ) ` y ) )
62 61 3adant3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) /\ x = ( y + 1 ) ) -> ( ( F cyclShift J ) ` ( y + 1 ) ) = ( ( F cyclShift ( J + 1 ) ) ` y ) )
63 21 62 eqtrd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) /\ x = ( y + 1 ) ) -> ( ( F cyclShift J ) ` x ) = ( ( F cyclShift ( J + 1 ) ) ` y ) )
64 63 eqeq1d 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 0 ..^ ( N - 1 ) ) /\ x = ( y + 1 ) ) -> ( ( ( F cyclShift J ) ` x ) = z <-> ( ( F cyclShift ( J + 1 ) ) ` y ) = z ) )
65 7 19 64 rexxfrd2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( E. x e. ( 1 ..^ N ) ( ( F cyclShift J ) ` x ) = z <-> E. y e. ( 0 ..^ ( N - 1 ) ) ( ( F cyclShift ( J + 1 ) ) ` y ) = z ) )
66 65 abbidv 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> { z | E. x e. ( 1 ..^ N ) ( ( F cyclShift J ) ` x ) = z } = { z | E. y e. ( 0 ..^ ( N - 1 ) ) ( ( F cyclShift ( J + 1 ) ) ` y ) = z } )
67 25 anim2i 
 |-  ( ( F e. Word S /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ J e. ZZ ) )
68 67 3adant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ J e. ZZ ) )
69 cshwfn 
 |-  ( ( F e. Word S /\ J e. ZZ ) -> ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) )
70 68 69 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) )
71 fnfun 
 |-  ( ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) -> Fun ( F cyclShift J ) )
72 71 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> Fun ( F cyclShift J ) )
73 42 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
74 51 73 sseqtrid 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 1 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
75 74 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 1 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
76 fndm 
 |-  ( ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) -> dom ( F cyclShift J ) = ( 0 ..^ ( # ` F ) ) )
77 76 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> dom ( F cyclShift J ) = ( 0 ..^ ( # ` F ) ) )
78 75 77 sseqtrrd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 1 ..^ N ) C_ dom ( F cyclShift J ) )
79 72 78 jca 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( Fun ( F cyclShift J ) /\ ( 1 ..^ N ) C_ dom ( F cyclShift J ) ) )
80 70 79 mpdan 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( Fun ( F cyclShift J ) /\ ( 1 ..^ N ) C_ dom ( F cyclShift J ) ) )
81 dfimafn 
 |-  ( ( Fun ( F cyclShift J ) /\ ( 1 ..^ N ) C_ dom ( F cyclShift J ) ) -> ( ( F cyclShift J ) " ( 1 ..^ N ) ) = { z | E. x e. ( 1 ..^ N ) ( ( F cyclShift J ) ` x ) = z } )
82 80 81 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( F cyclShift J ) " ( 1 ..^ N ) ) = { z | E. x e. ( 1 ..^ N ) ( ( F cyclShift J ) ` x ) = z } )
83 34 anim2i 
 |-  ( ( F e. Word S /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ ( J + 1 ) e. ZZ ) )
84 83 3adant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ ( J + 1 ) e. ZZ ) )
85 cshwfn 
 |-  ( ( F e. Word S /\ ( J + 1 ) e. ZZ ) -> ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) )
86 84 85 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) )
87 fnfun 
 |-  ( ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) -> Fun ( F cyclShift ( J + 1 ) ) )
88 87 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) ) -> Fun ( F cyclShift ( J + 1 ) ) )
89 38 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
90 oveq2 
 |-  ( ( # ` F ) = N -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
91 90 eqcoms 
 |-  ( N = ( # ` F ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
92 91 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
93 89 92 sseqtrrd 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
94 93 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
95 fndm 
 |-  ( ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) -> dom ( F cyclShift ( J + 1 ) ) = ( 0 ..^ ( # ` F ) ) )
96 95 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) ) -> dom ( F cyclShift ( J + 1 ) ) = ( 0 ..^ ( # ` F ) ) )
97 94 96 sseqtrrd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ dom ( F cyclShift ( J + 1 ) ) )
98 88 97 jca 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift ( J + 1 ) ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( Fun ( F cyclShift ( J + 1 ) ) /\ ( 0 ..^ ( N - 1 ) ) C_ dom ( F cyclShift ( J + 1 ) ) ) )
99 86 98 mpdan 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( Fun ( F cyclShift ( J + 1 ) ) /\ ( 0 ..^ ( N - 1 ) ) C_ dom ( F cyclShift ( J + 1 ) ) ) )
100 dfimafn 
 |-  ( ( Fun ( F cyclShift ( J + 1 ) ) /\ ( 0 ..^ ( N - 1 ) ) C_ dom ( F cyclShift ( J + 1 ) ) ) -> ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) = { z | E. y e. ( 0 ..^ ( N - 1 ) ) ( ( F cyclShift ( J + 1 ) ) ` y ) = z } )
101 99 100 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) = { z | E. y e. ( 0 ..^ ( N - 1 ) ) ( ( F cyclShift ( J + 1 ) ) ` y ) = z } )
102 66 82 101 3eqtr4d 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( F cyclShift J ) " ( 1 ..^ N ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )
103 1 102 eqtrd 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )