Metamath Proof Explorer


Theorem scshwfzeqfzo

Description: For a nonempty word the sets of shifted words, expressd by a finite interval of integers or by a half-open integer range are identical. (Contributed by Alexander van der Vekens, 15-Jun-2018)

Ref Expression
Assertion scshwfzeqfzo X Word V X N = X y Word V | n 0 N y = X cyclShift n = y Word V | n 0 ..^ N y = X cyclShift n

Proof

Step Hyp Ref Expression
1 lencl X Word V X 0
2 elnn0uz X 0 X 0
3 1 2 sylib X Word V X 0
4 3 adantr X Word V N = X X 0
5 eleq1 N = X N 0 X 0
6 5 adantl X Word V N = X N 0 X 0
7 4 6 mpbird X Word V N = X N 0
8 7 3adant2 X Word V X N = X N 0
9 8 adantr X Word V X N = X y Word V N 0
10 fzisfzounsn N 0 0 N = 0 ..^ N N
11 9 10 syl X Word V X N = X y Word V 0 N = 0 ..^ N N
12 11 rexeqdv X Word V X N = X y Word V n 0 N y = X cyclShift n n 0 ..^ N N y = X cyclShift n
13 rexun n 0 ..^ N N y = X cyclShift n n 0 ..^ N y = X cyclShift n n N y = X cyclShift n
14 12 13 bitrdi X Word V X N = X y Word V n 0 N y = X cyclShift n n 0 ..^ N y = X cyclShift n n N y = X cyclShift n
15 fvex X V
16 eleq1 N = X N V X V
17 15 16 mpbiri N = X N V
18 oveq2 n = N X cyclShift n = X cyclShift N
19 18 eqeq2d n = N y = X cyclShift n y = X cyclShift N
20 19 rexsng N V n N y = X cyclShift n y = X cyclShift N
21 17 20 syl N = X n N y = X cyclShift n y = X cyclShift N
22 21 3ad2ant3 X Word V X N = X n N y = X cyclShift n y = X cyclShift N
23 22 adantr X Word V X N = X y Word V n N y = X cyclShift n y = X cyclShift N
24 oveq2 N = X X cyclShift N = X cyclShift X
25 24 3ad2ant3 X Word V X N = X X cyclShift N = X cyclShift X
26 cshwn X Word V X cyclShift X = X
27 26 3ad2ant1 X Word V X N = X X cyclShift X = X
28 25 27 eqtrd X Word V X N = X X cyclShift N = X
29 28 eqeq2d X Word V X N = X y = X cyclShift N y = X
30 29 adantr X Word V X N = X y Word V y = X cyclShift N y = X
31 cshw0 X Word V X cyclShift 0 = X
32 31 3ad2ant1 X Word V X N = X X cyclShift 0 = X
33 lennncl X Word V X X
34 33 3adant3 X Word V X N = X X
35 eleq1 N = X N X
36 35 3ad2ant3 X Word V X N = X N X
37 34 36 mpbird X Word V X N = X N
38 lbfzo0 0 0 ..^ N N
39 37 38 sylibr X Word V X N = X 0 0 ..^ N
40 oveq2 0 = n X cyclShift 0 = X cyclShift n
41 40 eqeq1d 0 = n X cyclShift 0 = X X cyclShift n = X
42 41 eqcoms n = 0 X cyclShift 0 = X X cyclShift n = X
43 eqcom X cyclShift n = X X = X cyclShift n
44 42 43 bitrdi n = 0 X cyclShift 0 = X X = X cyclShift n
45 44 adantl X Word V X N = X n = 0 X cyclShift 0 = X X = X cyclShift n
46 45 biimpd X Word V X N = X n = 0 X cyclShift 0 = X X = X cyclShift n
47 39 46 rspcimedv X Word V X N = X X cyclShift 0 = X n 0 ..^ N X = X cyclShift n
48 32 47 mpd X Word V X N = X n 0 ..^ N X = X cyclShift n
49 48 adantr X Word V X N = X y Word V n 0 ..^ N X = X cyclShift n
50 49 adantr X Word V X N = X y Word V y = X n 0 ..^ N X = X cyclShift n
51 eqeq1 y = X y = X cyclShift n X = X cyclShift n
52 51 adantl X Word V X N = X y Word V y = X y = X cyclShift n X = X cyclShift n
53 52 rexbidv X Word V X N = X y Word V y = X n 0 ..^ N y = X cyclShift n n 0 ..^ N X = X cyclShift n
54 50 53 mpbird X Word V X N = X y Word V y = X n 0 ..^ N y = X cyclShift n
55 54 ex X Word V X N = X y Word V y = X n 0 ..^ N y = X cyclShift n
56 30 55 sylbid X Word V X N = X y Word V y = X cyclShift N n 0 ..^ N y = X cyclShift n
57 23 56 sylbid X Word V X N = X y Word V n N y = X cyclShift n n 0 ..^ N y = X cyclShift n
58 57 com12 n N y = X cyclShift n X Word V X N = X y Word V n 0 ..^ N y = X cyclShift n
59 58 jao1i n 0 ..^ N y = X cyclShift n n N y = X cyclShift n X Word V X N = X y Word V n 0 ..^ N y = X cyclShift n
60 59 com12 X Word V X N = X y Word V n 0 ..^ N y = X cyclShift n n N y = X cyclShift n n 0 ..^ N y = X cyclShift n
61 14 60 sylbid X Word V X N = X y Word V n 0 N y = X cyclShift n n 0 ..^ N y = X cyclShift n
62 fzossfz 0 ..^ N 0 N
63 ssrexv 0 ..^ N 0 N n 0 ..^ N y = X cyclShift n n 0 N y = X cyclShift n
64 62 63 mp1i X Word V X N = X y Word V n 0 ..^ N y = X cyclShift n n 0 N y = X cyclShift n
65 61 64 impbid X Word V X N = X y Word V n 0 N y = X cyclShift n n 0 ..^ N y = X cyclShift n
66 65 rabbidva X Word V X N = X y Word V | n 0 N y = X cyclShift n = y Word V | n 0 ..^ N y = X cyclShift n