Step | Hyp | Ref
| Expression |
1 | | ccatcl 13359 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
2 | | lencl 13324 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐵 → (#‘𝑆) ∈
ℕ0) |
3 | 2 | adantr 481 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
ℕ0) |
4 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
5 | 3, 4 | syl6eleq 2711 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘0)) |
6 | | ccatlen 13360 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) |
7 | 3 | nn0zd 11480 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ ℤ) |
8 | | uzid 11702 |
. . . . . . 7
⊢
((#‘𝑆) ∈
ℤ → (#‘𝑆)
∈ (ℤ≥‘(#‘𝑆))) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘(#‘𝑆))) |
10 | | lencl 13324 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐵 → (#‘𝑇) ∈
ℕ0) |
11 | 10 | adantl 482 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑇) ∈
ℕ0) |
12 | | uzaddcl 11744 |
. . . . . 6
⊢
(((#‘𝑆) ∈
(ℤ≥‘(#‘𝑆)) ∧ (#‘𝑇) ∈ ℕ0) →
((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
13 | 9, 11, 12 | syl2anc 693 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
14 | 6, 13 | eqeltrd 2701 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
15 | | elfzuzb 12336 |
. . . 4
⊢
((#‘𝑆) ∈
(0...(#‘(𝑆 ++ 𝑇))) ↔ ((#‘𝑆) ∈
(ℤ≥‘0) ∧ (#‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(#‘𝑆)))) |
16 | 5, 14, 15 | sylanbrc 698 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ (0...(#‘(𝑆 ++ 𝑇)))) |
17 | | swrd0val 13421 |
. . 3
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (#‘𝑆) ∈ (0...(#‘(𝑆 ++ 𝑇)))) → ((𝑆 ++ 𝑇) substr 〈0, (#‘𝑆)〉) = ((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆)))) |
18 | 1, 16, 17 | syl2anc 693 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (#‘𝑆)〉) = ((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆)))) |
19 | | wrdf 13310 |
. . . . 5
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐵 → (𝑆 ++ 𝑇):(0..^(#‘(𝑆 ++ 𝑇)))⟶𝐵) |
20 | | ffn 6045 |
. . . . 5
⊢ ((𝑆 ++ 𝑇):(0..^(#‘(𝑆 ++ 𝑇)))⟶𝐵 → (𝑆 ++ 𝑇) Fn (0..^(#‘(𝑆 ++ 𝑇)))) |
21 | 1, 19, 20 | 3syl 18 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) Fn (0..^(#‘(𝑆 ++ 𝑇)))) |
22 | | fzoss2 12496 |
. . . . 5
⊢
((#‘(𝑆 ++
𝑇)) ∈
(ℤ≥‘(#‘𝑆)) → (0..^(#‘𝑆)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
23 | 14, 22 | syl 17 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(#‘𝑆)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
24 | | fnssres 6004 |
. . . 4
⊢ (((𝑆 ++ 𝑇) Fn (0..^(#‘(𝑆 ++ 𝑇))) ∧ (0..^(#‘𝑆)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) → ((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆))) Fn (0..^(#‘𝑆))) |
25 | 21, 23, 24 | syl2anc 693 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆))) Fn (0..^(#‘𝑆))) |
26 | | wrdf 13310 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐵 → 𝑆:(0..^(#‘𝑆))⟶𝐵) |
27 | 26 | adantr 481 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆:(0..^(#‘𝑆))⟶𝐵) |
28 | | ffn 6045 |
. . . 4
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐵 → 𝑆 Fn (0..^(#‘𝑆))) |
29 | 27, 28 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 Fn (0..^(#‘𝑆))) |
30 | | fvres 6207 |
. . . . 5
⊢ (𝑘 ∈ (0..^(#‘𝑆)) → (((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆)))‘𝑘) = ((𝑆 ++ 𝑇)‘𝑘)) |
31 | 30 | adantl 482 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑆))) → (((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆)))‘𝑘) = ((𝑆 ++ 𝑇)‘𝑘)) |
32 | | ccatval1 13361 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑘 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑘) = (𝑆‘𝑘)) |
33 | 32 | 3expa 1265 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑘) = (𝑆‘𝑘)) |
34 | 31, 33 | eqtrd 2656 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(#‘𝑆))) → (((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆)))‘𝑘) = (𝑆‘𝑘)) |
35 | 25, 29, 34 | eqfnfvd 6314 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ↾ (0..^(#‘𝑆))) = 𝑆) |
36 | 18, 35 | eqtrd 2656 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (#‘𝑆)〉) = 𝑆) |