Metamath Proof Explorer

Theorem crctcshwlkn0lem4

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

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊒ ( πœ‘ β†’ 𝑆 ∈ ( 1 ..^ 𝑁 ) )
crctcshwlkn0lem.q ⊒ 𝑄 = ( π‘₯ ∈ ( 0 ... 𝑁 ) ↦ if ( π‘₯ ≀ ( 𝑁 βˆ’ 𝑆 ) , ( 𝑃 β€˜ ( π‘₯ + 𝑆 ) ) , ( 𝑃 β€˜ ( ( π‘₯ + 𝑆 ) βˆ’ 𝑁 ) ) ) )
crctcshwlkn0lem.h ⊒ 𝐻 = ( 𝐹 cyclShift 𝑆 )
crctcshwlkn0lem.n ⊒ 𝑁 = ( β™― β€˜ 𝐹 )
crctcshwlkn0lem.f ⊒ ( πœ‘ β†’ 𝐹 ∈ Word 𝐴 )
crctcshwlkn0lem.p ⊒ ( πœ‘ β†’ βˆ€ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 β€˜ 𝑖 ) = ( 𝑃 β€˜ ( 𝑖 + 1 ) ) , ( 𝐼 β€˜ ( 𝐹 β€˜ 𝑖 ) ) = { ( 𝑃 β€˜ 𝑖 ) } , { ( 𝑃 β€˜ 𝑖 ) , ( 𝑃 β€˜ ( 𝑖 + 1 ) ) } βŠ† ( 𝐼 β€˜ ( 𝐹 β€˜ 𝑖 ) ) ) )
Assertion crctcshwlkn0lem4 ( πœ‘ β†’ βˆ€ 𝑗 ∈ ( 0 ..^ ( 𝑁 βˆ’ 𝑆 ) ) if- ( ( 𝑄 β€˜ 𝑗 ) = ( 𝑄 β€˜ ( 𝑗 + 1 ) ) , ( 𝐼 β€˜ ( 𝐻 β€˜ 𝑗 ) ) = { ( 𝑄 β€˜ 𝑗 ) } , { ( 𝑄 β€˜ 𝑗 ) , ( 𝑄 β€˜ ( 𝑗 + 1 ) ) } βŠ† ( 𝐼 β€˜ ( 𝐻 β€˜ 𝑗 ) ) ) )

Proof

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