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 syl5eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑆 ) ) ) → ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( 𝑗 + 𝑆 ) )
139 138 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑆 ) ) ) → ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( 𝑗 + 𝑆 ) ) )
140 105 139 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑆 ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝑗 + 𝑆 ) ) )
141 80 140 syl5eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )