Theorem ccatws1len

Description: The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 4-Mar-2022)

	Ref	Expression
Assertion	ccatws1len	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“X”⟩\right|=\left|W\right|+1$$

Proof

Step	Hyp	Ref	Expression
1		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
2		ccatlen	$$⊢\left(W\in \mathrm{Word}V\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left|W\mathrm{++}⟨“X”⟩\right|=\left|W\right|+\left|⟨“X”⟩\right|$$
3	1 2	mpan2	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“X”⟩\right|=\left|W\right|+\left|⟨“X”⟩\right|$$
4		s1len	$$⊢\left|⟨“X”⟩\right|=1$$
5	4	oveq2i	$$⊢\left|W\right|+\left|⟨“X”⟩\right|=\left|W\right|+1$$
6	3 5	eqtrdi	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“X”⟩\right|=\left|W\right|+1$$