Metamath Proof Explorer


Theorem crctcshwlkn0lem4

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s
|- ( ph -> S e. ( 1 ..^ N ) )
crctcshwlkn0lem.q
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
crctcshwlkn0lem.h
|- H = ( F cyclShift S )
crctcshwlkn0lem.n
|- N = ( # ` F )
crctcshwlkn0lem.f
|- ( ph -> F e. Word A )
crctcshwlkn0lem.p
|- ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
Assertion crctcshwlkn0lem4
|- ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s
 |-  ( ph -> S e. ( 1 ..^ N ) )
2 crctcshwlkn0lem.q
 |-  Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
3 crctcshwlkn0lem.h
 |-  H = ( F cyclShift S )
4 crctcshwlkn0lem.n
 |-  N = ( # ` F )
5 crctcshwlkn0lem.f
 |-  ( ph -> F e. Word A )
6 crctcshwlkn0lem.p
 |-  ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
7 elfzoelz
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> j e. ZZ )
8 7 zcnd
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> j e. CC )
9 8 adantl
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. CC )
10 elfzoelz
 |-  ( S e. ( 1 ..^ N ) -> S e. ZZ )
11 10 zcnd
 |-  ( S e. ( 1 ..^ N ) -> S e. CC )
12 11 adantr
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> S e. CC )
13 1cnd
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> 1 e. CC )
14 9 12 13 add32d
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) )
15 elfzo1
 |-  ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) )
16 elfzonn0
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> j e. NN0 )
17 nnnn0
 |-  ( S e. NN -> S e. NN0 )
18 nn0addcl
 |-  ( ( j e. NN0 /\ S e. NN0 ) -> ( j + S ) e. NN0 )
19 18 ex
 |-  ( j e. NN0 -> ( S e. NN0 -> ( j + S ) e. NN0 ) )
20 16 17 19 syl2imc
 |-  ( S e. NN -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) )
21 20 3ad2ant1
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) )
22 15 21 sylbi
 |-  ( S e. ( 1 ..^ N ) -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) )
23 22 imp
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. NN0 )
24 fzo0ss1
 |-  ( 1 ..^ N ) C_ ( 0 ..^ N )
25 24 sseli
 |-  ( S e. ( 1 ..^ N ) -> S e. ( 0 ..^ N ) )
26 elfzo0
 |-  ( S e. ( 0 ..^ N ) <-> ( S e. NN0 /\ N e. NN /\ S < N ) )
27 26 simp2bi
 |-  ( S e. ( 0 ..^ N ) -> N e. NN )
28 25 27 syl
 |-  ( S e. ( 1 ..^ N ) -> N e. NN )
29 28 adantr
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> N e. NN )
30 elfzo0
 |-  ( j e. ( 0 ..^ ( N - S ) ) <-> ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) )
31 nn0re
 |-  ( j e. NN0 -> j e. RR )
32 nnre
 |-  ( S e. NN -> S e. RR )
33 nnre
 |-  ( N e. NN -> N e. RR )
34 32 33 anim12i
 |-  ( ( S e. NN /\ N e. NN ) -> ( S e. RR /\ N e. RR ) )
35 34 3adant3
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( S e. RR /\ N e. RR ) )
36 15 35 sylbi
 |-  ( S e. ( 1 ..^ N ) -> ( S e. RR /\ N e. RR ) )
37 31 36 anim12i
 |-  ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) )
38 3anass
 |-  ( ( j e. RR /\ S e. RR /\ N e. RR ) <-> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) )
39 37 38 sylibr
 |-  ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j e. RR /\ S e. RR /\ N e. RR ) )
40 ltaddsub
 |-  ( ( j e. RR /\ S e. RR /\ N e. RR ) -> ( ( j + S ) < N <-> j < ( N - S ) ) )
41 40 bicomd
 |-  ( ( j e. RR /\ S e. RR /\ N e. RR ) -> ( j < ( N - S ) <-> ( j + S ) < N ) )
42 39 41 syl
 |-  ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j < ( N - S ) <-> ( j + S ) < N ) )
43 42 biimpd
 |-  ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j < ( N - S ) -> ( j + S ) < N ) )
44 43 ex
 |-  ( j e. NN0 -> ( S e. ( 1 ..^ N ) -> ( j < ( N - S ) -> ( j + S ) < N ) ) )
