Step | Hyp | Ref
| Expression |
1 | | ccatcl 13435 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
2 | | lencl 13399 |
. . . . . 6
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
ℕ0) |
3 | 2 | adantr 472 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
ℕ0) |
4 | | nn0uz 11804 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
5 | 3, 4 | syl6eleq 2781 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
(ℤ≥‘0)) |
6 | | ccatlen 13436 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) |
7 | 3 | nn0zd 11561 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℤ) |
8 | | uzid 11783 |
. . . . . . 7
⊢
((♯‘𝑆)
∈ ℤ → (♯‘𝑆) ∈
(ℤ≥‘(♯‘𝑆))) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
(ℤ≥‘(♯‘𝑆))) |
10 | | lencl 13399 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈
ℕ0) |
11 | 10 | adantl 473 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑇) ∈
ℕ0) |
12 | | uzaddcl 11826 |
. . . . . 6
⊢
(((♯‘𝑆)
∈ (ℤ≥‘(♯‘𝑆)) ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) |
13 | 9, 11, 12 | syl2anc 696 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) |
14 | 6, 13 | eqeltrd 2771 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) |
15 | | elfzuzb 12418 |
. . . 4
⊢
((♯‘𝑆)
∈ (0...(♯‘(𝑆 ++ 𝑇))) ↔ ((♯‘𝑆) ∈ (ℤ≥‘0)
∧ (♯‘(𝑆 ++
𝑇)) ∈
(ℤ≥‘(♯‘𝑆)))) |
16 | 5, 14, 15 | sylanbrc 701 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ (0...(♯‘(𝑆 ++ 𝑇)))) |
17 | | swrd0val 13509 |
. . 3
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (♯‘𝑆) ∈ (0...(♯‘(𝑆 ++ 𝑇)))) → ((𝑆 ++ 𝑇) substr 〈0, (♯‘𝑆)〉) = ((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆)))) |
18 | 1, 16, 17 | syl2anc 696 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (♯‘𝑆)〉) = ((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆)))) |
19 | | wrdf 13385 |
. . . . 5
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐵 → (𝑆 ++ 𝑇):(0..^(♯‘(𝑆 ++ 𝑇)))⟶𝐵) |
20 | | ffn 6126 |
. . . . 5
⊢ ((𝑆 ++ 𝑇):(0..^(♯‘(𝑆 ++ 𝑇)))⟶𝐵 → (𝑆 ++ 𝑇) Fn (0..^(♯‘(𝑆 ++ 𝑇)))) |
21 | 1, 19, 20 | 3syl 18 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) Fn (0..^(♯‘(𝑆 ++ 𝑇)))) |
22 | | fzoss2 12579 |
. . . . 5
⊢
((♯‘(𝑆
++ 𝑇)) ∈
(ℤ≥‘(♯‘𝑆)) → (0..^(♯‘𝑆)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
23 | 14, 22 | syl 17 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(♯‘𝑆)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) |
24 | | fnssres 6085 |
. . . 4
⊢ (((𝑆 ++ 𝑇) Fn (0..^(♯‘(𝑆 ++ 𝑇))) ∧ (0..^(♯‘𝑆)) ⊆
(0..^(♯‘(𝑆 ++
𝑇)))) → ((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆))) Fn (0..^(♯‘𝑆))) |
25 | 21, 23, 24 | syl2anc 696 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆))) Fn (0..^(♯‘𝑆))) |
26 | | wrdf 13385 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐵 → 𝑆:(0..^(♯‘𝑆))⟶𝐵) |
27 | 26 | adantr 472 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆:(0..^(♯‘𝑆))⟶𝐵) |
28 | | ffn 6126 |
. . . 4
⊢ (𝑆:(0..^(♯‘𝑆))⟶𝐵 → 𝑆 Fn (0..^(♯‘𝑆))) |
29 | 27, 28 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 Fn (0..^(♯‘𝑆))) |
30 | | fvres 6288 |
. . . . 5
⊢ (𝑘 ∈
(0..^(♯‘𝑆))
→ (((𝑆 ++ 𝑇) ↾
(0..^(♯‘𝑆)))‘𝑘) = ((𝑆 ++ 𝑇)‘𝑘)) |
31 | 30 | adantl 473 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑆))) → (((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆)))‘𝑘) = ((𝑆 ++ 𝑇)‘𝑘)) |
32 | | ccatval1 13438 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑘 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑘) = (𝑆‘𝑘)) |
33 | 32 | 3expa 1111 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑘) = (𝑆‘𝑘)) |
34 | 31, 33 | eqtrd 2726 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑆))) → (((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆)))‘𝑘) = (𝑆‘𝑘)) |
35 | 25, 29, 34 | eqfnfvd 6397 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ↾ (0..^(♯‘𝑆))) = 𝑆) |
36 | 18, 35 | eqtrd 2726 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (♯‘𝑆)〉) = 𝑆) |