Step | Hyp | Ref
| Expression |
1 | | iswrd 13162 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑉) |
2 | | ffn 5958 |
. . . . . 6
⊢ (𝑊:(0..^𝑙)⟶𝑉 → 𝑊 Fn (0..^𝑙)) |
3 | 2 | reximi 2994 |
. . . . 5
⊢
(∃𝑙 ∈
ℕ0 𝑊:(0..^𝑙)⟶𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
4 | 1, 3 | sylbi 206 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
5 | | fneq1 5893 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤 Fn (0..^𝑙) ↔ 𝑊 Fn (0..^𝑙))) |
6 | 5 | rexbidv 3034 |
. . . . 5
⊢ (𝑤 = 𝑊 → (∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙) ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
7 | 6 | elabg 3320 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
8 | 4, 7 | mpbird 246 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)}) |
9 | | cshfn 13387 |
. . 3
⊢ ((𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
10 | 8, 9 | sylan 487 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
11 | | iftrue 4042 |
. . . . 5
⊢ (𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ∅) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ∅) |
13 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) = (∅ substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) |
14 | | swrd0 13286 |
. . . . . . . 8
⊢ (∅
substr 〈(𝑁 mod
(#‘𝑊)),
(#‘𝑊)〉) =
∅ |
15 | 13, 14 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) = ∅) |
16 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉) = (∅ substr 〈0, (𝑁 mod (#‘𝑊))〉)) |
17 | | swrd0 13286 |
. . . . . . . 8
⊢ (∅
substr 〈0, (𝑁 mod
(#‘𝑊))〉) =
∅ |
18 | 16, 17 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉) = ∅) |
19 | 15, 18 | oveq12d 6567 |
. . . . . 6
⊢ (𝑊 = ∅ → ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) = (∅ ++
∅)) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) = (∅ ++
∅)) |
21 | | wrd0 13185 |
. . . . . 6
⊢ ∅
∈ Word 𝑉 |
22 | | ccatrid 13223 |
. . . . . 6
⊢ (∅
∈ Word 𝑉 →
(∅ ++ ∅) = ∅) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢ (∅
++ ∅) = ∅ |
24 | 20, 23 | syl6req 2661 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ∅ = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
25 | 12, 24 | eqtrd 2644 |
. . 3
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
26 | | iffalse 4045 |
. . . 4
⊢ (¬
𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
27 | 26 | adantr 480 |
. . 3
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
28 | 25, 27 | pm2.61ian 827 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
29 | 10, 28 | eqtrd 2644 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |