MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  crctcshwlkn0lem4 Structured version   Visualization version   GIF version

Theorem crctcshwlkn0lem4 26686
Description: Lemma for crctcshwlkn0 26694. (Contributed by AV, 12-Mar-2021.)
Hypotheses
Ref Expression
crctcshwlkn0lem.s (𝜑𝑆 ∈ (1..^𝑁))
crctcshwlkn0lem.q 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
crctcshwlkn0lem.h 𝐻 = (𝐹 cyclShift 𝑆)
crctcshwlkn0lem.n 𝑁 = (#‘𝐹)
crctcshwlkn0lem.f (𝜑𝐹 ∈ Word 𝐴)
crctcshwlkn0lem.p (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))))
Assertion
Ref Expression
crctcshwlkn0lem4 (𝜑 → ∀𝑗 ∈ (0..^(𝑁𝑆))if-((𝑄𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻𝑗)) = {(𝑄𝑗)}, {(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗))))
Distinct variable groups:   𝑥,𝑁   𝑥,𝑃   𝑥,𝑆   𝜑,𝑥   𝑖,𝐹   𝑖,𝐼   𝑖,𝑁   𝑃,𝑖   𝑆,𝑖   𝜑,𝑖,𝑗   𝑥,𝑗
Allowed substitution hints:   𝐴(𝑥,𝑖,𝑗)   𝑃(𝑗)   𝑄(𝑥,𝑖,𝑗)   𝑆(𝑗)   𝐹(𝑥,𝑗)   𝐻(𝑥,𝑖,𝑗)   𝐼(𝑥,𝑗)   𝑁(𝑗)

Proof of Theorem crctcshwlkn0lem4
StepHypRef Expression
1 crctcshwlkn0lem.p . . . . 5 (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))))
2 crctcshwlkn0lem.s . . . . . . 7 (𝜑𝑆 ∈ (1..^𝑁))
3 elfzoelz 12454 . . . . . . . . . . 11 (𝑗 ∈ (0..^(𝑁𝑆)) → 𝑗 ∈ ℤ)
43zcnd 11468 . . . . . . . . . 10 (𝑗 ∈ (0..^(𝑁𝑆)) → 𝑗 ∈ ℂ)
54adantl 482 . . . . . . . . 9 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → 𝑗 ∈ ℂ)
6 elfzoelz 12454 . . . . . . . . . . 11 (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
76zcnd 11468 . . . . . . . . . 10 (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℂ)
87adantr 481 . . . . . . . . 9 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → 𝑆 ∈ ℂ)
9 1cnd 10041 . . . . . . . . 9 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → 1 ∈ ℂ)
105, 8, 9add32d 10248 . . . . . . . 8 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆))
11 elfzo1 12501 . . . . . . . . . . . . 13 (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
12 nnnn0 11284 . . . . . . . . . . . . . . 15 (𝑆 ∈ ℕ → 𝑆 ∈ ℕ0)
13 elfzonn0 12496 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^(𝑁𝑆)) → 𝑗 ∈ ℕ0)
14 nn0addcl 11313 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ0𝑆 ∈ ℕ0) → (𝑗 + 𝑆) ∈ ℕ0)
1514ex 450 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (𝑆 ∈ ℕ0 → (𝑗 + 𝑆) ∈ ℕ0))
1613, 15syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑆 ∈ ℕ0 → (𝑗 + 𝑆) ∈ ℕ0))
1712, 16syl5com 31 . . . . . . . . . . . . . 14 (𝑆 ∈ ℕ → (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑗 + 𝑆) ∈ ℕ0))
18173ad2ant1 1080 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑗 + 𝑆) ∈ ℕ0))
1911, 18sylbi 207 . . . . . . . . . . . 12 (𝑆 ∈ (1..^𝑁) → (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑗 + 𝑆) ∈ ℕ0))
2019imp 445 . . . . . . . . . . 11 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ∈ ℕ0)
21 fzo0ss1 12482 . . . . . . . . . . . . . 14 (1..^𝑁) ⊆ (0..^𝑁)
2221sseli 3591 . . . . . . . . . . . . 13 (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (0..^𝑁))
23 elfzo0 12492 . . . . . . . . . . . . . 14 (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
2423simp2bi 1075 . . . . . . . . . . . . 13 (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
2522, 24syl 17 . . . . . . . . . . . 12 (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
2625adantr 481 . . . . . . . . . . 11 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → 𝑁 ∈ ℕ)
27 elfzo0 12492 . . . . . . . . . . . . 13 (𝑗 ∈ (0..^(𝑁𝑆)) ↔ (𝑗 ∈ ℕ0 ∧ (𝑁𝑆) ∈ ℕ ∧ 𝑗 < (𝑁𝑆)))
28 nn0re 11286 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
29 nnre 11012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 ∈ ℕ → 𝑆 ∈ ℝ)
30 nnre 11012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
3129, 30anim12i 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))
32313adant3 1079 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))
3311, 32sylbi 207 . . . . . . . . . . . . . . . . . . . . 21 (𝑆 ∈ (1..^𝑁) → (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))
3428, 33anim12i 589 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ℕ0𝑆 ∈ (1..^𝑁)) → (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
35 3anass 1040 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ↔ (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
3634, 35sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ0𝑆 ∈ (1..^𝑁)) → (𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))
37 ltaddsub 10487 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑗 + 𝑆) < 𝑁𝑗 < (𝑁𝑆)))
3837bicomd 213 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑗 < (𝑁𝑆) ↔ (𝑗 + 𝑆) < 𝑁))
3936, 38syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ0𝑆 ∈ (1..^𝑁)) → (𝑗 < (𝑁𝑆) ↔ (𝑗 + 𝑆) < 𝑁))
4039biimpd 219 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ0𝑆 ∈ (1..^𝑁)) → (𝑗 < (𝑁𝑆) → (𝑗 + 𝑆) < 𝑁))
4140ex 450 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (𝑆 ∈ (1..^𝑁) → (𝑗 < (𝑁𝑆) → (𝑗 + 𝑆) < 𝑁)))
4241com23 86 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → (𝑗 < (𝑁𝑆) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁)))
4342a1d 25 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → ((𝑁𝑆) ∈ ℕ → (𝑗 < (𝑁𝑆) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁))))
44433imp 1254 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ0 ∧ (𝑁𝑆) ∈ ℕ ∧ 𝑗 < (𝑁𝑆)) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁))
4527, 44sylbi 207 . . . . . . . . . . . 12 (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁))
4645impcom 446 . . . . . . . . . . 11 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) < 𝑁)
47 elfzo0 12492 . . . . . . . . . . 11 ((𝑗 + 𝑆) ∈ (0..^𝑁) ↔ ((𝑗 + 𝑆) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝑗 + 𝑆) < 𝑁))
4820, 26, 46, 47syl3anbrc 1244 . . . . . . . . . 10 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ∈ (0..^𝑁))
4948adantr 481 . . . . . . . . 9 (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (𝑗 + 𝑆) ∈ (0..^𝑁))
50 fveq2 6178 . . . . . . . . . . . 12 (𝑖 = (𝑗 + 𝑆) → (𝑃𝑖) = (𝑃‘(𝑗 + 𝑆)))
5150adantl 482 . . . . . . . . . . 11 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝑃𝑖) = (𝑃‘(𝑗 + 𝑆)))
52 oveq1 6642 . . . . . . . . . . . . 13 (𝑖 = (𝑗 + 𝑆) → (𝑖 + 1) = ((𝑗 + 𝑆) + 1))
5352fveq2d 6182 . . . . . . . . . . . 12 (𝑖 = (𝑗 + 𝑆) → (𝑃‘(𝑖 + 1)) = (𝑃‘((𝑗 + 𝑆) + 1)))
54 simpr 477 . . . . . . . . . . . . 13 (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆))
5554fveq2d 6182 . . . . . . . . . . . 12 (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (𝑃‘((𝑗 + 𝑆) + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)))
5653, 55sylan9eqr 2676 . . . . . . . . . . 11 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝑃‘(𝑖 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)))
5751, 56eqeq12d 2635 . . . . . . . . . 10 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ((𝑃𝑖) = (𝑃‘(𝑖 + 1)) ↔ (𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆))))
58 fveq2 6178 . . . . . . . . . . . . 13 (𝑖 = (𝑗 + 𝑆) → (𝐹𝑖) = (𝐹‘(𝑗 + 𝑆)))
5958fveq2d 6182 . . . . . . . . . . . 12 (𝑖 = (𝑗 + 𝑆) → (𝐼‘(𝐹𝑖)) = (𝐼‘(𝐹‘(𝑗 + 𝑆))))
6050sneqd 4180 . . . . . . . . . . . 12 (𝑖 = (𝑗 + 𝑆) → {(𝑃𝑖)} = {(𝑃‘(𝑗 + 𝑆))})
6159, 60eqeq12d 2635 . . . . . . . . . . 11 (𝑖 = (𝑗 + 𝑆) → ((𝐼‘(𝐹𝑖)) = {(𝑃𝑖)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}))
6261adantl 482 . . . . . . . . . 10 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ((𝐼‘(𝐹𝑖)) = {(𝑃𝑖)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}))
6351, 56preq12d 4267 . . . . . . . . . . 11 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))})
6459adantl 482 . . . . . . . . . . 11 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝐼‘(𝐹𝑖)) = (𝐼‘(𝐹‘(𝑗 + 𝑆))))
6563, 64sseq12d 3626 . . . . . . . . . 10 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖)) ↔ {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))
6657, 62, 65ifpbi123d 1026 . . . . . . . . 9 ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
6749, 66rspcdv 3307 . . . . . . . 8 (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
6810, 67mpdan 701 . . . . . . 7 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
692, 68sylan 488 . . . . . 6 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
7069ex 450 . . . . 5 (𝜑 → (𝑗 ∈ (0..^(𝑁𝑆)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))))
711, 70mpid 44 . . . 4 (𝜑 → (𝑗 ∈ (0..^(𝑁𝑆)) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
7271imp 445 . . 3 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))
73 elfzofz 12469 . . . . 5 (𝑗 ∈ (0..^(𝑁𝑆)) → 𝑗 ∈ (0...(𝑁𝑆)))
74 crctcshwlkn0lem.q . . . . . 6 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
752, 74crctcshwlkn0lem2 26684 . . . . 5 ((𝜑𝑗 ∈ (0...(𝑁𝑆))) → (𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)))
7673, 75sylan2 491 . . . 4 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)))
77 fzofzp1 12549 . . . . 5 (𝑗 ∈ (0..^(𝑁𝑆)) → (𝑗 + 1) ∈ (0...(𝑁𝑆)))
782, 74crctcshwlkn0lem2 26684 . . . . 5 ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁𝑆))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)))
7977, 78sylan2 491 . . . 4 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)))
80 crctcshwlkn0lem.h . . . . . . 7 𝐻 = (𝐹 cyclShift 𝑆)
8180fveq1i 6179 . . . . . 6 (𝐻𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)
82 crctcshwlkn0lem.f . . . . . . . . 9 (𝜑𝐹 ∈ Word 𝐴)
8382adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → 𝐹 ∈ Word 𝐴)
842, 6syl 17 . . . . . . . . 9 (𝜑𝑆 ∈ ℤ)
8584adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → 𝑆 ∈ ℤ)
86 nnz 11384 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
8786adantl 482 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
88 nnz 11384 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ ℕ → 𝑆 ∈ ℤ)
8988adantr 481 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ ℤ)
9087, 89zsubcld 11472 . . . . . . . . . . . . . . 15 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁𝑆) ∈ ℤ)
9112nn0ge0d 11339 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ ℕ → 0 ≤ 𝑆)
9291adantr 481 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤ 𝑆)
93 subge02 10529 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (0 ≤ 𝑆 ↔ (𝑁𝑆) ≤ 𝑁))
9430, 29, 93syl2anr 495 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝑆 ↔ (𝑁𝑆) ≤ 𝑁))
9592, 94mpbid 222 . . . . . . . . . . . . . . 15 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁𝑆) ≤ 𝑁)
9690, 87, 953jca 1240 . . . . . . . . . . . . . 14 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁𝑆) ≤ 𝑁))
97963adant3 1079 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁𝑆) ≤ 𝑁))
9811, 97sylbi 207 . . . . . . . . . . . 12 (𝑆 ∈ (1..^𝑁) → ((𝑁𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁𝑆) ≤ 𝑁))
99 eluz2 11678 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝑁𝑆)) ↔ ((𝑁𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁𝑆) ≤ 𝑁))
10098, 99sylibr 224 . . . . . . . . . . 11 (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ (ℤ‘(𝑁𝑆)))
101 fzoss2 12480 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁𝑆)) → (0..^(𝑁𝑆)) ⊆ (0..^𝑁))
1022, 100, 1013syl 18 . . . . . . . . . 10 (𝜑 → (0..^(𝑁𝑆)) ⊆ (0..^𝑁))
103102sselda 3595 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → 𝑗 ∈ (0..^𝑁))
104 crctcshwlkn0lem.n . . . . . . . . . 10 𝑁 = (#‘𝐹)
105104oveq2i 6646 . . . . . . . . 9 (0..^𝑁) = (0..^(#‘𝐹))
106103, 105syl6eleq 2709 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → 𝑗 ∈ (0..^(#‘𝐹)))
107 cshwidxmod 13530 . . . . . . . 8 ((𝐹 ∈ Word 𝐴𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
10883, 85, 106, 107syl3anc 1324 . . . . . . 7 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
109104eqcomi 2629 . . . . . . . . . 10 (#‘𝐹) = 𝑁
110109oveq2i 6646 . . . . . . . . 9 ((𝑗 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod 𝑁)
11118imp 445 . . . . . . . . . . . . . 14 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ∈ ℕ0)
112 nnm1nn0 11319 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
1131123ad2ant2 1081 . . . . . . . . . . . . . . 15 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 1) ∈ ℕ0)
114113adantr 481 . . . . . . . . . . . . . 14 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑁 − 1) ∈ ℕ0)
11528, 32anim12i 589 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
116115, 35sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))
117116, 38syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 < (𝑁𝑆) ↔ (𝑗 + 𝑆) < 𝑁))
118123ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℕ0)
119118, 14sylan2 491 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 + 𝑆) ∈ ℕ0)
120119nn0zd 11465 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 + 𝑆) ∈ ℤ)
121863ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℤ)
122121adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → 𝑁 ∈ ℤ)
123 zltlem1 11415 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 + 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 𝑆) < 𝑁 ↔ (𝑗 + 𝑆) ≤ (𝑁 − 1)))
124120, 122, 123syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → ((𝑗 + 𝑆) < 𝑁 ↔ (𝑗 + 𝑆) ≤ (𝑁 − 1)))
125124biimpd 219 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → ((𝑗 + 𝑆) < 𝑁 → (𝑗 + 𝑆) ≤ (𝑁 − 1)))
126117, 125sylbid 230 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) → (𝑗 < (𝑁𝑆) → (𝑗 + 𝑆) ≤ (𝑁 − 1)))
127126impancom 456 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ0𝑗 < (𝑁𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1)))
1281273adant2 1078 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ0 ∧ (𝑁𝑆) ∈ ℕ ∧ 𝑗 < (𝑁𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1)))
12927, 128sylbi 207 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^(𝑁𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1)))
130129impcom 446 . . . . . . . . . . . . . 14 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ≤ (𝑁 − 1))
131111, 114, 1303jca 1240 . . . . . . . . . . . . 13 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1)))
13211, 131sylanb 489 . . . . . . . . . . . 12 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1)))
133 elfz2nn0 12415 . . . . . . . . . . . 12 ((𝑗 + 𝑆) ∈ (0...(𝑁 − 1)) ↔ ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1)))
134132, 133sylibr 224 . . . . . . . . . . 11 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ∈ (0...(𝑁 − 1)))
135 zaddcl 11402 . . . . . . . . . . . . 13 ((𝑗 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑗 + 𝑆) ∈ ℤ)
1363, 6, 135syl2anr 495 . . . . . . . . . . . 12 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (𝑗 + 𝑆) ∈ ℤ)
137 zmodid2 12681 . . . . . . . . . . . 12 (((𝑗 + 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆) ↔ (𝑗 + 𝑆) ∈ (0...(𝑁 − 1))))
138136, 26, 137syl2anc 692 . . . . . . . . . . 11 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → (((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆) ↔ (𝑗 + 𝑆) ∈ (0...(𝑁 − 1))))
139134, 138mpbird 247 . . . . . . . . . 10 ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆))
1402, 139sylan 488 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆))
141110, 140syl5eq 2666 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → ((𝑗 + 𝑆) mod (#‘𝐹)) = (𝑗 + 𝑆))
142141fveq2d 6182 . . . . . . 7 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) = (𝐹‘(𝑗 + 𝑆)))
143108, 142eqtrd 2654 . . . . . 6 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘(𝑗 + 𝑆)))
14481, 143syl5eq 2666 . . . . 5 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (𝐻𝑗) = (𝐹‘(𝑗 + 𝑆)))
145144fveq2d 6182 . . . 4 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆))))
146 simp1 1059 . . . . . 6 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)))
147 simp2 1060 . . . . . 6 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)))
148146, 147eqeq12d 2635 . . . . 5 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ((𝑄𝑗) = (𝑄‘(𝑗 + 1)) ↔ (𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆))))
149 simp3 1061 . . . . . 6 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆))))
150146sneqd 4180 . . . . . 6 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → {(𝑄𝑗)} = {(𝑃‘(𝑗 + 𝑆))})
151149, 150eqeq12d 2635 . . . . 5 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ((𝐼‘(𝐻𝑗)) = {(𝑄𝑗)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}))
152146, 147preq12d 4267 . . . . . 6 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → {(𝑄𝑗), (𝑄‘(𝑗 + 1))} = {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))})
153152, 149sseq12d 3626 . . . . 5 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ({(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗)) ↔ {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))
154148, 151, 153ifpbi123d 1026 . . . 4 (((𝑄𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (if-((𝑄𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻𝑗)) = {(𝑄𝑗)}, {(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
15576, 79, 145, 154syl3anc 1324 . . 3 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → (if-((𝑄𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻𝑗)) = {(𝑄𝑗)}, {(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))
15672, 155mpbird 247 . 2 ((𝜑𝑗 ∈ (0..^(𝑁𝑆))) → if-((𝑄𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻𝑗)) = {(𝑄𝑗)}, {(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗))))
157156ralrimiva 2963 1 (𝜑 → ∀𝑗 ∈ (0..^(𝑁𝑆))if-((𝑄𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻𝑗)) = {(𝑄𝑗)}, {(𝑄𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻𝑗))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  if-wif 1011  w3a 1036   = wceq 1481  wcel 1988  wral 2909  wss 3567  ifcif 4077  {csn 4168  {cpr 4170   class class class wbr 4644  cmpt 4720  cfv 5876  (class class class)co 6635  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   < clt 10059  cle 10060  cmin 10251  cn 11005  0cn0 11277  cz 11362  cuz 11672  ...cfz 12311  ..^cfzo 12449   mod cmo 12651  #chash 13100  Word cword 13274   cyclShift ccsh 13515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-fz 12312  df-fzo 12450  df-fl 12576  df-mod 12652  df-hash 13101  df-word 13282  df-concat 13284  df-substr 13286  df-csh 13516
This theorem is referenced by:  crctcshwlkn0lem7  26689
  Copyright terms: Public domain W3C validator