Proof of Theorem cshwcshid
Step | Hyp | Ref
| Expression |
1 | | cshwcshid.2 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑥) = (#‘𝑦)) |
2 | | fznn0sub2 12315 |
. . . . . . . 8
⊢ (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑦))) |
3 | | oveq2 6557 |
. . . . . . . . 9
⊢
((#‘𝑥) =
(#‘𝑦) →
(0...(#‘𝑥)) =
(0...(#‘𝑦))) |
4 | 3 | eleq2d 2673 |
. . . . . . . 8
⊢
((#‘𝑥) =
(#‘𝑦) →
(((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)) ↔ ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑦)))) |
5 | 2, 4 | syl5ibr 235 |
. . . . . . 7
⊢
((#‘𝑥) =
(#‘𝑦) → (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
7 | 6 | com12 32 |
. . . . 5
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝜑 → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝜑 → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥)))) |
9 | 8 | impcom 445 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ((#‘𝑦) − 𝑚) ∈ (0...(#‘𝑥))) |
10 | | cshwcshid.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑦 ∈ Word 𝑉) |
11 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑦 ∈ Word 𝑉) |
12 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → 𝑚 ∈ ℤ) |
13 | 12 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑚 ∈ ℤ) |
14 | | elfz2nn0 12300 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...(#‘𝑦)) ↔ (𝑚 ∈ ℕ0 ∧
(#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦))) |
15 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢
((#‘𝑦) ∈
ℕ0 → (#‘𝑦) ∈ ℤ) |
16 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
17 | | zsubcl 11296 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑦) ∈
ℤ ∧ 𝑚 ∈
ℤ) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
18 | 15, 16, 17 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
19 | 18 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦)) →
((#‘𝑦) − 𝑚) ∈
ℤ) |
20 | 14, 19 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((#‘𝑦) − 𝑚) ∈ ℤ) |
22 | 11, 13, 21 | 3jca 1235 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ)) |
23 | 10, 22 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ)) |
24 | | 2cshw 13410 |
. . . . . . 7
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((#‘𝑦) − 𝑚) ∈ ℤ) → ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚)))) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚)))) |
26 | | nn0cn 11179 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
27 | | nn0cn 11179 |
. . . . . . . . . . . 12
⊢
((#‘𝑦) ∈
ℕ0 → (#‘𝑦) ∈ ℂ) |
28 | 26, 27 | anim12i 588 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0) → (𝑚 ∈ ℂ ∧ (#‘𝑦) ∈
ℂ)) |
29 | 28 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑦) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑦)) →
(𝑚 ∈ ℂ ∧
(#‘𝑦) ∈
ℂ)) |
30 | 14, 29 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑚 ∈ ℂ ∧ (#‘𝑦) ∈
ℂ)) |
31 | | pncan3 10168 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧
(#‘𝑦) ∈ ℂ)
→ (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑚 + ((#‘𝑦) − 𝑚)) = (#‘𝑦)) |
34 | 33 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 cyclShift (𝑚 + ((#‘𝑦) − 𝑚))) = (𝑦 cyclShift (#‘𝑦))) |
35 | | cshwn 13394 |
. . . . . . . 8
⊢ (𝑦 ∈ Word 𝑉 → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
36 | 10, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
37 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑦 cyclShift (#‘𝑦)) = 𝑦) |
38 | 25, 34, 37 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(#‘𝑦))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
39 | 38 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
40 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑥 cyclShift ((#‘𝑦) − 𝑚)) = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚))) |
41 | 40 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
42 | 41 | adantl 481 |
. . . . 5
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
43 | 42 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → (𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((#‘𝑦) − 𝑚)))) |
44 | 39, 43 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) |
45 | | oveq2 6557 |
. . . . 5
⊢ (𝑛 = ((#‘𝑦) − 𝑚) → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) |
46 | 45 | eqeq2d 2620 |
. . . 4
⊢ (𝑛 = ((#‘𝑦) − 𝑚) → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚)))) |
47 | 46 | rspcev 3282 |
. . 3
⊢
((((#‘𝑦)
− 𝑚) ∈
(0...(#‘𝑥)) ∧
𝑦 = (𝑥 cyclShift ((#‘𝑦) − 𝑚))) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
48 | 9, 44, 47 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
49 | 48 | ex 449 |
1
⊢ (𝜑 → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |