Metamath Proof Explorer

Theorem ccatlen

Description: The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by JJ, 1-Jan-2024)

Ref Expression
Assertion ccatlen ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = S + T

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
2 1 fveq2d ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
3 fvex ⊢ S ⁡ x ∈ V
4 fvex ⊢ T ⁡ x − S ∈ V
5 3 4 ifex ⊢ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S ∈ V
6 eqid ⊢ x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
7 5 6 fnmpti ⊢ x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S Fn 0 ..^ S + T
8 hashfn ⊢ x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S Fn 0 ..^ S + T → x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = 0 ..^ S + T
9 7 8 mp1i ⊢ S ∈ Word A ∧ T ∈ Word B → x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = 0 ..^ S + T
10 lencl ⊢ S ∈ Word A → S ∈ ℕ 0
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 nn0addcl ⊢ S ∈ ℕ 0 ∧ T ∈ ℕ 0 → S + T ∈ ℕ 0
13 10 11 12 syl2an ⊢ S ∈ Word A ∧ T ∈ Word B → S + T ∈ ℕ 0
14 hashfzo0 ⊢ S + T ∈ ℕ 0 → 0 ..^ S + T = S + T
15 13 14 syl ⊢ S ∈ Word A ∧ T ∈ Word B → 0 ..^ S + T = S + T
16 2 9 15 3eqtrd ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = S + T