This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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