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 AVBVCVDV⟨“AB”⟩=⟨“CD”⟩⟨“A”⟩=⟨“C”⟩⟨“B”⟩=⟨“D”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⟨“AB”⟩=⟨“A”⟩++⟨“B”⟩
2 1 a1i AVBVCVDV⟨“AB”⟩=⟨“A”⟩++⟨“B”⟩
3 df-s2 ⟨“CD”⟩=⟨“C”⟩++⟨“D”⟩
4 3 a1i AVBVCVDV⟨“CD”⟩=⟨“C”⟩++⟨“D”⟩
5 2 4 eqeq12d AVBVCVDV⟨“AB”⟩=⟨“CD”⟩⟨“A”⟩++⟨“B”⟩=⟨“C”⟩++⟨“D”⟩
6 s1cl AV⟨“A”⟩WordV
7 s1cl BV⟨“B”⟩WordV
8 6 7 anim12i AVBV⟨“A”⟩WordV⟨“B”⟩WordV
9 8 adantr AVBVCVDV⟨“A”⟩WordV⟨“B”⟩WordV
10 s1cl CV⟨“C”⟩WordV
11 s1cl DV⟨“D”⟩WordV
12 10 11 anim12i CVDV⟨“C”⟩WordV⟨“D”⟩WordV
13 12 adantl AVBVCVDV⟨“C”⟩WordV⟨“D”⟩WordV
14 s1len ⟨“A”⟩=1
15 s1len ⟨“C”⟩=1
16 14 15 eqtr4i ⟨“A”⟩=⟨“C”⟩
17 16 a1i AVBVCVDV⟨“A”⟩=⟨“C”⟩
18 ccatopth ⟨“A”⟩WordV⟨“B”⟩WordV⟨“C”⟩WordV⟨“D”⟩WordV⟨“A”⟩=⟨“C”⟩⟨“A”⟩++⟨“B”⟩=⟨“C”⟩++⟨“D”⟩⟨“A”⟩=⟨“C”⟩⟨“B”⟩=⟨“D”⟩
19 9 13 17 18 syl3anc AVBVCVDV⟨“A”⟩++⟨“B”⟩=⟨“C”⟩++⟨“D”⟩⟨“A”⟩=⟨“C”⟩⟨“B”⟩=⟨“D”⟩
20 5 19 bitrd AVBVCVDV⟨“AB”⟩=⟨“CD”⟩⟨“A”⟩=⟨“C”⟩⟨“B”⟩=⟨“D”⟩