Metamath Proof Explorer


Theorem ccatws1len

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

Ref Expression
Assertion ccatws1len W Word V W ++ ⟨“ X ”⟩ = W + 1

Proof

Step Hyp Ref Expression
1 s1cli ⟨“ X ”⟩ Word V
2 ccatlen W Word V ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = W + ⟨“ X ”⟩
3 1 2 mpan2 W Word V W ++ ⟨“ X ”⟩ = W + ⟨“ X ”⟩
4 s1len ⟨“ X ”⟩ = 1
5 4 oveq2i W + ⟨“ X ”⟩ = W + 1
6 3 5 syl6eq W Word V W ++ ⟨“ X ”⟩ = W + 1