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 eqtrid ⊢ 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 eqtrid ⊢ 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 ”⟩