45 44 com23
 |-  ( j e. NN0 -> ( j < ( N - S ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) )
46 45 a1d
 |-  ( j e. NN0 -> ( ( N - S ) e. NN -> ( j < ( N - S ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) ) )
47 46 3imp
 |-  ( ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) )
48 30 47 sylbi
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) )
49 48 impcom
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) < N )
50 elfzo0
 |-  ( ( j + S ) e. ( 0 ..^ N ) <-> ( ( j + S ) e. NN0 /\ N e. NN /\ ( j + S ) < N ) )
51 23 29 49 50 syl3anbrc
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ( 0 ..^ N ) )
52 51 adantr
 |-  ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( j + S ) e. ( 0 ..^ N ) )
53 fveq2
 |-  ( i = ( j + S ) -> ( P ` i ) = ( P ` ( j + S ) ) )
54 53 adantl
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( P ` i ) = ( P ` ( j + S ) ) )
55 fvoveq1
 |-  ( i = ( j + S ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( j + S ) + 1 ) ) )
56 simpr
 |-  ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) )
57 56 fveq2d
 |-  ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( P ` ( ( j + S ) + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) )
58 55 57 sylan9eqr
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) )
59 54 58 eqeq12d
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( ( P ` i ) = ( P ` ( i + 1 ) ) <-> ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) ) )
60 2fveq3
 |-  ( i = ( j + S ) -> ( I ` ( F ` i ) ) = ( I ` ( F ` ( j + S ) ) ) )
61 53 sneqd
 |-  ( i = ( j + S ) -> { ( P ` i ) } = { ( P ` ( j + S ) ) } )
62 60 61 eqeq12d
 |-  ( i = ( j + S ) -> ( ( I ` ( F ` i ) ) = { ( P ` i ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) )
63 62 adantl
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( ( I ` ( F ` i ) ) = { ( P ` i ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) )
64 54 58 preq12d
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } )
65 60 adantl
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( I ` ( F ` i ) ) = ( I ` ( F ` ( j + S ) ) ) )
66 64 65 sseq12d
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) <-> { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) )
67 59 63 66 ifpbi123d
 |-  ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
68 52 67 rspcdv
 |-  ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
69 14 68 mpdan
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
70 1 69 sylan
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
71 70 ex
 |-  ( ph -> ( j e. ( 0 ..^ ( N - S ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) )
72 6 71 mpid
 |-  ( ph -> ( j e. ( 0 ..^ ( N - S ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
73 72 imp
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) )
74 elfzofz
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> j e. ( 0 ... ( N - S ) ) )
75 1 2 crctcshwlkn0lem2
 |-  ( ( ph /\ j e. ( 0 ... ( N - S ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) )
76 74 75 sylan2
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) )
77 fzofzp1
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> ( j + 1 ) e. ( 0 ... ( N - S ) ) )
78 1 2 crctcshwlkn0lem2
 |-  ( ( ph /\ ( j + 1 ) e. ( 0 ... ( N - S ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) )
79 77 78 sylan2
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) )
80 3 fveq1i
 |-  ( H ` j ) = ( ( F cyclShift S ) ` j )
81 5 adantr
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> F e. Word A )
82 1 10 syl
 |-  ( ph -> S e. ZZ )
83 82 adantr
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> S e. ZZ )
84 nnz
 |-  ( N e. NN -> N e. ZZ )
85 84 adantl
 |-  ( ( S e. NN /\ N e. NN ) -> N e. ZZ )
86 nnz
 |-  ( S e. NN -> S e. ZZ )
87 86 adantr
 |-  ( ( S e. NN /\ N e. NN ) -> S e. ZZ )
88 85 87 zsubcld
 |-  ( ( S e. NN /\ N e. NN ) -> ( N - S ) e. ZZ )
89 17 nn0ge0d
 |-  ( S e. NN -> 0 <_ S )
90 89 adantr
 |-  ( ( S e. NN /\ N e. NN ) -> 0 <_ S )
91 subge02
 |-  ( ( N e. RR /\ S e. RR ) -> ( 0 <_ S <-> ( N - S ) <_ N ) )
92 33 32 91 syl2anr
 |-  ( ( S e. NN /\ N e. NN ) -> ( 0 <_ S <-> ( N - S ) <_ N ) )
93 90 92 mpbid
 |-  ( ( S e. NN /\ N e. NN ) -> ( N - S ) <_ N )
94 88 85 93 3jca
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) )
95 94 3adant3
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) )
96 15 95 sylbi
 |-  ( S e. ( 1 ..^ N ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) )
97 eluz2
 |-  ( N e. ( ZZ>= ` ( N - S ) ) <-> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) )
98 96 97 sylibr
 |-  ( S e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( N - S ) ) )
99 fzoss2
 |-  ( N e. ( ZZ>= ` ( N - S ) ) -> ( 0 ..^ ( N - S ) ) C_ ( 0 ..^ N ) )
100 1 98 99 3syl
 |-  ( ph -> ( 0 ..^ ( N - S ) ) C_ ( 0 ..^ N ) )
101 100 sselda
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. ( 0 ..^ N ) )
102 4 oveq2i
 |-  ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) )
103 101 102 eleqtrdi
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. ( 0 ..^ ( # ` F ) ) )
104 cshwidxmod
 |-  ( ( F e. Word A /\ S e. ZZ /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) )
105 81 83 103 104 syl3anc
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) )
106 4 eqcomi
 |-  ( # ` F ) = N
107 106 oveq2i
 |-  ( ( j + S ) mod ( # ` F ) ) = ( ( j + S ) mod N )
108 21 imp
 |-  ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. NN0 )
109 nnm1nn0
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
110 109 3ad2ant2
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - 1 ) e. NN0 )
111 110 adantr
 |-  ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( N - 1 ) e. NN0 )
