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 e. V /\ B e. V ) -> ( <" A B "> cyclShift 1 ) = <" B A "> )

Proof

Step Hyp Ref Expression
1 s2len 
 |-  ( # ` <" A B "> ) = 2
2 1 oveq2i 
 |-  ( 1 mod ( # ` <" A B "> ) ) = ( 1 mod 2 )
3 1re 
 |-  1 e. RR
4 2rp 
 |-  2 e. RR+
5 0le1 
 |-  0 <_ 1
6 1lt2 
 |-  1 < 2
7 modid 
 |-  ( ( ( 1 e. RR /\ 2 e. RR+ ) /\ ( 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 ( # ` <" A B "> ) ) = 1
10 9 1 opeq12i 
 |-  <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. = <. 1 , 2 >.
11 10 oveq2i 
 |-  ( <" A B "> substr <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. ) = ( <" A B "> substr <. 1 , 2 >. )
12 s2cl 
 |-  ( ( A e. V /\ B e. V ) -> <" A B "> e. Word V )
13 tpid2g 
 |-  ( 1 e. RR -> 1 e. { 0 , 1 , 2 } )
14 3 13 ax-mp 
 |-  1 e. { 0 , 1 , 2 }
15 fz0tp 
 |-  ( 0 ... 2 ) = { 0 , 1 , 2 }
16 14 15 eleqtrri 
 |-  1 e. ( 0 ... 2 )
17 tpid3g 
 |-  ( 2 e. RR+ -> 2 e. { 0 , 1 , 2 } )
18 4 17 ax-mp 
 |-  2 e. { 0 , 1 , 2 }
19 18 15 eleqtrri 
 |-  2 e. ( 0 ... 2 )
20 1 oveq2i 
 |-  ( 0 ... ( # ` <" A B "> ) ) = ( 0 ... 2 )
21 19 20 eleqtrri 
 |-  2 e. ( 0 ... ( # ` <" A B "> ) )
22 swrdval2 
 |-  ( ( <" A B "> e. Word V /\ 1 e. ( 0 ... 2 ) /\ 2 e. ( 0 ... ( # ` <" A B "> ) ) ) -> ( <" A B "> substr <. 1 , 2 >. ) = ( i e. ( 0 ..^ ( 2 - 1 ) ) |-> ( <" A B "> ` ( i + 1 ) ) ) )
23 16 21 22 mp3an23 
 |-  ( <" A B "> e. Word V -> ( <" A B "> substr <. 1 , 2 >. ) = ( i e. ( 0 ..^ ( 2 - 1 ) ) |-> ( <" A B "> ` ( i + 1 ) ) ) )
24 12 23 syl 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> substr <. 1 , 2 >. ) = ( i e. ( 0 ..^ ( 2 - 1 ) ) |-> ( <" A B "> ` ( 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 e. V /\ B e. V ) -> ( 0 ..^ ( 2 - 1 ) ) = { 0 } )
30 simpr 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> i e. ( 0 ..^ ( 2 - 1 ) ) )
31 30 28 eleqtrdi 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> i e. { 0 } )
32 elsni 
 |-  ( i e. { 0 } -> i = 0 )
33 31 32 syl 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> i = 0 )
34 33 oveq1d 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> ( i + 1 ) = ( 0 + 1 ) )
35 0p1e1 
 |-  ( 0 + 1 ) = 1
36 34 35 eqtrdi 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> ( i + 1 ) = 1 )
37 36 fveq2d 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> ( <" A B "> ` ( i + 1 ) ) = ( <" A B "> ` 1 ) )
38 s2fv1 
 |-  ( B e. V -> ( <" A B "> ` 1 ) = B )
39 38 ad2antlr 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> ( <" A B "> ` 1 ) = B )
40 37 39 eqtrd 
 |-  ( ( ( A e. V /\ B e. V ) /\ i e. ( 0 ..^ ( 2 - 1 ) ) ) -> ( <" A B "> ` ( i + 1 ) ) = B )
41 29 40 mpteq12dva 
 |-  ( ( A e. V /\ B e. V ) -> ( i e. ( 0 ..^ ( 2 - 1 ) ) |-> ( <" A B "> ` ( i + 1 ) ) ) = ( i e. { 0 } |-> B ) )
42 fconstmpt 
 |-  ( { 0 } X. { B } ) = ( i e. { 0 } |-> B )
43 0nn0 
 |-  0 e. NN0
44 simpr 
 |-  ( ( A e. V /\ B e. V ) -> B e. V )
45 xpsng 
 |-  ( ( 0 e. NN0 /\ B e. V ) -> ( { 0 } X. { B } ) = { <. 0 , B >. } )
46 43 44 45 sylancr 
 |-  ( ( A e. V /\ B e. V ) -> ( { 0 } X. { B } ) = { <. 0 , B >. } )
47 s1val 
 |-  ( B e. V -> <" B "> = { <. 0 , B >. } )
48 47 adantl 
 |-  ( ( A e. V /\ B e. V ) -> <" B "> = { <. 0 , B >. } )
49 46 48 eqtr4d 
 |-  ( ( A e. V /\ B e. V ) -> ( { 0 } X. { B } ) = <" B "> )
50 42 49 eqtr3id 
 |-  ( ( A e. V /\ B e. V ) -> ( i e. { 0 } |-> B ) = <" B "> )
51 24 41 50 3eqtrd 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> substr <. 1 , 2 >. ) = <" B "> )
52 11 51 eqtrid 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> substr <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. ) = <" B "> )
53 9 oveq2i 
 |-  ( <" A B "> prefix ( 1 mod ( # ` <" A B "> ) ) ) = ( <" A B "> prefix 1 )
54 pfx1s2 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> prefix 1 ) = <" A "> )
55 53 54 eqtrid 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> prefix ( 1 mod ( # ` <" A B "> ) ) ) = <" A "> )
56 52 55 oveq12d 
 |-  ( ( A e. V /\ B e. V ) -> ( ( <" A B "> substr <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. ) ++ ( <" A B "> prefix ( 1 mod ( # ` <" A B "> ) ) ) ) = ( <" B "> ++ <" A "> ) )
57 1z 
 |-  1 e. ZZ
58 cshword 
 |-  ( ( <" A B "> e. Word V /\ 1 e. ZZ ) -> ( <" A B "> cyclShift 1 ) = ( ( <" A B "> substr <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. ) ++ ( <" A B "> prefix ( 1 mod ( # ` <" A B "> ) ) ) ) )
59 12 57 58 sylancl 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> cyclShift 1 ) = ( ( <" A B "> substr <. ( 1 mod ( # ` <" A B "> ) ) , ( # ` <" A B "> ) >. ) ++ ( <" A B "> prefix ( 1 mod ( # ` <" A B "> ) ) ) ) )
60 df-s2 
 |-  <" B A "> = ( <" B "> ++ <" A "> )
61 60 a1i 
 |-  ( ( A e. V /\ B e. V ) -> <" B A "> = ( <" B "> ++ <" A "> ) )
62 56 59 61 3eqtr4d 
 |-  ( ( A e. V /\ B e. V ) -> ( <" A B "> cyclShift 1 ) = <" B A "> )