Metamath Proof Explorer

Theorem cshw0

Description: A word cyclically shifted by 0 is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshw0 
|- ( W e. Word V -> ( W cyclShift 0 ) = W )

Proof

Step Hyp Ref Expression
1 0csh0 
 |-  ( (/) cyclShift 0 ) = (/)
2 oveq1 
 |-  ( (/) = W -> ( (/) cyclShift 0 ) = ( W cyclShift 0 ) )
3 id 
 |-  ( (/) = W -> (/) = W )
4 1 2 3 3eqtr3a 
 |-  ( (/) = W -> ( W cyclShift 0 ) = W )
5 4 a1d 
 |-  ( (/) = W -> ( W e. Word V -> ( W cyclShift 0 ) = W ) )
6 0z 
 |-  0 e. ZZ
7 cshword 
 |-  ( ( W e. Word V /\ 0 e. ZZ ) -> ( W cyclShift 0 ) = ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) )
8 6 7 mpan2 
 |-  ( W e. Word V -> ( W cyclShift 0 ) = ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) )
9 8 adantr 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W cyclShift 0 ) = ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) )
10 necom 
 |-  ( (/) =/= W <-> W =/= (/) )
11 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
12 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
13 0mod 
 |-  ( ( # ` W ) e. RR+ -> ( 0 mod ( # ` W ) ) = 0 )
14 13 opeq1d 
 |-  ( ( # ` W ) e. RR+ -> <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. = <. 0 , ( # ` W ) >. )
15 14 oveq2d 
 |-  ( ( # ` W ) e. RR+ -> ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) = ( W substr <. 0 , ( # ` W ) >. ) )
16 13 oveq2d 
 |-  ( ( # ` W ) e. RR+ -> ( W prefix ( 0 mod ( # ` W ) ) ) = ( W prefix 0 ) )
17 15 16 oveq12d 
 |-  ( ( # ` W ) e. RR+ -> ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) = ( ( W substr <. 0 , ( # ` W ) >. ) ++ ( W prefix 0 ) ) )
18 11 12 17 3syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) = ( ( W substr <. 0 , ( # ` W ) >. ) ++ ( W prefix 0 ) ) )
19 10 18 sylan2b 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( ( W substr <. ( 0 mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( 0 mod ( # ` W ) ) ) ) = ( ( W substr <. 0 , ( # ` W ) >. ) ++ ( W prefix 0 ) ) )
20 9 19 eqtrd 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W cyclShift 0 ) = ( ( W substr <. 0 , ( # ` W ) >. ) ++ ( W prefix 0 ) ) )
21 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
22 pfxval 
 |-  ( ( W e. Word V /\ ( # ` W ) e. NN0 ) -> ( W prefix ( # ` W ) ) = ( W substr <. 0 , ( # ` W ) >. ) )
23 21 22 mpdan 
 |-  ( W e. Word V -> ( W prefix ( # ` W ) ) = ( W substr <. 0 , ( # ` W ) >. ) )
24 pfxid 
 |-  ( W e. Word V -> ( W prefix ( # ` W ) ) = W )
25 23 24 eqtr3d 
 |-  ( W e. Word V -> ( W substr <. 0 , ( # ` W ) >. ) = W )
26 25 adantr 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W substr <. 0 , ( # ` W ) >. ) = W )
27 pfx00 
 |-  ( W prefix 0 ) = (/)
28 27 a1i 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W prefix 0 ) = (/) )
29 26 28 oveq12d 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( ( W substr <. 0 , ( # ` W ) >. ) ++ ( W prefix 0 ) ) = ( W ++ (/) ) )
30 ccatrid 
 |-  ( W e. Word V -> ( W ++ (/) ) = W )
31 30 adantr 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W ++ (/) ) = W )
32 20 29 31 3eqtrd 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( W cyclShift 0 ) = W )
33 32 expcom 
 |-  ( (/) =/= W -> ( W e. Word V -> ( W cyclShift 0 ) = W ) )
34 5 33 pm2.61ine 
 |-  ( W e. Word V -> ( W cyclShift 0 ) = W )