Proof of Theorem cshwlen
| Step | Hyp | Ref
| Expression |
| 1 | | 0csh0 14831 |
. . . . 5
⊢ (∅
cyclShift 𝑁) =
∅ |
| 2 | | oveq1 7438 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (∅ cyclShift 𝑁)) |
| 3 | | id 22 |
. . . . 5
⊢ (𝑊 = ∅ → 𝑊 = ∅) |
| 4 | 1, 2, 3 | 3eqtr4a 2803 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = 𝑊) |
| 5 | 4 | fveq2d 6910 |
. . 3
⊢ (𝑊 = ∅ →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊)) |
| 6 | 5 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊))) |
| 7 | | cshword 14829 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
| 8 | 7 | fveq2d 6910 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) =
(♯‘((𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉) ++
(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
| 9 | 8 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
| 10 | | swrdcl 14683 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉) |
| 11 | | pfxcl 14715 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) |
| 12 | | ccatlen 14613 |
. . . . . 6
⊢ (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) → (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
| 13 | 10, 11, 12 | syl2anc 584 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
| 14 | 13 | ad2antrr 726 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
| 15 | | lennncl 14572 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
| 16 | | pm3.21 471 |
. . . . . . . . . . 11
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑊
∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))) |
| 17 | 16 | ex 412 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → (𝑁
∈ ℤ → (𝑊
∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
| 18 | 15, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
| 19 | 18 | ex 412 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
| 20 | 19 | com24 95 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
| 21 | 20 | pm2.43i 52 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
| 22 | 21 | imp31 417 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))) |
| 23 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
| 24 | | zmodfzp1 13935 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
(0...(♯‘𝑊))) |
| 25 | 24 | ancoms 458 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ (0...(♯‘𝑊))) |
| 26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) |
| 27 | | lencl 14571 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
| 28 | | nn0fz0 13665 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 30 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘𝑊) ∈
(0...(♯‘𝑊))) |
| 31 | | swrdlen 14685 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
| 32 | 23, 26, 30, 31 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
| 33 | | pfxlen 14721 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
| 34 | 25, 33 | sylan2 593 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
| 35 | 32, 34 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) +
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) |
| 36 | 27 | nn0cnd 12589 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ) |
| 37 | | zmodcl 13931 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℕ0) |
| 38 | 37 | nn0cnd 12589 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℂ) |
| 39 | 38 | ancoms 458 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ ℂ) |
| 40 | | npcan 11517 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℂ ∧ (𝑁 mod
(♯‘𝑊)) ∈
ℂ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
| 41 | 36, 39, 40 | syl2an 596 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
| 42 | 35, 41 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) +
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊))))) = (♯‘𝑊)) |
| 43 | 22, 42 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))) = (♯‘𝑊)) |
| 44 | 9, 14, 43 | 3eqtrd 2781 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘𝑊)) |
| 45 | 44 | expcom 413 |
. 2
⊢ (𝑊 ≠ ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊))) |
| 46 | 6, 45 | pm2.61ine 3025 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊)) |