Metamath Proof Explorer


Theorem ccat2s1lenOLD

Description: Obsolete version of ccat2s1len as of 14-Jan-2024. The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ccat2s1lenOLD XVYV⟨“X”⟩++⟨“Y”⟩=2

Proof

Step Hyp Ref Expression
1 s1cl XV⟨“X”⟩WordV
2 s1cl YV⟨“Y”⟩WordV
3 ccatlenOLD ⟨“X”⟩WordV⟨“Y”⟩WordV⟨“X”⟩++⟨“Y”⟩=⟨“X”⟩+⟨“Y”⟩
4 s1len ⟨“X”⟩=1
5 s1len ⟨“Y”⟩=1
6 4 5 oveq12i ⟨“X”⟩+⟨“Y”⟩=1+1
7 1p1e2 1+1=2
8 6 7 eqtri ⟨“X”⟩+⟨“Y”⟩=2
9 3 8 eqtrdi ⟨“X”⟩WordV⟨“Y”⟩WordV⟨“X”⟩++⟨“Y”⟩=2
10 1 2 9 syl2an XVYV⟨“X”⟩++⟨“Y”⟩=2