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	$⊢ B \in Word V$
		cats2cat.d	$⊢ D \in Word V$
		cats2cat.a	$⊢ A = B ++ ⟨“ X ”⟩$
		cats2cat.c	$⊢ C = ⟨“ Y ”⟩ ++ D$
	Assertion	cats2cat	$⊢ A ++ C = (B ++ ⟨“ X Y ”⟩) ++ D$

Proof

Step	Hyp	Ref	Expression
1		cats2cat.b	$⊢ B \in Word V$
2		cats2cat.d	$⊢ D \in Word V$
3		cats2cat.a	$⊢ A = B ++ ⟨“ X ”⟩$
4		cats2cat.c	$⊢ C = ⟨“ Y ”⟩ ++ D$
5	3 4	oveq12i	$⊢ A ++ C = (B ++ ⟨“ X ”⟩) ++ (⟨“ Y ”⟩ ++ D)$
6		s1cli	$⊢ ⟨“ X ”⟩ \in Word V$
7		ccatcl	$⊢ (B \in Word V \land ⟨“ X ”⟩ \in Word V) \to B ++ ⟨“ X ”⟩ \in Word V$
8	1 6 7	mp2an	$⊢ B ++ ⟨“ X ”⟩ \in Word V$
9		s1cli	$⊢ ⟨“ Y ”⟩ \in Word V$
10		ccatass	$⊢ (B ++ ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V \land D \in Word V) \to ((B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) ++ D = (B ++ ⟨“ X ”⟩) ++ (⟨“ Y ”⟩ ++ D)$
11	8 9 2 10	mp3an	$⊢ ((B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) ++ D = (B ++ ⟨“ X ”⟩) ++ (⟨“ Y ”⟩ ++ D)$
12		ccatass	$⊢ (B \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V) \to (B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = B ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
13	1 6 9 12	mp3an	$⊢ (B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = B ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
14		df-s2	$⊢ ⟨“ X Y ”⟩ = ⟨“ X ”⟩ ++ ⟨“ Y ”⟩$
15	14	eqcomi	$⊢ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = ⟨“ X Y ”⟩$
16	15	oveq2i	$⊢ B ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) = B ++ ⟨“ X Y ”⟩$
17	13 16	eqtri	$⊢ (B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = B ++ ⟨“ X Y ”⟩$
18	17	oveq1i	$⊢ ((B ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) ++ D = (B ++ ⟨“ X Y ”⟩) ++ D$
19	5 11 18	3eqtr2i	$⊢ A ++ C = (B ++ ⟨“ X Y ”⟩) ++ D$