Step | Hyp | Ref
| Expression |
1 | | iswrd 13307 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑉) |
2 | | ffn 6045 |
. . . . . 6
⊢ (𝑊:(0..^𝑙)⟶𝑉 → 𝑊 Fn (0..^𝑙)) |
3 | 2 | reximi 3011 |
. . . . 5
⊢
(∃𝑙 ∈
ℕ0 𝑊:(0..^𝑙)⟶𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
4 | 1, 3 | sylbi 207 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
5 | | fneq1 5979 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤 Fn (0..^𝑙) ↔ 𝑊 Fn (0..^𝑙))) |
6 | 5 | rexbidv 3052 |
. . . . 5
⊢ (𝑤 = 𝑊 → (∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙) ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
7 | 6 | elabg 3351 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
8 | 4, 7 | mpbird 247 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)}) |
9 | | cshfn 13536 |
. . 3
⊢ ((𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
10 | 8, 9 | sylan 488 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
11 | | iftrue 4092 |
. . . . 5
⊢ (𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ∅) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ∅) |
13 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) = (∅ substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) |
14 | | swrd0 13434 |
. . . . . . . 8
⊢ (∅
substr 〈(𝑁 mod
(#‘𝑊)),
(#‘𝑊)〉) =
∅ |
15 | 13, 14 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) = ∅) |
16 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 prefix (𝑁 mod (#‘𝑊))) = (∅ prefix (𝑁 mod (#‘𝑊)))) |
17 | | pfx0 41385 |
. . . . . . . 8
⊢ (∅
prefix (𝑁 mod
(#‘𝑊))) =
∅ |
18 | 16, 17 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 prefix (𝑁 mod (#‘𝑊))) = ∅) |
19 | 15, 18 | oveq12d 6668 |
. . . . . 6
⊢ (𝑊 = ∅ → ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊)))) = (∅ ++
∅)) |
20 | 19 | adantr 481 |
. . . . 5
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊)))) = (∅ ++
∅)) |
21 | | wrd0 13330 |
. . . . . 6
⊢ ∅
∈ Word V |
22 | | ccatrid 13370 |
. . . . . 6
⊢ (∅
∈ Word V → (∅ ++ ∅) = ∅) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢ (∅
++ ∅) = ∅ |
24 | 20, 23 | syl6req 2673 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ∅ = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
25 | 12, 24 | eqtrd 2656 |
. . 3
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
26 | | iffalse 4095 |
. . . . 5
⊢ (¬
𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
27 | 26 | adantr 481 |
. . . 4
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
28 | | simprl 794 |
. . . . . . 7
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
29 | | simprr 796 |
. . . . . . . 8
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ) |
30 | | df-ne 2795 |
. . . . . . . . . 10
⊢ (𝑊 ≠ ∅ ↔ ¬ 𝑊 = ∅) |
31 | | lennncl 13325 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
32 | 31 | ex 450 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (#‘𝑊) ∈
ℕ)) |
33 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 ≠ ∅ → (#‘𝑊) ∈
ℕ)) |
34 | 30, 33 | syl5bir 233 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (¬ 𝑊 = ∅ → (#‘𝑊) ∈
ℕ)) |
35 | 34 | impcom 446 |
. . . . . . . 8
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (#‘𝑊) ∈
ℕ) |
36 | 29, 35 | zmodcld 12691 |
. . . . . . 7
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈
ℕ0) |
37 | | pfxval 41383 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ ℕ0) → (𝑊 prefix (𝑁 mod (#‘𝑊))) = (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) |
38 | 28, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 prefix (𝑁 mod (#‘𝑊))) = (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) |
39 | 38 | eqcomd 2628 |
. . . . 5
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉) = (𝑊 prefix (𝑁 mod (#‘𝑊)))) |
40 | 39 | oveq2d 6666 |
. . . 4
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
41 | 27, 40 | eqtrd 2656 |
. . 3
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
42 | 25, 41 | pm2.61ian 831 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
43 | 10, 42 | eqtrd 2656 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |