Theorem ccatw2s1ccatws2OLD

Description: Obsolete version of ccatw2s1ccatws2 as of 29-Jan-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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