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 𝑉 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑋 𝑌 ”⟩ ) )