Step | Hyp | Ref
| Expression |
1 | | iswrd 14207 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑉) |
2 | | ffn 6593 |
. . . . . 6
⊢ (𝑊:(0..^𝑙)⟶𝑉 → 𝑊 Fn (0..^𝑙)) |
3 | 2 | reximi 3176 |
. . . . 5
⊢
(∃𝑙 ∈
ℕ0 𝑊:(0..^𝑙)⟶𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
4 | 1, 3 | sylbi 216 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙)) |
5 | | fneq1 6517 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤 Fn (0..^𝑙) ↔ 𝑊 Fn (0..^𝑙))) |
6 | 5 | rexbidv 3224 |
. . . . 5
⊢ (𝑤 = 𝑊 → (∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙) ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
7 | 6 | elabg 3607 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ↔ ∃𝑙 ∈ ℕ0 𝑊 Fn (0..^𝑙))) |
8 | 4, 7 | mpbird 256 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)}) |
9 | | cshfn 14491 |
. . 3
⊢ ((𝑊 ∈ {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
10 | 8, 9 | sylan 580 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))) |
11 | | iftrue 4466 |
. . . . 5
⊢ (𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ∅) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ∅) |
13 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) = (∅ substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) |
14 | | swrd0 14359 |
. . . . . . . 8
⊢ (∅
substr 〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉) =
∅ |
15 | 13, 14 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) = ∅) |
16 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 prefix (𝑁 mod (♯‘𝑊))) = (∅ prefix (𝑁 mod (♯‘𝑊)))) |
17 | | pfx0 14376 |
. . . . . . . 8
⊢ (∅
prefix (𝑁 mod
(♯‘𝑊))) =
∅ |
18 | 16, 17 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 prefix (𝑁 mod (♯‘𝑊))) = ∅) |
19 | 15, 18 | oveq12d 7286 |
. . . . . 6
⊢ (𝑊 = ∅ → ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (∅ ++
∅)) |
20 | 19 | adantr 481 |
. . . . 5
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (∅ ++
∅)) |
21 | | ccatidid 14283 |
. . . . 5
⊢ (∅
++ ∅) = ∅ |
22 | 20, 21 | eqtr2di 2795 |
. . . 4
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ∅ = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
23 | 12, 22 | eqtrd 2778 |
. . 3
⊢ ((𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
24 | | iffalse 4469 |
. . . 4
⊢ (¬
𝑊 = ∅ → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
25 | 24 | adantr 481 |
. . 3
⊢ ((¬
𝑊 = ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
26 | 23, 25 | pm2.61ian 809 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
27 | 10, 26 | eqtrd 2778 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |