Metamath Proof Explorer


Theorem ofs2

Description: Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018)

Ref Expression
Assertion ofs2 ASBSCTDT⟨“AB”⟩Rf⟨“CD”⟩=⟨“ARCBRD”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⟨“AB”⟩=⟨“A”⟩++⟨“B”⟩
2 df-s2 ⟨“CD”⟩=⟨“C”⟩++⟨“D”⟩
3 1 2 oveq12i ⟨“AB”⟩Rf⟨“CD”⟩=⟨“A”⟩++⟨“B”⟩Rf⟨“C”⟩++⟨“D”⟩
4 simpll ASBSCTDTAS
5 4 s1cld ASBSCTDT⟨“A”⟩WordS
6 simplr ASBSCTDTBS
7 6 s1cld ASBSCTDT⟨“B”⟩WordS
8 simprl ASBSCTDTCT
9 8 s1cld ASBSCTDT⟨“C”⟩WordT
10 simprr ASBSCTDTDT
11 10 s1cld ASBSCTDT⟨“D”⟩WordT
12 s1len ⟨“A”⟩=1
13 s1len ⟨“C”⟩=1
14 12 13 eqtr4i ⟨“A”⟩=⟨“C”⟩
15 14 a1i ASBSCTDT⟨“A”⟩=⟨“C”⟩
16 s1len ⟨“B”⟩=1
17 s1len ⟨“D”⟩=1
18 16 17 eqtr4i ⟨“B”⟩=⟨“D”⟩
19 18 a1i ASBSCTDT⟨“B”⟩=⟨“D”⟩
20 5 7 9 11 15 19 ofccat ASBSCTDT⟨“A”⟩++⟨“B”⟩Rf⟨“C”⟩++⟨“D”⟩=⟨“A”⟩Rf⟨“C”⟩++⟨“B”⟩Rf⟨“D”⟩
21 3 20 eqtrid ASBSCTDT⟨“AB”⟩Rf⟨“CD”⟩=⟨“A”⟩Rf⟨“C”⟩++⟨“B”⟩Rf⟨“D”⟩
22 ofs1 ASCT⟨“A”⟩Rf⟨“C”⟩=⟨“ARC”⟩
23 4 8 22 syl2anc ASBSCTDT⟨“A”⟩Rf⟨“C”⟩=⟨“ARC”⟩
24 ofs1 BSDT⟨“B”⟩Rf⟨“D”⟩=⟨“BRD”⟩
25 6 10 24 syl2anc ASBSCTDT⟨“B”⟩Rf⟨“D”⟩=⟨“BRD”⟩
26 23 25 oveq12d ASBSCTDT⟨“A”⟩Rf⟨“C”⟩++⟨“B”⟩Rf⟨“D”⟩=⟨“ARC”⟩++⟨“BRD”⟩
27 df-s2 ⟨“ARCBRD”⟩=⟨“ARC”⟩++⟨“BRD”⟩
28 26 27 eqtr4di ASBSCTDT⟨“A”⟩Rf⟨“C”⟩++⟨“B”⟩Rf⟨“D”⟩=⟨“ARCBRD”⟩
29 21 28 eqtrd ASBSCTDT⟨“AB”⟩Rf⟨“CD”⟩=⟨“ARCBRD”⟩