# Metamath Proof Explorer

## Theorem ccatlenOLD

Description: Obsolete version of ccatlen as of 1-Jan-2024. The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ccatlenOLD ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|{S}\right|+\left|{T}\right|$

### Proof

Step Hyp Ref Expression
1 ccatfval ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to {S}\mathrm{++}{T}=\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)$
2 1 fveq2d ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)\right|$
3 fvex ${⊢}{S}\left({x}\right)\in \mathrm{V}$
4 fvex ${⊢}{T}\left({x}-\left|{S}\right|\right)\in \mathrm{V}$
5 3 4 ifex ${⊢}if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\in \mathrm{V}$
6 eqid ${⊢}\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)=\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)$
7 5 6 fnmpti ${⊢}\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)Fn\left(0..^\left|{S}\right|+\left|{T}\right|\right)$
8 hashfn ${⊢}\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)Fn\left(0..^\left|{S}\right|+\left|{T}\right|\right)\to \left|\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)\right|=\left|\left(0..^\left|{S}\right|+\left|{T}\right|\right)\right|$
9 7 8 mp1i ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)⟼if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\right)\right|=\left|\left(0..^\left|{S}\right|+\left|{T}\right|\right)\right|$
10 lencl ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|\in {ℕ}_{0}$
11 lencl ${⊢}{T}\in \mathrm{Word}{B}\to \left|{T}\right|\in {ℕ}_{0}$
12 nn0addcl ${⊢}\left(\left|{S}\right|\in {ℕ}_{0}\wedge \left|{T}\right|\in {ℕ}_{0}\right)\to \left|{S}\right|+\left|{T}\right|\in {ℕ}_{0}$
13 10 11 12 syl2an ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|{S}\right|+\left|{T}\right|\in {ℕ}_{0}$
14 hashfzo0 ${⊢}\left|{S}\right|+\left|{T}\right|\in {ℕ}_{0}\to \left|\left(0..^\left|{S}\right|+\left|{T}\right|\right)\right|=\left|{S}\right|+\left|{T}\right|$
15 13 14 syl ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|\left(0..^\left|{S}\right|+\left|{T}\right|\right)\right|=\left|{S}\right|+\left|{T}\right|$
16 2 9 15 3eqtrd ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|{S}\right|+\left|{T}\right|$