Proof of Theorem cshwcshid
| Step | Hyp | Ref
| Expression |
| 1 | | fznn0sub2 13675 |
. . . . . . 7
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ ((♯‘𝑦)
− 𝑚) ∈
(0...(♯‘𝑦))) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢
((♯‘𝑥) =
(♯‘𝑦) →
(0...(♯‘𝑥)) =
(0...(♯‘𝑦))) |
| 3 | 2 | eleq2d 2827 |
. . . . . . 7
⊢
((♯‘𝑥) =
(♯‘𝑦) →
(((♯‘𝑦) −
𝑚) ∈
(0...(♯‘𝑥))
↔ ((♯‘𝑦)
− 𝑚) ∈
(0...(♯‘𝑦)))) |
| 4 | 1, 3 | imbitrrid 246 |
. . . . . 6
⊢
((♯‘𝑥) =
(♯‘𝑦) →
(𝑚 ∈
(0...(♯‘𝑦))
→ ((♯‘𝑦)
− 𝑚) ∈
(0...(♯‘𝑥)))) |
| 5 | | cshwcshid.2 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑥) = (♯‘𝑦)) |
| 6 | 4, 5 | syl11 33 |
. . . . 5
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ (𝜑 →
((♯‘𝑦) −
𝑚) ∈
(0...(♯‘𝑥)))) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝜑 → ((♯‘𝑦) − 𝑚) ∈ (0...(♯‘𝑥)))) |
| 8 | 7 | impcom 407 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ((♯‘𝑦) − 𝑚) ∈ (0...(♯‘𝑥))) |
| 9 | | cshwcshid.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑦 ∈ Word 𝑉) |
| 10 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → 𝑦 ∈ Word 𝑉) |
| 11 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ 𝑚 ∈
ℤ) |
| 12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → 𝑚 ∈ ℤ) |
| 13 | | elfz2nn0 13658 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(0...(♯‘𝑦))
↔ (𝑚 ∈
ℕ0 ∧ (♯‘𝑦) ∈ ℕ0 ∧ 𝑚 ≤ (♯‘𝑦))) |
| 14 | | nn0z 12638 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑦)
∈ ℕ0 → (♯‘𝑦) ∈ ℤ) |
| 15 | | nn0z 12638 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
| 16 | | zsubcl 12659 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑦)
∈ ℤ ∧ 𝑚
∈ ℤ) → ((♯‘𝑦) − 𝑚) ∈ ℤ) |
| 17 | 14, 15, 16 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (♯‘𝑦)
∈ ℕ0) → ((♯‘𝑦) − 𝑚) ∈ ℤ) |
| 18 | 17 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (♯‘𝑦)
∈ ℕ0 ∧ 𝑚 ≤ (♯‘𝑦)) → ((♯‘𝑦) − 𝑚) ∈ ℤ) |
| 19 | 13, 18 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ ((♯‘𝑦)
− 𝑚) ∈
ℤ) |
| 20 | 19 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → ((♯‘𝑦) − 𝑚) ∈ ℤ) |
| 21 | 10, 12, 20 | 3jca 1129 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((♯‘𝑦) − 𝑚) ∈ ℤ)) |
| 22 | 9, 21 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → (𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((♯‘𝑦) − 𝑚) ∈ ℤ)) |
| 23 | | 2cshw 14851 |
. . . . . . 7
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ((♯‘𝑦) − 𝑚) ∈ ℤ) → ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((♯‘𝑦) − 𝑚)))) |
| 24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚)) = (𝑦 cyclShift (𝑚 + ((♯‘𝑦) − 𝑚)))) |
| 25 | | nn0cn 12536 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
| 26 | | nn0cn 12536 |
. . . . . . . . . . . 12
⊢
((♯‘𝑦)
∈ ℕ0 → (♯‘𝑦) ∈ ℂ) |
| 27 | 25, 26 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (♯‘𝑦)
∈ ℕ0) → (𝑚 ∈ ℂ ∧ (♯‘𝑦) ∈
ℂ)) |
| 28 | 27 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (♯‘𝑦)
∈ ℕ0 ∧ 𝑚 ≤ (♯‘𝑦)) → (𝑚 ∈ ℂ ∧ (♯‘𝑦) ∈
ℂ)) |
| 29 | 13, 28 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ (𝑚 ∈ ℂ
∧ (♯‘𝑦)
∈ ℂ)) |
| 30 | | pncan3 11516 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧
(♯‘𝑦) ∈
ℂ) → (𝑚 +
((♯‘𝑦) −
𝑚)) = (♯‘𝑦)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ (𝑚 +
((♯‘𝑦) −
𝑚)) = (♯‘𝑦)) |
| 32 | 31 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → (𝑚 + ((♯‘𝑦) − 𝑚)) = (♯‘𝑦)) |
| 33 | 32 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → (𝑦 cyclShift (𝑚 + ((♯‘𝑦) − 𝑚))) = (𝑦 cyclShift (♯‘𝑦))) |
| 34 | | cshwn 14835 |
. . . . . . . 8
⊢ (𝑦 ∈ Word 𝑉 → (𝑦 cyclShift (♯‘𝑦)) = 𝑦) |
| 35 | 9, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 cyclShift (♯‘𝑦)) = 𝑦) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → (𝑦 cyclShift (♯‘𝑦)) = 𝑦) |
| 37 | 24, 33, 36 | 3eqtrrd 2782 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(♯‘𝑦))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚))) |
| 38 | 37 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚))) |
| 39 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑥 cyclShift ((♯‘𝑦) − 𝑚)) = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚))) |
| 40 | 39 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑦 = (𝑥 cyclShift ((♯‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚)))) |
| 41 | 40 | adantl 481 |
. . . . 5
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝑦 = (𝑥 cyclShift ((♯‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚)))) |
| 42 | 41 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → (𝑦 = (𝑥 cyclShift ((♯‘𝑦) − 𝑚)) ↔ 𝑦 = ((𝑦 cyclShift 𝑚) cyclShift ((♯‘𝑦) − 𝑚)))) |
| 43 | 38, 42 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → 𝑦 = (𝑥 cyclShift ((♯‘𝑦) − 𝑚))) |
| 44 | | oveq2 7439 |
. . . 4
⊢ (𝑛 = ((♯‘𝑦) − 𝑚) → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift ((♯‘𝑦) − 𝑚))) |
| 45 | 44 | rspceeqv 3645 |
. . 3
⊢
((((♯‘𝑦)
− 𝑚) ∈
(0...(♯‘𝑥))
∧ 𝑦 = (𝑥 cyclShift ((♯‘𝑦) − 𝑚))) → ∃𝑛 ∈ (0...(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
| 46 | 8, 43, 45 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))) → ∃𝑛 ∈ (0...(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
| 47 | 46 | ex 412 |
1
⊢ (𝜑 → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |