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