Step | Hyp | Ref
| Expression |
1 | | ccatcl 13212 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
2 | | swrdcl 13271 |
. . . 4
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) ∈ Word 𝐵) |
3 | | wrdf 13165 |
. . . 4
⊢ (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉):(0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)))⟶𝐵) |
4 | | ffn 5958 |
. . . 4
⊢ (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉):(0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)))⟶𝐵 → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) Fn (0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) Fn (0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)))) |
6 | | lencl 13179 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐵 → (#‘𝑆) ∈
ℕ0) |
7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
ℕ0) |
8 | | nn0uz 11598 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
9 | 7, 8 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘0)) |
10 | 7 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ ℤ) |
11 | | uzid 11578 |
. . . . . . . . . 10
⊢
((#‘𝑆) ∈
ℤ → (#‘𝑆)
∈ (ℤ≥‘(#‘𝑆))) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘(#‘𝑆))) |
13 | | lencl 13179 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Word 𝐵 → (#‘𝑇) ∈
ℕ0) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑇) ∈
ℕ0) |
15 | | uzaddcl 11620 |
. . . . . . . . 9
⊢
(((#‘𝑆) ∈
(ℤ≥‘(#‘𝑆)) ∧ (#‘𝑇) ∈ ℕ0) →
((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
16 | 12, 14, 15 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
17 | | elfzuzb 12207 |
. . . . . . . 8
⊢
((#‘𝑆) ∈
(0...((#‘𝑆) +
(#‘𝑇))) ↔
((#‘𝑆) ∈
(ℤ≥‘0) ∧ ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆)))) |
18 | 9, 16, 17 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ (0...((#‘𝑆) + (#‘𝑇)))) |
19 | 7, 14 | nn0addcld 11232 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
ℕ0) |
20 | 19, 8 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘0)) |
21 | 19 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈ ℤ) |
22 | | uzid 11578 |
. . . . . . . . . 10
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈ ℤ
→ ((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
24 | | elfzuzb 12207 |
. . . . . . . . 9
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈
(0...((#‘𝑆) +
(#‘𝑇))) ↔
(((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘0) ∧ ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇))))) |
25 | 20, 23, 24 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈ (0...((#‘𝑆) + (#‘𝑇)))) |
26 | | ccatlen 13213 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) |
27 | 26 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0...(#‘(𝑆 ++ 𝑇))) = (0...((#‘𝑆) + (#‘𝑇)))) |
28 | 25, 27 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈ (0...(#‘(𝑆 ++ 𝑇)))) |
29 | | swrdlen 13275 |
. . . . . . 7
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (#‘𝑆) ∈ (0...((#‘𝑆) + (#‘𝑇))) ∧ ((#‘𝑆) + (#‘𝑇)) ∈ (0...(#‘(𝑆 ++ 𝑇)))) → (#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)) = (((#‘𝑆) + (#‘𝑇)) − (#‘𝑆))) |
30 | 1, 18, 28, 29 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)) = (((#‘𝑆) + (#‘𝑇)) − (#‘𝑆))) |
31 | 7 | nn0cnd 11230 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ ℂ) |
32 | 14 | nn0cnd 11230 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑇) ∈ ℂ) |
33 | 31, 32 | pncan2d 10273 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇)) − (#‘𝑆)) = (#‘𝑇)) |
34 | 30, 33 | eqtrd 2644 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)) = (#‘𝑇)) |
35 | 34 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉))) = (0..^(#‘𝑇))) |
36 | 35 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) Fn (0..^(#‘((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉))) ↔ ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) Fn (0..^(#‘𝑇)))) |
37 | 5, 36 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) Fn (0..^(#‘𝑇))) |
38 | | wrdf 13165 |
. . . 4
⊢ (𝑇 ∈ Word 𝐵 → 𝑇:(0..^(#‘𝑇))⟶𝐵) |
39 | 38 | adantl 481 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇:(0..^(#‘𝑇))⟶𝐵) |
40 | | ffn 5958 |
. . 3
⊢ (𝑇:(0..^(#‘𝑇))⟶𝐵 → 𝑇 Fn (0..^(#‘𝑇))) |
41 | 39, 40 | syl 17 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 Fn (0..^(#‘𝑇))) |
42 | 1 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
43 | 18 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → (#‘𝑆) ∈ (0...((#‘𝑆) + (#‘𝑇)))) |
44 | 28 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → ((#‘𝑆) + (#‘𝑇)) ∈ (0...(#‘(𝑆 ++ 𝑇)))) |
45 | 33 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(((#‘𝑆) + (#‘𝑇)) − (#‘𝑆))) = (0..^(#‘𝑇))) |
46 | 45 | eleq2d 2673 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑘 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) − (#‘𝑆))) ↔ 𝑘 ∈ (0..^(#‘𝑇)))) |
47 | 46 | biimpar 501 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → 𝑘 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) − (#‘𝑆)))) |
48 | | swrdfv 13276 |
. . . 4
⊢ ((((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (#‘𝑆) ∈ (0...((#‘𝑆) + (#‘𝑇))) ∧ ((#‘𝑆) + (#‘𝑇)) ∈ (0...(#‘(𝑆 ++ 𝑇)))) ∧ 𝑘 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) − (#‘𝑆)))) → (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)‘𝑘) = ((𝑆 ++ 𝑇)‘(𝑘 + (#‘𝑆)))) |
49 | 42, 43, 44, 47, 48 | syl31anc 1321 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)‘𝑘) = ((𝑆 ++ 𝑇)‘(𝑘 + (#‘𝑆)))) |
50 | | ccatval3 13216 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑘 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑘 + (#‘𝑆))) = (𝑇‘𝑘)) |
51 | 50 | 3expa 1257 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑘 + (#‘𝑆))) = (𝑇‘𝑘)) |
52 | 49, 51 | eqtrd 2644 |
. 2
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑇))) → (((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉)‘𝑘) = (𝑇‘𝑘)) |
53 | 37, 41, 52 | eqfnfvd 6222 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) = 𝑇) |