Proof of Theorem cshwcshid
Step | Hyp | Ref
| Expression |
1 | | fznn0sub2 12446 |
. . . . . . 7
⊢ (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑦))) |
2 | | oveq2 6658 |
. . . . . . . 8
⊢
((#‘𝑥) =
(#‘𝑦) →
(0...(#‘𝑥)) =
(0...(#‘𝑦))) |
3 | 2 | eleq2d 2687 |
. . . . . . 7
⊢
((#‘𝑥) =
(#‘𝑦) →
(((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)) ↔ ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑦)))) |
4 | 1, 3 | syl5ibr 236 |
. . . . . 6
⊢
((#‘𝑥) =
(#‘𝑦) → (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
5 | | cshwcshid.2 |
. . . . . 6
⊢ (𝜑 → (#‘𝑥) = (#‘𝑦)) |
6 | 4, 5 | syl11 33 |
. . . . 5
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝜑 → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝜑 → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
8 | 7 | impcom 446 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥))) |
9 | | cshwcshid.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑦 ∈ Word 𝑉) |
10 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑦 ∈ Word 𝑉) |
11 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → 𝑚 ∈ ℤ) |
12 | 11 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑚 ∈ ℤ) |
13 | | elfz2nn0 12431 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...(#‘𝑦)) ↔ (𝑚 ∈ ℕ0 ∧
(#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦))) |
14 | | nn0z 11400 |
. . . . . . . . . . . . 13
⊢
((#‘𝑦) ∈
ℕ0 → (#‘𝑦) ∈ ℤ) |
15 | | nn0z 11400 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
16 | | zsubcl 11419 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑦) ∈
ℤ ∧ 𝑚 ∈
ℤ) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
17 | 14, 15, 16 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
18 | 17 | 3adant3 1081 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦)) →
((#‘𝑦) − 𝑚) ∈
ℤ) |
19 | 13, 18 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
20 | 19 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
21 | 10, 12, 20 | 3jca 1242 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ)) |
22 | 9, 21 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ)) |
23 | | 2cshw 13559 |
. . . . . . 7
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ) → ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚)))) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚)))) |
25 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
26 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢
((#‘𝑦) ∈
ℕ0 → (#‘𝑦) ∈ ℂ) |
27 | 25, 26 | anim12i 590 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0) → (𝑚 ∈ ℂ ∧ (#‘𝑦) ∈
ℂ)) |
28 | 27 | 3adant3 1081 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦)) →
(𝑚 ∈ ℂ ∧
(#‘𝑦) ∈
ℂ)) |
29 | 13, 28 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑚 ∈ ℂ ∧ (#‘𝑦) ∈
ℂ)) |
30 | | pncan3 10289 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧
(#‘𝑦) ∈ ℂ)
→ (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
32 | 31 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
33 | 32 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚))) = (𝑦 cyclShift (#‘𝑦))) |
34 | | cshwn 13543 |
. . . . . . . 8
⊢ (𝑦 ∈ Word 𝑉 → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
35 | 9, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
37 | 24, 33, 36 | 3eqtrrd 2661 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
38 | 37 | adantrr 753 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
39 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑥 cyclShift ((#‘𝑦) − 𝑚)) = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
40 | 39 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
41 | 40 | adantl 482 |
. . . . 5
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
42 | 41 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
43 | 38, 42 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) |
44 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = ((#‘𝑦) − 𝑚) → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) |
45 | 44 | eqeq2d 2632 |
. . . 4
⊢ (𝑛 = ((#‘𝑦) − 𝑚) → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)))) |
46 | 45 | rspcev 3309 |
. . 3
⊢
((((#‘𝑦)
− 𝑚) ∈
(0...(#‘𝑥)) ∧
𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
47 | 8, 43, 46 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
48 | 47 | ex 450 |
1
⊢ (𝜑 → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |