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 ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 s1cli ⟨“ 𝑋 ”⟩ ∈ Word V
2 ccatlen ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
3 1 2 mpan2 ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
4 s1len ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
5 4 oveq2i ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 )
6 3 5 eqtrdi ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )