Proof of Theorem cshwlen
Step | Hyp | Ref
| Expression |
1 | | 0csh0 14506 |
. . . . 5
⊢ (∅
cyclShift 𝑁) =
∅ |
2 | | oveq1 7282 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (∅ cyclShift 𝑁)) |
3 | | id 22 |
. . . . 5
⊢ (𝑊 = ∅ → 𝑊 = ∅) |
4 | 1, 2, 3 | 3eqtr4a 2804 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = 𝑊) |
5 | 4 | fveq2d 6778 |
. . 3
⊢ (𝑊 = ∅ →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊)) |
6 | 5 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊))) |
7 | | cshword 14504 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
8 | 7 | fveq2d 6778 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) =
(♯‘((𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉) ++
(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
9 | 8 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
10 | | swrdcl 14358 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉) |
11 | | pfxcl 14390 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) |
12 | | ccatlen 14278 |
. . . . . 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 723 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
15 | | lennncl 14237 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
16 | | pm3.21 472 |
. . . . . . . . . . 11
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑊
∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))) |
17 | 16 | ex 413 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → (𝑁
∈ ℤ → (𝑊
∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
18 | 15, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
19 | 18 | ex 413 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
20 | 19 | com24 95 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
21 | 20 | pm2.43i 52 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
22 | 21 | imp31 418 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))) |
23 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
24 | | zmodfzp1 13615 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
(0...(♯‘𝑊))) |
25 | 24 | ancoms 459 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ (0...(♯‘𝑊))) |
26 | 25 | adantl 482 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) |
27 | | lencl 14236 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
28 | | nn0fz0 13354 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
29 | 27, 28 | sylib 217 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
30 | 29 | adantr 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘𝑊) ∈
(0...(♯‘𝑊))) |
31 | | swrdlen 14360 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
32 | 23, 26, 30, 31 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
33 | | pfxlen 14396 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
34 | 25, 33 | sylan2 593 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
35 | 32, 34 | oveq12d 7293 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) +
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) |
36 | 27 | nn0cnd 12295 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ) |
37 | | zmodcl 13611 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℕ0) |
38 | 37 | nn0cnd 12295 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℂ) |
39 | 38 | ancoms 459 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ ℂ) |
40 | | npcan 11230 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℂ ∧ (𝑁 mod
(♯‘𝑊)) ∈
ℂ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
41 | 36, 39, 40 | syl2an 596 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
42 | 35, 41 | eqtrd 2778 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) +
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊))))) = (♯‘𝑊)) |
43 | 22, 42 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))) = (♯‘𝑊)) |
44 | 9, 14, 43 | 3eqtrd 2782 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘𝑊)) |
45 | 44 | expcom 414 |
. 2
⊢ (𝑊 ≠ ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊))) |
46 | 6, 45 | pm2.61ine 3028 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑁)) = (♯‘𝑊)) |