| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ccatcl 14612 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) | 
| 2 |  | swrdcl 14683 | . . . 4
⊢ ((𝑆 ++ 𝑇) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) ∈ Word 𝐵) | 
| 3 |  | wrdfn 14566 | . . . 4
⊢ (((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) Fn
(0..^(♯‘((𝑆 ++
𝑇) substr
〈(♯‘𝑆),
((♯‘𝑆) +
(♯‘𝑇))〉)))) | 
| 4 | 1, 2, 3 | 3syl 18 | . . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) Fn
(0..^(♯‘((𝑆 ++
𝑇) substr
〈(♯‘𝑆),
((♯‘𝑆) +
(♯‘𝑇))〉)))) | 
| 5 |  | lencl 14571 | . . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
ℕ0) | 
| 6 |  | nn0uz 12920 | . . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) | 
| 7 | 5, 6 | eleqtrdi 2851 | . . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘0)) | 
| 8 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
(ℤ≥‘0)) | 
| 9 | 5 | nn0zd 12639 | . . . . . . . . . 10
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℤ) | 
| 10 | 9 | uzidd 12894 | . . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 11 |  | lencl 14571 | . . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈
ℕ0) | 
| 12 |  | uzaddcl 12946 | . . . . . . . . 9
⊢
(((♯‘𝑆)
∈ (ℤ≥‘(♯‘𝑆)) ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 13 | 10, 11, 12 | syl2an 596 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 14 |  | elfzuzb 13558 | . . . . . . . 8
⊢
((♯‘𝑆)
∈ (0...((♯‘𝑆) + (♯‘𝑇))) ↔ ((♯‘𝑆) ∈ (ℤ≥‘0)
∧ ((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆)))) | 
| 15 | 8, 13, 14 | sylanbrc 583 | . . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇)))) | 
| 16 |  | nn0addcl 12561 | . . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ ℕ0 ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
ℕ0) | 
| 17 | 5, 11, 16 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
ℕ0) | 
| 18 | 17, 6 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘0)) | 
| 19 | 17 | nn0zd 12639 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) | 
| 20 | 19 | uzidd 12894 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘((♯‘𝑆) + (♯‘𝑇)))) | 
| 21 |  | elfzuzb 13558 | . . . . . . . . 9
⊢
(((♯‘𝑆)
+ (♯‘𝑇)) ∈
(0...((♯‘𝑆) +
(♯‘𝑇))) ↔
(((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘0) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘((♯‘𝑆) + (♯‘𝑇))))) | 
| 22 | 18, 20, 21 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ (0...((♯‘𝑆) + (♯‘𝑇)))) | 
| 23 |  | ccatlen 14613 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) | 
| 24 | 23 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0...(♯‘(𝑆 ++ 𝑇))) = (0...((♯‘𝑆) + (♯‘𝑇)))) | 
| 25 | 22, 24 | eleqtrrd 2844 | . . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ (0...(♯‘(𝑆 ++ 𝑇)))) | 
| 26 |  | swrdlen 14685 | . . . . . . 7
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇))) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈
(0...(♯‘(𝑆 ++
𝑇)))) →
(♯‘((𝑆 ++ 𝑇) substr
〈(♯‘𝑆),
((♯‘𝑆) +
(♯‘𝑇))〉))
= (((♯‘𝑆) +
(♯‘𝑇)) −
(♯‘𝑆))) | 
| 27 | 1, 15, 25, 26 | syl3anc 1373 | . . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉)) =
(((♯‘𝑆) +
(♯‘𝑇)) −
(♯‘𝑆))) | 
| 28 | 5 | nn0cnd 12589 | . . . . . . 7
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℂ) | 
| 29 | 11 | nn0cnd 12589 | . . . . . . 7
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℂ) | 
| 30 |  | pncan2 11515 | . . . . . . 7
⊢
(((♯‘𝑆)
∈ ℂ ∧ (♯‘𝑇) ∈ ℂ) →
(((♯‘𝑆) +
(♯‘𝑇)) −
(♯‘𝑆)) =
(♯‘𝑇)) | 
| 31 | 28, 29, 30 | syl2an 596 | . . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (((♯‘𝑆) + (♯‘𝑇)) − (♯‘𝑆)) = (♯‘𝑇)) | 
| 32 | 27, 31 | eqtrd 2777 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉)) =
(♯‘𝑇)) | 
| 33 | 32 | oveq2d 7447 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(♯‘((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉))) =
(0..^(♯‘𝑇))) | 
| 34 | 33 | fneq2d 6662 | . . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) Fn
(0..^(♯‘((𝑆 ++
𝑇) substr
〈(♯‘𝑆),
((♯‘𝑆) +
(♯‘𝑇))〉)))
↔ ((𝑆 ++ 𝑇) substr
〈(♯‘𝑆),
((♯‘𝑆) +
(♯‘𝑇))〉)
Fn (0..^(♯‘𝑇)))) | 
| 35 | 4, 34 | mpbid 232 | . 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) Fn
(0..^(♯‘𝑇))) | 
| 36 |  | wrdfn 14566 | . . 3
⊢ (𝑇 ∈ Word 𝐵 → 𝑇 Fn (0..^(♯‘𝑇))) | 
| 37 | 36 | adantl 481 | . 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 Fn (0..^(♯‘𝑇))) | 
| 38 | 1, 15, 25 | 3jca 1129 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇))) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈
(0...(♯‘(𝑆 ++
𝑇))))) | 
| 39 | 31 | oveq2d 7447 | . . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(((♯‘𝑆) + (♯‘𝑇)) − (♯‘𝑆))) = (0..^(♯‘𝑇))) | 
| 40 | 39 | eleq2d 2827 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑘 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) − (♯‘𝑆))) ↔ 𝑘 ∈ (0..^(♯‘𝑇)))) | 
| 41 | 40 | biimpar 477 | . . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑇))) → 𝑘 ∈ (0..^(((♯‘𝑆) + (♯‘𝑇)) − (♯‘𝑆)))) | 
| 42 |  | swrdfv 14686 | . . . 4
⊢ ((((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇))) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈
(0...(♯‘(𝑆 ++
𝑇)))) ∧ 𝑘 ∈
(0..^(((♯‘𝑆) +
(♯‘𝑇)) −
(♯‘𝑆)))) →
(((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉)‘𝑘) = ((𝑆 ++ 𝑇)‘(𝑘 + (♯‘𝑆)))) | 
| 43 | 38, 41, 42 | syl2an2r 685 | . . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑇))) → (((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉)‘𝑘) = ((𝑆 ++ 𝑇)‘(𝑘 + (♯‘𝑆)))) | 
| 44 |  | ccatval3 14617 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑘 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑘 + (♯‘𝑆))) = (𝑇‘𝑘)) | 
| 45 | 44 | 3expa 1119 | . . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑘 + (♯‘𝑆))) = (𝑇‘𝑘)) | 
| 46 | 43, 45 | eqtrd 2777 | . 2
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑘 ∈ (0..^(♯‘𝑇))) → (((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉)‘𝑘) = (𝑇‘𝑘)) | 
| 47 | 35, 37, 46 | eqfnfvd 7054 | 1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) = 𝑇) |