Step | Hyp | Ref
| Expression |
1 | | eqeq1 2614 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑤 = ∅ ↔ 𝑊 = ∅)) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (𝑤 = ∅ ↔ 𝑊 = ∅)) |
3 | | simpl 472 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → 𝑤 = 𝑊) |
4 | | simpr 476 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
5 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊)) |
6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (#‘𝑤) = (#‘𝑊)) |
7 | 4, 6 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (𝑛 mod (#‘𝑤)) = (𝑁 mod (#‘𝑊))) |
8 | 7, 6 | opeq12d 4348 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉 = 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) |
9 | 3, 8 | oveq12d 6567 |
. . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (𝑤 substr 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉) = (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) |
10 | 7 | opeq2d 4347 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → 〈0, (𝑛 mod (#‘𝑤))〉 = 〈0, (𝑁 mod (#‘𝑊))〉) |
11 | 3, 10 | oveq12d 6567 |
. . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (𝑤 substr 〈0, (𝑛 mod (#‘𝑤))〉) = (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) |
12 | 9, 11 | oveq12d 6567 |
. . 3
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → ((𝑤 substr 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉) ++ (𝑤 substr 〈0, (𝑛 mod (#‘𝑤))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
13 | 2, 12 | ifbieq2d 4061 |
. 2
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → if(𝑤 = ∅, ∅, ((𝑤 substr 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉) ++ (𝑤 substr 〈0, (𝑛 mod (#‘𝑤))〉))) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
14 | | df-csh 13386 |
. 2
⊢
cyclShift = (𝑤 ∈
{𝑓 ∣ ∃𝑙 ∈ ℕ0
𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉) ++ (𝑤 substr 〈0, (𝑛 mod (#‘𝑤))〉)))) |
15 | | 0ex 4718 |
. . 3
⊢ ∅
∈ V |
16 | | ovex 6577 |
. . 3
⊢ ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) ∈ V |
17 | 15, 16 | ifex 4106 |
. 2
⊢ if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) ∈ V |
18 | 13, 14, 17 | ovmpt2a 6689 |
1
⊢ ((𝑊 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |