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 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ substr ⟨ ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) , ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ⟩ ) = ⟨“ 𝐵 ”⟩ )
53 9 oveq2i ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ prefix ( 1 mod ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ) = ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 )
54 pfx1s2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ 𝐴 ”⟩ )
55 53 54 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ 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 ) = ⟨“ 𝐵 𝐴 ”⟩ )