Metamath Proof Explorer


Theorem ccatw2s1ccatws2

Description: The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 29-Jan-2024)

Ref Expression
Assertion ccatw2s1ccatws2 ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 ccatw2s1ass ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
2 df-s2 ⟨“ 𝑋 𝑌 ”⟩ = ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ )
3 2 eqcomi ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) = ⟨“ 𝑋 𝑌 ”⟩
4 3 a1i ( 𝑊 ∈ Word 𝑉 → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) = ⟨“ 𝑋 𝑌 ”⟩ )
5 4 oveq2d ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )
6 1 5 eqtrd ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )