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

Theorem 2cshwcshw 13617
Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
Assertion
Ref Expression
2cshwcshw ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
Distinct variable groups:   𝑚,𝑛,𝐾   𝑚,𝑁,𝑛   𝑚,𝑉,𝑛   𝑚,𝑋,𝑛   𝑚,𝑌,𝑛   𝑚,𝑍,𝑛

Proof of Theorem 2cshwcshw
StepHypRef Expression
1 difelfznle 12492 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ ¬ 𝐾𝑚) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
213exp 1283 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
32ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
43imp 444 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
54adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
65com12 32 . . . . . . . . . . . . . 14 𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
76adantl 481 . . . . . . . . . . . . 13 ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
87imp 444 . . . . . . . . . . . 12 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
9 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝑌 ∈ Word 𝑉)
109ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
11 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
1211adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝐾 ∈ ℤ)
1312ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
14 elfz2 12371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐾 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)))
15 zaddcl 11455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 + 𝑁) ∈ ℤ)
1615adantrr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑚 + 𝑁) ∈ ℤ)
17 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈ ℤ)
1816, 17zsubcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
1918ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
20 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
2119, 20syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
22213adant1 1099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2322adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2414, 23sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2524ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2625imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
27 2cshw 13605 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ ((𝑚 + 𝑁) − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
2810, 13, 26, 27syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
2917, 18zaddcld 11524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
3029ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3130, 20syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
32313adant1 1099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3332adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3414, 33sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3534ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3635imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
37 cshwsublen 13588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉 ∧ (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
3810, 36, 37syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
3928, 38eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
40 elfz2nn0 12469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
41 nn0cn 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
42 nn0cn 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐾 ∈ ℕ0𝐾 ∈ ℂ)
43 nn0cn 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
4442, 43anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ))
45 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → 𝐾 ∈ ℂ)
46 addcl 10056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑚 + 𝑁) ∈ ℂ)
4746adantrl 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝑚 + 𝑁) ∈ ℂ)
4845, 47pncan3d 10433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) = (𝑚 + 𝑁))
4948oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = ((𝑚 + 𝑁) − 𝑁))
50 pncan 10325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
5150adantrl 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
5249, 51eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
5341, 44, 52syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ℕ0 ∧ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
5453ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ ℕ0 → ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
55 elfznn0 12471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
5654, 55syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
57563adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
5840, 57sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
5958adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
60 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝑌) = 𝑁 → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁))
6160eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑌) = 𝑁 → (((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚 ↔ ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
6261imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑌) = 𝑁 → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6362adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6463adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6559, 64mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
6665adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
6766imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚)
6867oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))) = (𝑌 cyclShift 𝑚))
6939, 68eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7069adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
71 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7271adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7370, 72eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
7473exp41 637 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
7574com24 95 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
7675imp41 618 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
7776eqeq2d 2661 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
7877biimpd 219 . . . . . . . . . . . . . 14 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
7978impancom 455 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8079impcom 445 . . . . . . . . . . . 12 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
81 oveq2 6698 . . . . . . . . . . . . . 14 (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
8281eqeq2d 2661 . . . . . . . . . . . . 13 (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8382rspcev 3340 . . . . . . . . . . . 12 ((((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
848, 80, 83syl2anc 694 . . . . . . . . . . 11 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
8584exp31 629 . . . . . . . . . 10 𝑚 = 0 → (¬ 𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
86 oveq2 6698 . . . . . . . . . . . . . . . 16 (𝑚 = 0 → (𝑌 cyclShift 𝑚) = (𝑌 cyclShift 0))
8786eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑌 cyclShift 0)))
88 cshw0 13586 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 ∈ Word 𝑉 → (𝑌 cyclShift 0) = 𝑌)
8988adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑌 cyclShift 0) = 𝑌)
9089eqeq2d 2661 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) ↔ 𝑍 = 𝑌))
91 fznn0sub2 12485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐾 ∈ (0...𝑁) → (𝑁𝐾) ∈ (0...𝑁))
9291adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ (0...𝑁))
93 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑌) = 𝑁 → ((#‘𝑌) − 𝐾) = (𝑁𝐾))
9493eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑌) = 𝑁 → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁𝐾) ∈ (0...𝑁)))
9594ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁𝐾) ∈ (0...𝑁)))
9692, 95mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
9796adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
98 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)))
99 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → 𝑌 ∈ Word 𝑉)
100 2cshwid 13606 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
10199, 11, 100syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
10298, 101sylan9eqr 2707 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
103102eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
104 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = ((#‘𝑌) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
105104eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = ((#‘𝑌) − 𝐾) → (𝑌 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))))
106105rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((#‘𝑌) − 𝐾) ∈ (0...𝑁) ∧ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
10797, 103, 106syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
109 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑌 → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift 𝑛)))
110109rexbidv 3081 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 = 𝑌 → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
111110adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
112108, 111mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
113112exp41 637 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = 𝑌 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
114113com24 95 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = 𝑌 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
11590, 114sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
116115com24 95 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
117116impcom 445 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
118117com13 88 . . . . . . . . . . . . . . . 16 (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
119118a1d 25 . . . . . . . . . . . . . . 15 (𝑍 = (𝑌 cyclShift 0) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
12087, 119syl6bi 243 . . . . . . . . . . . . . 14 (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
121120com24 95 . . . . . . . . . . . . 13 (𝑚 = 0 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
122121com15 101 . . . . . . . . . . . 12 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
123122imp41 618 . . . . . . . . . . 11 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
124123com12 32 . . . . . . . . . 10 (𝑚 = 0 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
125 difelfzle 12491 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ 𝐾𝑚) → (𝑚𝐾) ∈ (0...𝑁))
1261253exp 1283 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁))))
127126ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁))))
128127imp 444 . . . . . . . . . . . . . 14 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁)))
129128adantr 480 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁)))
130129impcom 445 . . . . . . . . . . . 12 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → (𝑚𝐾) ∈ (0...𝑁))
1319ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
13212ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
133 zsubcl 11457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ ℤ)
134133ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℤ → (𝐾 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
13520, 11, 134syl2imc 41 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝑚𝐾) ∈ ℤ))
136135ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝑚𝐾) ∈ ℤ))
137136imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚𝐾) ∈ ℤ)
138 2cshw 13605 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ (𝑚𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚𝐾))))
139131, 132, 137, 138syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚𝐾))))
140 zcn 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
14120zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℂ)
142 pncan3 10327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐾 + (𝑚𝐾)) = 𝑚)
143140, 141, 142syl2anr 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ (0...𝑁) ∧ 𝐾 ∈ ℤ) → (𝐾 + (𝑚𝐾)) = 𝑚)
144143ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ (0...𝑁) → (𝐾 ∈ ℤ → (𝐾 + (𝑚𝐾)) = 𝑚))
14511, 144syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚𝐾)) = 𝑚))
146145ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚𝐾)) = 𝑚))
147146imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + (𝑚𝐾)) = 𝑚)
148147oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + (𝑚𝐾))) = (𝑌 cyclShift 𝑚))
149139, 148eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
150149adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
151 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift (𝑚𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
152151eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = (𝑌 cyclShift 𝐾) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾))))
153152adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾))))
154150, 153mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)))
155154eqeq2d 2661 . . . . . . . . . . . . . . . . . . 19 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
156155biimpd 219 . . . . . . . . . . . . . . . . . 18 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
157156exp41 637 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝐾𝑚 → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))))
158157com24 95 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))))
159158imp31 447 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))
160159com23 86 . . . . . . . . . . . . . 14 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝐾𝑚𝑍 = (𝑋 cyclShift (𝑚𝐾)))))
161160imp 444 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾𝑚𝑍 = (𝑋 cyclShift (𝑚𝐾))))
162161impcom 445 . . . . . . . . . . . 12 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))
163 oveq2 6698 . . . . . . . . . . . . . 14 (𝑛 = (𝑚𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift (𝑚𝐾)))
164163eqeq2d 2661 . . . . . . . . . . . . 13 (𝑛 = (𝑚𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
165164rspcev 3340 . . . . . . . . . . . 12 (((𝑚𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift (𝑚𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
166130, 162, 165syl2anc 694 . . . . . . . . . . 11 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
167166ex 449 . . . . . . . . . 10 (𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
16885, 124, 167pm2.61ii 177 . . . . . . . . 9 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
169168ex 449 . . . . . . . 8 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
170169rexlimdva 3060 . . . . . . 7 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
171170ex 449 . . . . . 6 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
172171com23 86 . . . . 5 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
173172ex 449 . . . 4 (𝐾 ∈ (0...𝑁) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
174173com24 95 . . 3 (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
1751743imp 1275 . 2 ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
176175com12 32 1 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wrex 2942   class class class wbr 4685  cfv 5926  (class class class)co 6690  cc 9972  0cc0 9974   + caddc 9977  cle 10113  cmin 10304  0cn0 11330  cz 11415  ...cfz 12364  #chash 13157  Word cword 13323   cyclShift ccsh 13580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-hash 13158  df-word 13331  df-concat 13333  df-substr 13335  df-csh 13581
This theorem is referenced by:  eleclclwwlknlem1  27025
  Copyright terms: Public domain W3C validator