Metamath Proof Explorer

Theorem cshimadifsn

Description: The image of a cyclically shifted word under its domain without its left 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 cshimadifsn 
|- ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift J ) " ( 1 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 wrdfn 
 |-  ( F e. Word S -> F Fn ( 0 ..^ ( # ` F ) ) )
2 fnfun 
 |-  ( F Fn ( 0 ..^ ( # ` F ) ) -> Fun F )
3 1 2 syl 
 |-  ( F e. Word S -> Fun F )
4 3 3ad2ant1 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> Fun F )
5 wrddm 
 |-  ( F e. Word S -> dom F = ( 0 ..^ ( # ` F ) ) )
6 difssd 
 |-  ( ( dom F = ( 0 ..^ ( # ` F ) ) /\ N = ( # ` F ) ) -> ( ( 0 ..^ ( # ` F ) ) \ { J } ) C_ ( 0 ..^ ( # ` F ) ) )
7 oveq2 
 |-  ( N = ( # ` F ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
8 7 difeq1d 
 |-  ( N = ( # ` F ) -> ( ( 0 ..^ N ) \ { J } ) = ( ( 0 ..^ ( # ` F ) ) \ { J } ) )
9 8 adantl 
 |-  ( ( dom F = ( 0 ..^ ( # ` F ) ) /\ N = ( # ` F ) ) -> ( ( 0 ..^ N ) \ { J } ) = ( ( 0 ..^ ( # ` F ) ) \ { J } ) )
10 simpl 
 |-  ( ( dom F = ( 0 ..^ ( # ` F ) ) /\ N = ( # ` F ) ) -> dom F = ( 0 ..^ ( # ` F ) ) )
11 6 9 10 3sstr4d 
 |-  ( ( dom F = ( 0 ..^ ( # ` F ) ) /\ N = ( # ` F ) ) -> ( ( 0 ..^ N ) \ { J } ) C_ dom F )
12 11 a1d 
 |-  ( ( dom F = ( 0 ..^ ( # ` F ) ) /\ N = ( # ` F ) ) -> ( J e. ( 0 ..^ N ) -> ( ( 0 ..^ N ) \ { J } ) C_ dom F ) )
13 12 ex 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( N = ( # ` F ) -> ( J e. ( 0 ..^ N ) -> ( ( 0 ..^ N ) \ { J } ) C_ dom F ) ) )
14 5 13 syl 
 |-  ( F e. Word S -> ( N = ( # ` F ) -> ( J e. ( 0 ..^ N ) -> ( ( 0 ..^ N ) \ { J } ) C_ dom F ) ) )
15 14 3imp 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( 0 ..^ N ) \ { J } ) C_ dom F )
16 4 15 jca 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( Fun F /\ ( ( 0 ..^ N ) \ { J } ) C_ dom F ) )
17 dfimafn 
 |-  ( ( Fun F /\ ( ( 0 ..^ N ) \ { J } ) C_ dom F ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = { z | E. x e. ( ( 0 ..^ N ) \ { J } ) ( F ` x ) = z } )
18 16 17 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = { z | E. x e. ( ( 0 ..^ N ) \ { J } ) ( F ` x ) = z } )
19 modsumfzodifsn 
 |-  ( ( J e. ( 0 ..^ N ) /\ y e. ( 1 ..^ N ) ) -> ( ( y + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) )
20 19 3ad2antl3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> ( ( y + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) )
21 oveq2 
 |-  ( ( # ` F ) = N -> ( ( y + J ) mod ( # ` F ) ) = ( ( y + J ) mod N ) )
22 21 eqcoms 
 |-  ( N = ( # ` F ) -> ( ( y + J ) mod ( # ` F ) ) = ( ( y + J ) mod N ) )
23 22 eleq1d 
 |-  ( N = ( # ` F ) -> ( ( ( y + J ) mod ( # ` F ) ) e. ( ( 0 ..^ N ) \ { J } ) <-> ( ( y + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) ) )
24 23 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( ( y + J ) mod ( # ` F ) ) e. ( ( 0 ..^ N ) \ { J } ) <-> ( ( y + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) ) )
25 24 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> ( ( ( y + J ) mod ( # ` F ) ) e. ( ( 0 ..^ N ) \ { J } ) <-> ( ( y + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) ) )
26 20 25 mpbird 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> ( ( y + J ) mod ( # ` F ) ) e. ( ( 0 ..^ N ) \ { J } ) )
27 modfzo0difsn 
 |-  ( ( J e. ( 0 ..^ N ) /\ x e. ( ( 0 ..^ N ) \ { J } ) ) -> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod N ) )
28 27 3ad2antl3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( ( 0 ..^ N ) \ { J } ) ) -> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod N ) )
29 oveq2 
 |-  ( N = ( # ` F ) -> ( ( y + J ) mod N ) = ( ( y + J ) mod ( # ` F ) ) )
30 29 eqcomd 
 |-  ( N = ( # ` F ) -> ( ( y + J ) mod ( # ` F ) ) = ( ( y + J ) mod N ) )
31 30 eqeq2d 
 |-  ( N = ( # ` F ) -> ( x = ( ( y + J ) mod ( # ` F ) ) <-> x = ( ( y + J ) mod N ) ) )
32 31 rexbidv 
 |-  ( N = ( # ` F ) -> ( E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod ( # ` F ) ) <-> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod N ) ) )
33 32 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod ( # ` F ) ) <-> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod N ) ) )
34 33 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( ( 0 ..^ N ) \ { J } ) ) -> ( E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod ( # ` F ) ) <-> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod N ) ) )
35 28 34 mpbird 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ x e. ( ( 0 ..^ N ) \ { J } ) ) -> E. y e. ( 1 ..^ N ) x = ( ( y + J ) mod ( # ` F ) ) )
36 fveq2 
 |-  ( x = ( ( y + J ) mod ( # ` F ) ) -> ( F ` x ) = ( F ` ( ( y + J ) mod ( # ` F ) ) ) )
37 36 3ad2ant3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) /\ x = ( ( y + J ) mod ( # ` F ) ) ) -> ( F ` x ) = ( F ` ( ( y + J ) mod ( # ` F ) ) ) )
38 simpl1 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> F e. Word S )
39 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
40 39 3ad2ant3 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> J e. ZZ )
41 40 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> J e. ZZ )
42 oveq2 
 |-  ( N = ( # ` F ) -> ( 1 ..^ N ) = ( 1 ..^ ( # ` F ) ) )
43 42 eleq2d 
 |-  ( N = ( # ` F ) -> ( y e. ( 1 ..^ N ) <-> y e. ( 1 ..^ ( # ` F ) ) ) )
44 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
45 44 sseli 
 |-  ( y e. ( 1 ..^ ( # ` F ) ) -> y e. ( 0 ..^ ( # ` F ) ) )
46 43 45 syl6bi 
 |-  ( N = ( # ` F ) -> ( y e. ( 1 ..^ N ) -> y e. ( 0 ..^ ( # ` F ) ) ) )
47 46 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( y e. ( 1 ..^ N ) -> y e. ( 0 ..^ ( # ` F ) ) ) )
48 47 imp 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> y e. ( 0 ..^ ( # ` F ) ) )
49 cshwidxmod 
 |-  ( ( F e. Word S /\ J e. ZZ /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift J ) ` y ) = ( F ` ( ( y + J ) mod ( # ` F ) ) ) )
50 49 eqcomd 
 |-  ( ( F e. Word S /\ J e. ZZ /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( ( y + J ) mod ( # ` F ) ) ) = ( ( F cyclShift J ) ` y ) )
51 38 41 48 50 syl3anc 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) ) -> ( F ` ( ( y + J ) mod ( # ` F ) ) ) = ( ( F cyclShift J ) ` y ) )
52 51 3adant3 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) /\ x = ( ( y + J ) mod ( # ` F ) ) ) -> ( F ` ( ( y + J ) mod ( # ` F ) ) ) = ( ( F cyclShift J ) ` y ) )
53 37 52 eqtrd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) /\ x = ( ( y + J ) mod ( # ` F ) ) ) -> ( F ` x ) = ( ( F cyclShift J ) ` y ) )
54 53 eqeq1d 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ y e. ( 1 ..^ N ) /\ x = ( ( y + J ) mod ( # ` F ) ) ) -> ( ( F ` x ) = z <-> ( ( F cyclShift J ) ` y ) = z ) )
55 26 35 54 rexxfrd2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( E. x e. ( ( 0 ..^ N ) \ { J } ) ( F ` x ) = z <-> E. y e. ( 1 ..^ N ) ( ( F cyclShift J ) ` y ) = z ) )
56 55 abbidv 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> { z | E. x e. ( ( 0 ..^ N ) \ { J } ) ( F ` x ) = z } = { z | E. y e. ( 1 ..^ N ) ( ( F cyclShift J ) ` y ) = z } )
57 39 anim2i 
 |-  ( ( F e. Word S /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ J e. ZZ ) )
58 57 3adant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F e. Word S /\ J e. ZZ ) )
59 cshwfn 
 |-  ( ( F e. Word S /\ J e. ZZ ) -> ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) )
60 58 59 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) )
61 fnfun 
 |-  ( ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) -> Fun ( F cyclShift J ) )
62 61 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> Fun ( F cyclShift J ) )
63 42 44 eqsstrdi 
 |-  ( N = ( # ` F ) -> ( 1 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
64 63 3ad2ant2 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( 1 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
65 64 adantr 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 1 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
66 fndm 
 |-  ( ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) -> dom ( F cyclShift J ) = ( 0 ..^ ( # ` F ) ) )
67 66 adantl 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> dom ( F cyclShift J ) = ( 0 ..^ ( # ` F ) ) )
68 65 67 sseqtrrd 
 |-  ( ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) /\ ( F cyclShift J ) Fn ( 0 ..^ ( # ` F ) ) ) -> ( 1 ..^ N ) C_ dom ( F cyclShift J ) )
69 62 68 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 ) ) )
70 60 69 mpdan 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( Fun ( F cyclShift J ) /\ ( 1 ..^ N ) C_ dom ( F cyclShift J ) ) )
71 dfimafn 
 |-  ( ( Fun ( F cyclShift J ) /\ ( 1 ..^ N ) C_ dom ( F cyclShift J ) ) -> ( ( F cyclShift J ) " ( 1 ..^ N ) ) = { z | E. y e. ( 1 ..^ N ) ( ( F cyclShift J ) ` y ) = z } )
72 70 71 syl 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( ( F cyclShift J ) " ( 1 ..^ N ) ) = { z | E. y e. ( 1 ..^ N ) ( ( F cyclShift J ) ` y ) = z } )
73 56 72 eqtr4d 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> { z | E. x e. ( ( 0 ..^ N ) \ { J } ) ( F ` x ) = z } = ( ( F cyclShift J ) " ( 1 ..^ N ) ) )
74 18 73 eqtrd 
 |-  ( ( F e. Word S /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift J ) " ( 1 ..^ N ) ) )