Metamath Proof Explorer

Theorem crctcshwlkn0lem6

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 ) ) ) )
crctcshwlkn0lem.e 
|- ( ph -> ( P ` N ) = ( P ` 0 ) )
Assertion crctcshwlkn0lem6 
|- ( ( ph /\ J = ( 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 crctcshwlkn0lem.e 
 |-  ( ph -> ( P ` N ) = ( P ` 0 ) )
8 oveq1 
 |-  ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
9 0p1e1 
 |-  ( 0 + 1 ) = 1
10 8 9 eqtrdi 
 |-  ( i = 0 -> ( i + 1 ) = 1 )
11 wkslem2 
 |-  ( ( i = 0 /\ ( i + 1 ) = 1 ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
12 10 11 mpdan 
 |-  ( i = 0 -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
13 elfzo1 
 |-  ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) )
14 simp2 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> N e. NN )
15 13 14 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> N e. NN )
16 1 15 syl 
 |-  ( ph -> N e. NN )
17 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
18 16 17 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ N ) )
19 12 6 18 rspcdva 
 |-  ( ph -> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
20 eqeq1 
 |-  ( ( P ` N ) = ( P ` 0 ) -> ( ( P ` N ) = ( P ` 1 ) <-> ( P ` 0 ) = ( P ` 1 ) ) )
21 sneq 
 |-  ( ( P ` N ) = ( P ` 0 ) -> { ( P ` N ) } = { ( P ` 0 ) } )
22 21 eqeq2d 
 |-  ( ( P ` N ) = ( P ` 0 ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` N ) } <-> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } ) )
23 preq1 
 |-  ( ( P ` N ) = ( P ` 0 ) -> { ( P ` N ) , ( P ` 1 ) } = { ( P ` 0 ) , ( P ` 1 ) } )
24 23 sseq1d 
 |-  ( ( P ` N ) = ( P ` 0 ) -> ( { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) <-> { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
25 20 22 24 ifpbi123d 
 |-  ( ( P ` N ) = ( P ` 0 ) -> ( if- ( ( P ` N ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
26 7 25 syl 
 |-  ( ph -> ( if- ( ( P ` N ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
27 19 26 mpbird 
 |-  ( ph -> if- ( ( P ` N ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
28 nncn 
 |-  ( N e. NN -> N e. CC )
29 nncn 
 |-  ( S e. NN -> S e. CC )
30 npcan 
 |-  ( ( N e. CC /\ S e. CC ) -> ( ( N - S ) + S ) = N )
31 28 29 30 syl2anr 
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) + S ) = N )
32 simpr 
 |-  ( ( ( S e. NN /\ N e. NN ) /\ ( ( N - S ) + S ) = N ) -> ( ( N - S ) + S ) = N )
33 oveq1 
 |-  ( ( ( N - S ) + S ) = N -> ( ( ( N - S ) + S ) mod ( # ` F ) ) = ( N mod ( # ` F ) ) )
34 4 eqcomi 
 |-  ( # ` F ) = N
35 34 a1i 
 |-  ( ( S e. NN /\ N e. NN ) -> ( # ` F ) = N )
36 35 oveq2d 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N mod ( # ` F ) ) = ( N mod N ) )
37 nnrp 
 |-  ( N e. NN -> N e. RR+ )
38 modid0 
 |-  ( N e. RR+ -> ( N mod N ) = 0 )
39 37 38 syl 
 |-  ( N e. NN -> ( N mod N ) = 0 )
40 39 adantl 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N mod N ) = 0 )
41 36 40 eqtrd 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N mod ( # ` F ) ) = 0 )
42 33 41 sylan9eqr 
 |-  ( ( ( S e. NN /\ N e. NN ) /\ ( ( N - S ) + S ) = N ) -> ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 )
43 simpl 
 |-  ( ( ( S e. NN /\ N e. NN ) /\ ( ( N - S ) + S ) = N ) -> ( S e. NN /\ N e. NN ) )
44 32 42 43 3jca 
 |-  ( ( ( S e. NN /\ N e. NN ) /\ ( ( N - S ) + S ) = N ) -> ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) )
45 31 44 mpdan 
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) )
46 45 3adant3 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) )
47 13 46 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) )
48 simp1 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( ( N - S ) + S ) = N )
49 48 fveq2d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( P ` ( ( N - S ) + S ) ) = ( P ` N ) )
50 49 eqeq1d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) <-> ( P ` N ) = ( P ` 1 ) ) )
51 simp2 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 )
52 51 fveq2d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) = ( F ` 0 ) )
53 52 fveq2d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = ( I ` ( F ` 0 ) ) )
54 49 sneqd 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> { ( P ` ( ( N - S ) + S ) ) } = { ( P ` N ) } )
55 53 54 eqeq12d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } <-> ( I ` ( F ` 0 ) ) = { ( P ` N ) } ) )
56 49 preq1d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } = { ( P ` N ) , ( P ` 1 ) } )
57 56 53 sseq12d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) <-> { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
58 50 55 57 ifpbi123d 
 |-  ( ( ( ( N - S ) + S ) = N /\ ( ( ( N - S ) + S ) mod ( # ` F ) ) = 0 /\ ( S e. NN /\ N e. NN ) ) -> ( if- ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) , ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } , { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) <-> if- ( ( P ` N ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
59 1 47 58 3syl 
 |-  ( ph -> ( if- ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) , ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } , { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) <-> if- ( ( P ` N ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
60 27 59 mpbird 
 |-  ( ph -> if- ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) , ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } , { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) )
61 nnsub 
 |-  ( ( S e. NN /\ N e. NN ) -> ( S < N <-> ( N - S ) e. NN ) )
62 61 biimp3a 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN )
63 62 nnnn0d 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN0 )
64 13 63 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( N - S ) e. NN0 )
65 1 64 syl 
 |-  ( ph -> ( N - S ) e. NN0 )
66 nn0fz0 
 |-  ( ( N - S ) e. NN0 <-> ( N - S ) e. ( 0 ... ( N - S ) ) )
67 65 66 sylib 
 |-  ( ph -> ( N - S ) e. ( 0 ... ( N - S ) ) )
68 1 2 crctcshwlkn0lem2 
 |-  ( ( ph /\ ( N - S ) e. ( 0 ... ( N - S ) ) ) -> ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) )
69 67 68 mpdan 
 |-  ( ph -> ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) )
70 elfzoel2 
 |-  ( S e. ( 1 ..^ N ) -> N e. ZZ )
71 elfzoelz 
 |-  ( S e. ( 1 ..^ N ) -> S e. ZZ )
72 70 71 zsubcld 
 |-  ( S e. ( 1 ..^ N ) -> ( N - S ) e. ZZ )
73 72 peano2zd 
 |-  ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) e. ZZ )
74 nnre 
 |-  ( N e. NN -> N e. RR )
75 74 anim1i 
 |-  ( ( N e. NN /\ S e. NN ) -> ( N e. RR /\ S e. NN ) )
76 75 ancoms 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N e. RR /\ S e. NN ) )
77 crctcshwlkn0lem1 
 |-  ( ( N e. RR /\ S e. NN ) -> ( ( N - S ) + 1 ) <_ N )
78 76 77 syl 
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) + 1 ) <_ N )
79 78 3adant3 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) <_ N )
80 13 79 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) <_ N )
81 73 70 80 3jca 
 |-  ( S e. ( 1 ..^ N ) -> ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( N - S ) + 1 ) <_ N ) )
82 1 81 syl 
 |-  ( ph -> ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( N - S ) + 1 ) <_ N ) )
83 eluz2 
 |-  ( N e. ( ZZ>= ` ( ( N - S ) + 1 ) ) <-> ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( N - S ) + 1 ) <_ N ) )
84 82 83 sylibr 
 |-  ( ph -> N e. ( ZZ>= ` ( ( N - S ) + 1 ) ) )
85 eluzfz1 
 |-  ( N e. ( ZZ>= ` ( ( N - S ) + 1 ) ) -> ( ( N - S ) + 1 ) e. ( ( ( N - S ) + 1 ) ... N ) )
86 84 85 syl 
 |-  ( ph -> ( ( N - S ) + 1 ) e. ( ( ( N - S ) + 1 ) ... N ) )
87 1 2 crctcshwlkn0lem3 
 |-  ( ( ph /\ ( ( N - S ) + 1 ) e. ( ( ( N - S ) + 1 ) ... N ) ) -> ( Q ` ( ( N - S ) + 1 ) ) = ( P ` ( ( ( ( N - S ) + 1 ) + S ) - N ) ) )
88 86 87 mpdan 
 |-  ( ph -> ( Q ` ( ( N - S ) + 1 ) ) = ( P ` ( ( ( ( N - S ) + 1 ) + S ) - N ) ) )
89 subcl 
 |-  ( ( N e. CC /\ S e. CC ) -> ( N - S ) e. CC )
90 89 ancoms 
 |-  ( ( S e. CC /\ N e. CC ) -> ( N - S ) e. CC )
91 ax-1cn 
 |-  1 e. CC
92 pncan2 
 |-  ( ( ( N - S ) e. CC /\ 1 e. CC ) -> ( ( ( N - S ) + 1 ) - ( N - S ) ) = 1 )
93 92 eqcomd 
 |-  ( ( ( N - S ) e. CC /\ 1 e. CC ) -> 1 = ( ( ( N - S ) + 1 ) - ( N - S ) ) )
94 90 91 93 sylancl 
 |-  ( ( S e. CC /\ N e. CC ) -> 1 = ( ( ( N - S ) + 1 ) - ( N - S ) ) )
95 peano2cn 
 |-  ( ( N - S ) e. CC -> ( ( N - S ) + 1 ) e. CC )
96 90 95 syl 
 |-  ( ( S e. CC /\ N e. CC ) -> ( ( N - S ) + 1 ) e. CC )
97 simpr 
 |-  ( ( S e. CC /\ N e. CC ) -> N e. CC )
98 simpl 
 |-  ( ( S e. CC /\ N e. CC ) -> S e. CC )
99 96 97 98 subsub3d 
 |-  ( ( S e. CC /\ N e. CC ) -> ( ( ( N - S ) + 1 ) - ( N - S ) ) = ( ( ( ( N - S ) + 1 ) + S ) - N ) )
100 94 99 eqtr2d 
 |-  ( ( S e. CC /\ N e. CC ) -> ( ( ( ( N - S ) + 1 ) + S ) - N ) = 1 )
101 29 28 100 syl2an 
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( ( ( N - S ) + 1 ) + S ) - N ) = 1 )
102 101 3adant3 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( ( ( N - S ) + 1 ) + S ) - N ) = 1 )
103 13 102 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( ( ( ( N - S ) + 1 ) + S ) - N ) = 1 )
104 1 103 syl 
 |-  ( ph -> ( ( ( ( N - S ) + 1 ) + S ) - N ) = 1 )
