Metamath Proof Explorer


Theorem cshw1s2

Description: Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Assertion cshw1s2 A V B V ⟨“ AB ”⟩ cyclShift 1 = ⟨“ BA ”⟩

Proof

Step Hyp Ref Expression
1 s2len ⟨“ AB ”⟩ = 2
2 1 oveq2i 1 mod ⟨“ AB ”⟩ = 1 mod 2
3 1re 1
4 2rp 2 +
5 0le1 0 1
6 1lt2 1 < 2
7 modid 1 2 + 0 1 1 < 2 1 mod 2 = 1
8 3 4 5 6 7 mp4an 1 mod 2 = 1
9 2 8 eqtri 1 mod ⟨“ AB ”⟩ = 1
10 9 1 opeq12i 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ = 1 2
11 10 oveq2i ⟨“ AB ”⟩ substr 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ = ⟨“ AB ”⟩ substr 1 2
12 s2cl A V B V ⟨“ AB ”⟩ Word V
13 tpid2g 1 1 0 1 2
14 3 13 ax-mp 1 0 1 2
15 fz0tp 0 2 = 0 1 2
16 14 15 eleqtrri 1 0 2
17 tpid3g 2 + 2 0 1 2
18 4 17 ax-mp 2 0 1 2
19 18 15 eleqtrri 2 0 2
20 1 oveq2i 0 ⟨“ AB ”⟩ = 0 2
21 19 20 eleqtrri 2 0 ⟨“ AB ”⟩
22 swrdval2 ⟨“ AB ”⟩ Word V 1 0 2 2 0 ⟨“ AB ”⟩ ⟨“ AB ”⟩ substr 1 2 = i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1
23 16 21 22 mp3an23 ⟨“ AB ”⟩ Word V ⟨“ AB ”⟩ substr 1 2 = i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1
24 12 23 syl A V B V ⟨“ AB ”⟩ substr 1 2 = i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1
25 2m1e1 2 1 = 1
26 25 oveq2i 0 ..^ 2 1 = 0 ..^ 1
27 fzo01 0 ..^ 1 = 0
28 26 27 eqtri 0 ..^ 2 1 = 0
29 28 a1i A V B V 0 ..^ 2 1 = 0
30 simpr A V B V i 0 ..^ 2 1 i 0 ..^ 2 1
31 30 28 eleqtrdi A V B V i 0 ..^ 2 1 i 0
32 elsni i 0 i = 0
33 31 32 syl A V B V i 0 ..^ 2 1 i = 0
34 33 oveq1d A V B V i 0 ..^ 2 1 i + 1 = 0 + 1
35 0p1e1 0 + 1 = 1
36 34 35 eqtrdi A V B V i 0 ..^ 2 1 i + 1 = 1
37 36 fveq2d A V B V i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1 = ⟨“ AB ”⟩ 1
38 s2fv1 B V ⟨“ AB ”⟩ 1 = B
39 38 ad2antlr A V B V i 0 ..^ 2 1 ⟨“ AB ”⟩ 1 = B
40 37 39 eqtrd A V B V i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1 = B
41 29 40 mpteq12dva A V B V i 0 ..^ 2 1 ⟨“ AB ”⟩ i + 1 = i 0 B
42 fconstmpt 0 × B = i 0 B
43 0nn0 0 0
44 simpr A V B V B V
45 xpsng 0 0 B V 0 × B = 0 B
46 43 44 45 sylancr A V B V 0 × B = 0 B
47 s1val B V ⟨“ B ”⟩ = 0 B
48 47 adantl A V B V ⟨“ B ”⟩ = 0 B
49 46 48 eqtr4d A V B V 0 × B = ⟨“ B ”⟩
50 42 49 eqtr3id A V B V i 0 B = ⟨“ B ”⟩
51 24 41 50 3eqtrd A V B V ⟨“ AB ”⟩ substr 1 2 = ⟨“ B ”⟩
52 11 51 syl5eq A V B V ⟨“ AB ”⟩ substr 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ = ⟨“ B ”⟩
53 9 oveq2i ⟨“ AB ”⟩ prefix 1 mod ⟨“ AB ”⟩ = ⟨“ AB ”⟩ prefix 1
54 pfx1s2 A V B V ⟨“ AB ”⟩ prefix 1 = ⟨“ A ”⟩
55 53 54 syl5eq A V B V ⟨“ AB ”⟩ prefix 1 mod ⟨“ AB ”⟩ = ⟨“ A ”⟩
56 52 55 oveq12d A V B V ⟨“ AB ”⟩ substr 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ ++ ⟨“ AB ”⟩ prefix 1 mod ⟨“ AB ”⟩ = ⟨“ B ”⟩ ++ ⟨“ A ”⟩
57 1z 1
58 cshword ⟨“ AB ”⟩ Word V 1 ⟨“ AB ”⟩ cyclShift 1 = ⟨“ AB ”⟩ substr 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ ++ ⟨“ AB ”⟩ prefix 1 mod ⟨“ AB ”⟩
59 12 57 58 sylancl A V B V ⟨“ AB ”⟩ cyclShift 1 = ⟨“ AB ”⟩ substr 1 mod ⟨“ AB ”⟩ ⟨“ AB ”⟩ ++ ⟨“ AB ”⟩ prefix 1 mod ⟨“ AB ”⟩
60 df-s2 ⟨“ BA ”⟩ = ⟨“ B ”⟩ ++ ⟨“ A ”⟩
61 60 a1i A V B V ⟨“ BA ”⟩ = ⟨“ B ”⟩ ++ ⟨“ A ”⟩
62 56 59 61 3eqtr4d A V B V ⟨“ AB ”⟩ cyclShift 1 = ⟨“ BA ”⟩