112 31 35 anim12i
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) )
113 112 38 sylibr
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j e. RR /\ S e. RR /\ N e. RR ) )
114 113 41 syl
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j < ( N - S ) <-> ( j + S ) < N ) )
115 17 3ad2ant1
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> S e. NN0 )
116 115 18 sylan2
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j + S ) e. NN0 )
117 116 nn0zd
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j + S ) e. ZZ )
118 84 3ad2ant2
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> N e. ZZ )
119 118 adantl
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> N e. ZZ )
120 zltlem1
 |-  ( ( ( j + S ) e. ZZ /\ N e. ZZ ) -> ( ( j + S ) < N <-> ( j + S ) <_ ( N - 1 ) ) )
121 117 119 120 syl2anc
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( ( j + S ) < N <-> ( j + S ) <_ ( N - 1 ) ) )
122 121 biimpd
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( ( j + S ) < N -> ( j + S ) <_ ( N - 1 ) ) )
123 114 122 sylbid
 |-  ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j < ( N - S ) -> ( j + S ) <_ ( N - 1 ) ) )
124 123 impancom
 |-  ( ( j e. NN0 /\ j < ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) )
125 124 3adant2
 |-  ( ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) )
126 30 125 sylbi
 |-  ( j e. ( 0 ..^ ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) )
127 126 impcom
 |-  ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) <_ ( N - 1 ) )
128 108 111 127 3jca
 |-  ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) )
129 15 128 sylanb
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) )
130 elfz2nn0
 |-  ( ( j + S ) e. ( 0 ... ( N - 1 ) ) <-> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) )
131 129 130 sylibr
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ( 0 ... ( N - 1 ) ) )
132 zaddcl
 |-  ( ( j e. ZZ /\ S e. ZZ ) -> ( j + S ) e. ZZ )
133 7 10 132 syl2anr
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ZZ )
134 zmodid2
 |-  ( ( ( j + S ) e. ZZ /\ N e. NN ) -> ( ( ( j + S ) mod N ) = ( j + S ) <-> ( j + S ) e. ( 0 ... ( N - 1 ) ) ) )
135 133 29 134 syl2anc
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( ( j + S ) mod N ) = ( j + S ) <-> ( j + S ) e. ( 0 ... ( N - 1 ) ) ) )
136 131 135 mpbird
 |-  ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod N ) = ( j + S ) )
137 1 136 sylan
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod N ) = ( j + S ) )
138 107 137 syl5eq
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod ( # ` F ) ) = ( j + S ) )
139 138 fveq2d
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( F ` ( ( j + S ) mod ( # ` F ) ) ) = ( F ` ( j + S ) ) )
140 105 139 eqtrd
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( j + S ) ) )
141 80 140 syl5eq
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( H ` j ) = ( F ` ( j + S ) ) )
142 141 fveq2d
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) )
143 simp1
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) )
144 simp2
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) )
145 143 144 eqeq12d
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( ( Q ` j ) = ( Q ` ( j + 1 ) ) <-> ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) ) )
146 simp3
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) )
147 143 sneqd
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> { ( Q ` j ) } = { ( P ` ( j + S ) ) } )
148 146 147 eqeq12d
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( ( I ` ( H ` j ) ) = { ( Q ` j ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) )
149 143 144 preq12d
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> { ( Q ` j ) , ( Q ` ( j + 1 ) ) } = { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } )
150 149 146 sseq12d
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) <-> { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) )
151 145 148 150 ifpbi123d
 |-  ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
152 76 79 142 151 syl3anc
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) )
153 73 152 mpbird
 |-  ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
154 153 ralrimiva
 |-  ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )