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

Proof

Step	Hyp	Ref	Expression
1		ccatws1clv	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )
2		ccatws1len	⊢ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) + 1 ) )
3	1 2	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) + 1 ) )
4		ccatws1len	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
5	4	oveq1d	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) + 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) + 1 ) )
6		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7		nn0cn	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
8		add1p1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) + 1 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
9	6 7 8	3syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) + 1 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )
10	3 5 9	3eqtrd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 2 ) )