# Metamath Proof Explorer

## Theorem ccatcl

Description: The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014) (Proof shortened by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 29-Apr-2020)

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

### 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 wrdf ${⊢}{S}\in \mathrm{Word}{B}\to {S}:\left(0..^\left|{S}\right|\right)⟶{B}$
3 2 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\to {S}:\left(0..^\left|{S}\right|\right)⟶{B}$
4 3 ffvelrnda ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge {x}\in \left(0..^\left|{S}\right|\right)\right)\to {S}\left({x}\right)\in {B}$
5 wrdf ${⊢}{T}\in \mathrm{Word}{B}\to {T}:\left(0..^\left|{T}\right|\right)⟶{B}$
6 5 ad3antlr ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\to {T}:\left(0..^\left|{T}\right|\right)⟶{B}$
7 simpr ${⊢}\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\to {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)$
8 7 anim1i ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\to \left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)$
9 lencl ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|\in {ℕ}_{0}$
10 9 nn0zd ${⊢}{S}\in \mathrm{Word}{B}\to \left|{S}\right|\in ℤ$
11 lencl ${⊢}{T}\in \mathrm{Word}{B}\to \left|{T}\right|\in {ℕ}_{0}$
12 11 nn0zd ${⊢}{T}\in \mathrm{Word}{B}\to \left|{T}\right|\in ℤ$
13 10 12 anim12i ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \left(\left|{S}\right|\in ℤ\wedge \left|{T}\right|\in ℤ\right)$
14 13 ad2antrr ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\to \left(\left|{S}\right|\in ℤ\wedge \left|{T}\right|\in ℤ\right)$
15 fzocatel ${⊢}\left(\left({x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\wedge \left(\left|{S}\right|\in ℤ\wedge \left|{T}\right|\in ℤ\right)\right)\to {x}-\left|{S}\right|\in \left(0..^\left|{T}\right|\right)$
16 8 14 15 syl2anc ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\to {x}-\left|{S}\right|\in \left(0..^\left|{T}\right|\right)$
17 6 16 ffvelrnd ${⊢}\left(\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\wedge ¬{x}\in \left(0..^\left|{S}\right|\right)\right)\to {T}\left({x}-\left|{S}\right|\right)\in {B}$
18 4 17 ifclda ${⊢}\left(\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\wedge {x}\in \left(0..^\left|{S}\right|+\left|{T}\right|\right)\right)\to if\left({x}\in \left(0..^\left|{S}\right|\right),{S}\left({x}\right),{T}\left({x}-\left|{S}\right|\right)\right)\in {B}$
19 18 fmpttd ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \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(0..^\left|{S}\right|+\left|{T}\right|\right)⟶{B}$
20 iswrdi ${⊢}\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(0..^\left|{S}\right|+\left|{T}\right|\right)⟶{B}\to \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)\in \mathrm{Word}{B}$
21 19 20 syl ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to \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)\in \mathrm{Word}{B}$
22 1 21 eqeltrd ${⊢}\left({S}\in \mathrm{Word}{B}\wedge {T}\in \mathrm{Word}{B}\right)\to {S}\mathrm{++}{T}\in \mathrm{Word}{B}$