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