Metamath Proof Explorer

Theorem s2eq2s1eq

Description: Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018)

Ref Expression
Assertion s2eq2s1eq ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
2 1 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
3 df-s2 ⊢ ⟨“ CD ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩
4 3 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ CD ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩
5 2 4 eqeq12d ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ ⟨“ A ”⟩ ++ ⟨“ B ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩
6 s1cl ⊢ A ∈ V → ⟨“ A ”⟩ ∈ Word V
7 s1cl ⊢ B ∈ V → ⟨“ B ”⟩ ∈ Word V
8 6 7 anim12i ⊢ A ∈ V ∧ B ∈ V → ⟨“ A ”⟩ ∈ Word V ∧ ⟨“ B ”⟩ ∈ Word V
9 8 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ A ”⟩ ∈ Word V ∧ ⟨“ B ”⟩ ∈ Word V
10 s1cl ⊢ C ∈ V → ⟨“ C ”⟩ ∈ Word V
11 s1cl ⊢ D ∈ V → ⟨“ D ”⟩ ∈ Word V
12 10 11 anim12i ⊢ C ∈ V ∧ D ∈ V → ⟨“ C ”⟩ ∈ Word V ∧ ⟨“ D ”⟩ ∈ Word V
13 12 adantl ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ C ”⟩ ∈ Word V ∧ ⟨“ D ”⟩ ∈ Word V
14 s1len ⊢ ⟨“ A ”⟩ = 1
15 s1len ⊢ ⟨“ C ”⟩ = 1
16 14 15 eqtr4i ⊢ ⟨“ A ”⟩ = ⟨“ C ”⟩
17 16 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ A ”⟩ = ⟨“ C ”⟩
18 ccatopth ⊢ ⟨“ A ”⟩ ∈ Word V ∧ ⟨“ B ”⟩ ∈ Word V ∧ ⟨“ C ”⟩ ∈ Word V ∧ ⟨“ D ”⟩ ∈ Word V ∧ ⟨“ A ”⟩ = ⟨“ C ”⟩ → ⟨“ A ”⟩ ++ ⟨“ B ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩ ↔ ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩
19 9 13 17 18 syl3anc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ A ”⟩ ++ ⟨“ B ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩ ↔ ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩
20 5 19 bitrd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