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”⟩cyclShift1=⟨“BA”⟩

Proof

Step Hyp Ref Expression
1 s2len ⊢⟨“AB”⟩=2
2 1 oveq2i ⊢1mod⟨“AB”⟩=1mod2
3 1re ⊢1∈ℝ
4 2rp ⊢2∈ℝ+
5 0le1 ⊢0≤1
6 1lt2 ⊢1<2
7 modid ⊢1∈ℝ∧2∈ℝ+∧0≤1∧1<2→1mod2=1
8 3 4 5 6 7 mp4an ⊢1mod2=1
9 2 8 eqtri ⊢1mod⟨“AB”⟩=1
10 9 1 opeq12i ⊢1mod⟨“AB”⟩⟨“AB”⟩=12
11 10 oveq2i ⊢⟨“AB”⟩substr1mod⟨“AB”⟩⟨“AB”⟩=⟨“AB”⟩substr12
12 s2cl ⊢A∈V∧B∈V→⟨“AB”⟩∈WordV
13 tpid2g ⊢1∈ℝ→1∈012
14 3 13 ax-mp ⊢1∈012
15 fz0tp ⊢0…2=012
16 14 15 eleqtrri ⊢1∈0…2
17 tpid3g ⊢2∈ℝ+→2∈012
18 4 17 ax-mp ⊢2∈012
19 18 15 eleqtrri ⊢2∈0…2
20 1 oveq2i ⊢0…⟨“AB”⟩=0…2
21 19 20 eleqtrri ⊢2∈0…⟨“AB”⟩
22 swrdval2 ⊢⟨“AB”⟩∈WordV∧1∈0…2∧2∈0…⟨“AB”⟩→⟨“AB”⟩substr12=i∈0..^2−1⟼⟨“AB”⟩⁡i+1
23 16 21 22 mp3an23 ⊢⟨“AB”⟩∈WordV→⟨“AB”⟩substr12=i∈0..^2−1⟼⟨“AB”⟩⁡i+1
24 12 23 syl ⊢A∈V∧B∈V→⟨“AB”⟩substr12=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=0B
46 43 44 45 sylancr ⊢A∈V∧B∈V→0×B=0B
47 s1val ⊢B∈V→⟨“B”⟩=0B
48 47 adantl ⊢A∈V∧B∈V→⟨“B”⟩=0B
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”⟩substr12=⟨“B”⟩
52 11 51 eqtrid ⊢A∈V∧B∈V→⟨“AB”⟩substr1mod⟨“AB”⟩⟨“AB”⟩=⟨“B”⟩
53 9 oveq2i ⊢⟨“AB”⟩prefix1mod⟨“AB”⟩=⟨“AB”⟩prefix1
54 pfx1s2 ⊢A∈V∧B∈V→⟨“AB”⟩prefix1=⟨“A”⟩
55 53 54 eqtrid ⊢A∈V∧B∈V→⟨“AB”⟩prefix1mod⟨“AB”⟩=⟨“A”⟩
56 52 55 oveq12d ⊢A∈V∧B∈V→⟨“AB”⟩substr1mod⟨“AB”⟩⟨“AB”⟩++⟨“AB”⟩prefix1mod⟨“AB”⟩=⟨“B”⟩++⟨“A”⟩
57 1z ⊢1∈ℤ
58 cshword ⊢⟨“AB”⟩∈WordV∧1∈ℤ→⟨“AB”⟩cyclShift1=⟨“AB”⟩substr1mod⟨“AB”⟩⟨“AB”⟩++⟨“AB”⟩prefix1mod⟨“AB”⟩
59 12 57 58 sylancl ⊢A∈V∧B∈V→⟨“AB”⟩cyclShift1=⟨“AB”⟩substr1mod⟨“AB”⟩⟨“AB”⟩++⟨“AB”⟩prefix1mod⟨“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”⟩cyclShift1=⟨“BA”⟩