Theorem wrdlenccats1lenm1

Description: The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018) (Revised by AV, 5-Mar-2022)

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

Proof

Step	Hyp	Ref	Expression
1		ccatws1len	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“S”⟩\right|=\left|W\right|+1$$
2	1	oveq1d	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“S”⟩\right|-1=\left|W\right|+1-1$$
3		lencl	$$⊢W\in \mathrm{Word}V\to \left|W\right|\in {\mathbb{N}}_0$$
4	3	nn0cnd	$$⊢W\in \mathrm{Word}V\to \left|W\right|\in ℂ$$
5		pncan1	$$⊢\left|W\right|\in ℂ\to \left|W\right|+1-1=\left|W\right|$$
6	4 5	syl	$$⊢W\in \mathrm{Word}V\to \left|W\right|+1-1=\left|W\right|$$
7	2 6	eqtrd	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“S”⟩\right|-1=\left|W\right|$$