This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝐴 ++ 𝐶 ) = ( ( 𝐵 ++ ⟨“ 𝑋 𝑌 ”⟩ ) ++ 𝐷 )