# Metamath Proof Explorer

## Theorem cats1len

Description: The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 ${⊢}{T}={S}\mathrm{++}⟨“{X}”⟩$
cats1cli.2 ${⊢}{S}\in \mathrm{Word}\mathrm{V}$
cats1fvn.3 ${⊢}\left|{S}\right|={M}$
cats1len.4 ${⊢}{M}+1={N}$
Assertion cats1len ${⊢}\left|{T}\right|={N}$

### Proof

Step Hyp Ref Expression
1 cats1cld.1 ${⊢}{T}={S}\mathrm{++}⟨“{X}”⟩$
2 cats1cli.2 ${⊢}{S}\in \mathrm{Word}\mathrm{V}$
3 cats1fvn.3 ${⊢}\left|{S}\right|={M}$
4 cats1len.4 ${⊢}{M}+1={N}$
5 1 fveq2i ${⊢}\left|{T}\right|=\left|{S}\mathrm{++}⟨“{X}”⟩\right|$
6 s1cli ${⊢}⟨“{X}”⟩\in \mathrm{Word}\mathrm{V}$
7 ccatlen ${⊢}\left({S}\in \mathrm{Word}\mathrm{V}\wedge ⟨“{X}”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left|{S}\mathrm{++}⟨“{X}”⟩\right|=\left|{S}\right|+\left|⟨“{X}”⟩\right|$
8 2 6 7 mp2an ${⊢}\left|{S}\mathrm{++}⟨“{X}”⟩\right|=\left|{S}\right|+\left|⟨“{X}”⟩\right|$
9 s1len ${⊢}\left|⟨“{X}”⟩\right|=1$
10 3 9 oveq12i ${⊢}\left|{S}\right|+\left|⟨“{X}”⟩\right|={M}+1$
11 8 10 eqtri ${⊢}\left|{S}\mathrm{++}⟨“{X}”⟩\right|={M}+1$
12 11 4 eqtri ${⊢}\left|{S}\mathrm{++}⟨“{X}”⟩\right|={N}$
13 5 12 eqtri ${⊢}\left|{T}\right|={N}$