Metamath Proof Explorer


Theorem ccatw2s1assOLD

Description: Obsolete version of ccatw2s1ass as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 id ( 𝑊 ∈ Word 𝑉𝑊 ∈ Word 𝑉 )
2 s1cl ( 𝑋𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
3 s1cl ( 𝑌𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
4 ccatass ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
5 1 2 3 4 syl3an ( ( 𝑊 ∈ Word 𝑉𝑋𝑉𝑌𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )