Metamath Proof Explorer

Theorem ccatw2s1len

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

Ref Expression
Assertion ccatw2s1len ⊢W∈WordV→W++⟨“X”⟩++⟨“Y”⟩=W+2

Proof

Step Hyp Ref Expression
1 ccatws1clv ⊢W∈WordV→W++⟨“X”⟩∈WordV
2 ccatws1len ⊢W++⟨“X”⟩∈WordV→W++⟨“X”⟩++⟨“Y”⟩=W++⟨“X”⟩+1
3 1 2 syl ⊢W∈WordV→W++⟨“X”⟩++⟨“Y”⟩=W++⟨“X”⟩+1
4 ccatws1len ⊢W∈WordV→W++⟨“X”⟩=W+1
5 4 oveq1d ⊢W∈WordV→W++⟨“X”⟩+1=W+1+1
6 lencl ⊢W∈WordV→W∈ℕ0
7 nn0cn ⊢W∈ℕ0→W∈ℂ
8 add1p1 ⊢W∈ℂ→W+1+1=W+2
9 6 7 8 3syl ⊢W∈WordV→W+1+1=W+2
10 3 5 9 3eqtrd ⊢W∈WordV→W++⟨“X”⟩++⟨“Y”⟩=W+2