s3eqs2s1eq

Description: Two length 3 words are equal iff the corresponding length 2 words and singleton words consisting of their symbols are equal. (Contributed by AV, 4-Jan-2022)

		Ref	Expression
	Assertion	s3eqs2s1eq	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ A B C ”⟩ = ⟨“ D E F ”⟩ \leftrightarrow (⟨“ A B ”⟩ = ⟨“ D E ”⟩ \land ⟨“ C ”⟩ = ⟨“ F ”⟩))$

Proof

Step	Hyp	Ref	Expression
1		df-s3	$⊢ ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ ++ ⟨“ C ”⟩$
2	1	a1i	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ ++ ⟨“ C ”⟩$
3		df-s3	$⊢ ⟨“ D E F ”⟩ = ⟨“ D E ”⟩ ++ ⟨“ F ”⟩$
4	3	a1i	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to ⟨“ D E F ”⟩ = ⟨“ D E ”⟩ ++ ⟨“ F ”⟩$
5	2 4	eqeq12d	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ A B C ”⟩ = ⟨“ D E F ”⟩ \leftrightarrow ⟨“ A B ”⟩ ++ ⟨“ C ”⟩ = ⟨“ D E ”⟩ ++ ⟨“ F ”⟩)$
6		s2cl	$⊢ (A \in V \land B \in V) \to ⟨“ A B ”⟩ \in Word V$
7		s1cl	$⊢ C \in V \to ⟨“ C ”⟩ \in Word V$
8	6 7	anim12i	$⊢ ((A \in V \land B \in V) \land C \in V) \to (⟨“ A B ”⟩ \in Word V \land ⟨“ C ”⟩ \in Word V)$
9	8	3impa	$⊢ (A \in V \land B \in V \land C \in V) \to (⟨“ A B ”⟩ \in Word V \land ⟨“ C ”⟩ \in Word V)$
10	9	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ A B ”⟩ \in Word V \land ⟨“ C ”⟩ \in Word V)$
11		s2cl	$⊢ (D \in V \land E \in V) \to ⟨“ D E ”⟩ \in Word V$
12		s1cl	$⊢ F \in V \to ⟨“ F ”⟩ \in Word V$
13	11 12	anim12i	$⊢ ((D \in V \land E \in V) \land F \in V) \to (⟨“ D E ”⟩ \in Word V \land ⟨“ F ”⟩ \in Word V)$
14	13	3impa	$⊢ (D \in V \land E \in V \land F \in V) \to (⟨“ D E ”⟩ \in Word V \land ⟨“ F ”⟩ \in Word V)$
15	14	adantl	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ D E ”⟩ \in Word V \land ⟨“ F ”⟩ \in Word V)$
16		s2len	$⊢ \|⟨“ A B ”⟩\| = 2$
17		s2len	$⊢ \|⟨“ D E ”⟩\| = 2$
18	16 17	eqtr4i	$⊢ \|⟨“ A B ”⟩\| = \|⟨“ D E ”⟩\|$
19	18	a1i	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to \|⟨“ A B ”⟩\| = \|⟨“ D E ”⟩\|$
20		ccatopth	$⊢ ((⟨“ A B ”⟩ \in Word V \land ⟨“ C ”⟩ \in Word V) \land (⟨“ D E ”⟩ \in Word V \land ⟨“ F ”⟩ \in Word V) \land \|⟨“ A B ”⟩\| = \|⟨“ D E ”⟩\|) \to (⟨“ A B ”⟩ ++ ⟨“ C ”⟩ = ⟨“ D E ”⟩ ++ ⟨“ F ”⟩ \leftrightarrow (⟨“ A B ”⟩ = ⟨“ D E ”⟩ \land ⟨“ C ”⟩ = ⟨“ F ”⟩))$
21	10 15 19 20	syl3anc	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ A B ”⟩ ++ ⟨“ C ”⟩ = ⟨“ D E ”⟩ ++ ⟨“ F ”⟩ \leftrightarrow (⟨“ A B ”⟩ = ⟨“ D E ”⟩ \land ⟨“ C ”⟩ = ⟨“ F ”⟩))$
22	5 21	bitrd	$⊢ ((A \in V \land B \in V \land C \in V) \land (D \in V \land E \in V \land F \in V)) \to (⟨“ A B C ”⟩ = ⟨“ D E F ”⟩ \leftrightarrow (⟨“ A B ”⟩ = ⟨“ D E ”⟩ \land ⟨“ C ”⟩ = ⟨“ F ”⟩))$

Metamath Proof Explorer

Theorem s3eqs2s1eq

Proof