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 ) )