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 ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ cyclShift 1 ) = ⟨“ 𝐵 𝐴 ”⟩ )

Proof

Step Hyp Ref Expression
1 s2len ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
2 1 oveq2i ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) = ( 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 ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) = 1
10 9 1 opeq12i ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ = ⟨ 1 , 2 ⟩
11 10 oveq2i ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) = ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ 1 , 2 ⟩ )
12 s2cl ( ( 𝐴𝑉𝐵𝑉 ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 )
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 ... ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) = ( 0 ... 2 )
21 19 20 eleqtrri 2 ∈ ( 0 ... ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) )
22 swrdval2 ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 ∧ 1 ∈ ( 0 ... 2 ) ∧ 2 ∈ ( 0 ... ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ 1 , 2 ⟩ ) = ( 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ↦ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 1 ) ) ) )
23 16 21 22 mp3an23 ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ 1 , 2 ⟩ ) = ( 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ↦ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 1 ) ) ) )
24 12 23 syl ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ 1 , 2 ⟩ ) = ( 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ↦ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 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 ( ( 𝐴𝑉𝐵𝑉 ) → ( 0 ..^ ( 2 − 1 ) ) = { 0 } )
30 simpr ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) )
31 30 28 eleqtrdi ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → 𝑖 ∈ { 0 } )
32 elsni ( 𝑖 ∈ { 0 } → 𝑖 = 0 )
33 31 32 syl ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → 𝑖 = 0 )
34 33 oveq1d ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → ( 𝑖 + 1 ) = ( 0 + 1 ) )
35 0p1e1 ( 0 + 1 ) = 1
36 34 35 eqtrdi ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → ( 𝑖 + 1 ) = 1 )
37 36 fveq2d ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 1 ) ) = ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 1 ) )
38 s2fv1 ( 𝐵𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 1 ) = 𝐵 )
39 38 ad2antlr ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 1 ) = 𝐵 )
40 37 39 eqtrd ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 1 ) ) = 𝐵 )
41 29 40 mpteq12dva ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝑖 ∈ ( 0 ..^ ( 2 − 1 ) ) ↦ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ ( 𝑖 + 1 ) ) ) = ( 𝑖 ∈ { 0 } ↦ 𝐵 ) )
42 fconstmpt ( { 0 } × { 𝐵 } ) = ( 𝑖 ∈ { 0 } ↦ 𝐵 )
43 0nn0 0 ∈ ℕ0
44 simpr ( ( 𝐴𝑉𝐵𝑉 ) → 𝐵𝑉 )
45 xpsng ( ( 0 ∈ ℕ0𝐵𝑉 ) → ( { 0 } × { 𝐵 } ) = { ⟨ 0 , 𝐵 ⟩ } )
46 43 44 45 sylancr ( ( 𝐴𝑉𝐵𝑉 ) → ( { 0 } × { 𝐵 } ) = { ⟨ 0 , 𝐵 ⟩ } )
47 s1val ( 𝐵𝑉 → ⟨“ 𝐵 ”⟩ = { ⟨ 0 , 𝐵 ⟩ } )
48 47 adantl ( ( 𝐴𝑉𝐵𝑉 ) → ⟨“ 𝐵 ”⟩ = { ⟨ 0 , 𝐵 ⟩ } )
49 46 48 eqtr4d ( ( 𝐴𝑉𝐵𝑉 ) → ( { 0 } × { 𝐵 } ) = ⟨“ 𝐵 ”⟩ )
50 42 49 eqtr3id ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝑖 ∈ { 0 } ↦ 𝐵 ) = ⟨“ 𝐵 ”⟩ )
51 24 41 50 3eqtrd ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ 1 , 2 ⟩ ) = ⟨“ 𝐵 ”⟩ )
52 11 51 syl5eq ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) = ⟨“ 𝐵 ”⟩ )
53 9 oveq2i ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) = ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 )
54 pfx1s2 ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ 𝐴 ”⟩ )
55 53 54 syl5eq ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) = ⟨“ 𝐴 ”⟩ )
56 52 55 oveq12d ( ( 𝐴𝑉𝐵𝑉 ) → ( ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) ++ ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) ) = ( ⟨“ 𝐵 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) )
57 1z 1 ∈ ℤ
58 cshword ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 ∧ 1 ∈ ℤ ) → ( ⟨“ 𝐴 𝐵 ”⟩ cyclShift 1 ) = ( ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) ++ ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) ) )
59 12 57 58 sylancl ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ cyclShift 1 ) = ( ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) ++ ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) ) )
60 df-s2 ⟨“ 𝐵 𝐴 ”⟩ = ( ⟨“ 𝐵 ”⟩ ++ ⟨“ 𝐴 ”⟩ )
61 60 a1i ( ( 𝐴𝑉𝐵𝑉 ) → ⟨“ 𝐵 𝐴 ”⟩ = ( ⟨“ 𝐵 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) )
62 56 59 61 3eqtr4d ( ( 𝐴𝑉𝐵𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ cyclShift 1 ) = ⟨“ 𝐵 𝐴 ”⟩ )