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 ∈ Word V → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2

Proof

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