Metamath Proof Explorer


Theorem cats2cat

Description: Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021)

Ref Expression
Hypotheses cats2cat.b 𝐵 ∈ Word V
cats2cat.d 𝐷 ∈ Word V
cats2cat.a 𝐴 = ( 𝐵 ++ ⟨“ 𝑋 ”⟩ )
cats2cat.c 𝐶 = ( ⟨“ 𝑌 ”⟩ ++ 𝐷 )
Assertion cats2cat ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ++ 𝐷 )

Proof

Step Hyp Ref Expression
1 cats2cat.b 𝐵 ∈ Word V
2 cats2cat.d 𝐷 ∈ Word V
3 cats2cat.a 𝐴 = ( 𝐵 ++ ⟨“ 𝑋 ”⟩ )
4 cats2cat.c 𝐶 = ( ⟨“ 𝑌 ”⟩ ++ 𝐷 )
5 3 4 oveq12i ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ( ⟨“ 𝑌 ”⟩ ++ 𝐷 ) )
6 s1cli ⟨“ 𝑋 ”⟩ ∈ Word V
7 ccatcl ( ( 𝐵 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )
8 1 6 7 mp2an ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V
9 s1cli ⟨“ 𝑌 ”⟩ ∈ Word V
10 ccatass ( ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ∧ 𝐷 ∈ Word V ) → ( ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ++ 𝐷 ) = ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ( ⟨“ 𝑌 ”⟩ ++ 𝐷 ) ) )
11 8 9 2 10 mp3an ( ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ++ 𝐷 ) = ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ( ⟨“ 𝑌 ”⟩ ++ 𝐷 ) )
12 ccatass ( ( 𝐵 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ) → ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝐵 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
13 1 6 9 12 mp3an ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝐵 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) )
14 df-s2 ⟨“ 𝑋 𝑌 ”⟩ = ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ )
15 14 eqcomi ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) = ⟨“ 𝑋 𝑌 ”⟩
16 15 oveq2i ( 𝐵 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) = ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ )
17 13 16 eqtri ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ )
18 17 oveq1i ( ( ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ++ 𝐷 ) = ( ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ++ 𝐷 )
19 5 11 18 3eqtr2i ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ++ 𝐷 )