Theorem ccat2s1len

Description: The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 14-Jan-2024)

	Ref	Expression
Assertion	ccat2s1len	$$⊢\left|⟨“X”⟩\mathrm{++}⟨“Y”⟩\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
2		s1cli	$$⊢⟨“Y”⟩\in \mathrm{Word}\mathrm{V}$$
3		ccatlen	$$⊢\left(⟨“X”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“Y”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left|⟨“X”⟩\mathrm{++}⟨“Y”⟩\right|=\left|⟨“X”⟩\right|+\left|⟨“Y”⟩\right|$$
4		s1len	$$⊢\left|⟨“X”⟩\right|=1$$
5		s1len	$$⊢\left|⟨“Y”⟩\right|=1$$
6	4 5	oveq12i	$$⊢\left|⟨“X”⟩\right|+\left|⟨“Y”⟩\right|=1+1$$
7		1p1e2	$$⊢1+1=2$$
8	6 7	eqtri	$$⊢\left|⟨“X”⟩\right|+\left|⟨“Y”⟩\right|=2$$
9	3 8	eqtrdi	$$⊢\left(⟨“X”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“Y”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left|⟨“X”⟩\mathrm{++}⟨“Y”⟩\right|=2$$
10	1 2 9	mp2an	$$⊢\left|⟨“X”⟩\mathrm{++}⟨“Y”⟩\right|=2$$