105 104 fveq2d 
 |-  ( ph -> ( P ` ( ( ( ( N - S ) + 1 ) + S ) - N ) ) = ( P ` 1 ) )
106 88 105 eqtrd 
 |-  ( ph -> ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) )
107 3 fveq1i 
 |-  ( H ` ( N - S ) ) = ( ( F cyclShift S ) ` ( N - S ) )
108 5 adantr 
 |-  ( ( ph /\ S e. ( 1 ..^ N ) ) -> F e. Word A )
109 71 adantl 
 |-  ( ( ph /\ S e. ( 1 ..^ N ) ) -> S e. ZZ )
110 elfzofz 
 |-  ( S e. ( 1 ..^ N ) -> S e. ( 1 ... N ) )
111 ubmelfzo 
 |-  ( S e. ( 1 ... N ) -> ( N - S ) e. ( 0 ..^ N ) )
112 110 111 syl 
 |-  ( S e. ( 1 ..^ N ) -> ( N - S ) e. ( 0 ..^ N ) )
113 112 adantl 
 |-  ( ( ph /\ S e. ( 1 ..^ N ) ) -> ( N - S ) e. ( 0 ..^ N ) )
114 34 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N )
115 113 114 eleqtrrdi 
 |-  ( ( ph /\ S e. ( 1 ..^ N ) ) -> ( N - S ) e. ( 0 ..^ ( # ` F ) ) )
116 cshwidxmod 
 |-  ( ( F e. Word A /\ S e. ZZ /\ ( N - S ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) )
117 108 109 115 116 syl3anc 
 |-  ( ( ph /\ S e. ( 1 ..^ N ) ) -> ( ( F cyclShift S ) ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) )
118 1 117 mpdan 
 |-  ( ph -> ( ( F cyclShift S ) ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) )
119 107 118 eqtrid 
 |-  ( ph -> ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) )
120 simp1 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) )
121 simp2 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) )
122 120 121 eqeq12d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) <-> ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) ) )
123 simp3 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) )
124 123 fveq2d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( I ` ( H ` ( N - S ) ) ) = ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) )
125 120 sneqd 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> { ( Q ` ( N - S ) ) } = { ( P ` ( ( N - S ) + S ) ) } )
126 124 125 eqeq12d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } <-> ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } ) )
127 120 121 preq12d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } = { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } )
128 127 124 sseq12d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) <-> { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) )
129 122 126 128 ifpbi123d 
 |-  ( ( ( Q ` ( N - S ) ) = ( P ` ( ( N - S ) + S ) ) /\ ( Q ` ( ( N - S ) + 1 ) ) = ( P ` 1 ) /\ ( H ` ( N - S ) ) = ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) -> ( if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) <-> if- ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) , ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } , { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) ) )
130 69 106 119 129 syl3anc 
 |-  ( ph -> ( if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) <-> if- ( ( P ` ( ( N - S ) + S ) ) = ( P ` 1 ) , ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) = { ( P ` ( ( N - S ) + S ) ) } , { ( P ` ( ( N - S ) + S ) ) , ( P ` 1 ) } C_ ( I ` ( F ` ( ( ( N - S ) + S ) mod ( # ` F ) ) ) ) ) ) )
131 60 130 mpbird 
 |-  ( ph -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) )
132 131 adantr 
 |-  ( ( ph /\ J = ( N - S ) ) -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) )
133 wkslem1 
 |-  ( J = ( N - S ) -> ( if- ( ( Q ` J ) = ( Q ` ( J + 1 ) ) , ( I ` ( H ` J ) ) = { ( Q ` J ) } , { ( Q ` J ) , ( Q ` ( J + 1 ) ) } C_ ( I ` ( H ` J ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) )
134 133 adantl 
 |-  ( ( ph /\ J = ( N - S ) ) -> ( if- ( ( Q ` J ) = ( Q ` ( J + 1 ) ) , ( I ` ( H ` J ) ) = { ( Q ` J ) } , { ( Q ` J ) , ( Q ` ( J + 1 ) ) } C_ ( I ` ( H ` J ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) )
135 132 134 mpbird 
 |-  ( ( ph /\ J = ( N - S ) ) -> if- ( ( Q ` J ) = ( Q ` ( J + 1 ) ) , ( I ` ( H ` J ) ) = { ( Q ` J ) } , { ( Q ` J ) , ( Q ` ( J + 1 ) ) } C_ ( I ` ( H ` J ) ) ) )