Metamath Proof Explorer

Theorem cshwshashlem3

Description: If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Hypothesis cshwshash.0 
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
Assertion cshwshashlem3 
|- ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K =/= L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )

Proof

Step Hyp Ref Expression
1 cshwshash.0 
 |-  ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
2 elfzoelz 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) -> K e. ZZ )
3 2 zred 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) -> K e. RR )
4 elfzoelz 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> L e. ZZ )
5 4 zred 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> L e. RR )
6 lttri2 
 |-  ( ( K e. RR /\ L e. RR ) -> ( K =/= L <-> ( K < L \/ L < K ) ) )
7 3 5 6 syl2anr 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( K =/= L <-> ( K < L \/ L < K ) ) )
8 1 cshwshashlem2 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
9 8 com12 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
10 9 3expia 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( K < L -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
11 1 cshwshashlem2 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( K e. ( 0 ..^ ( # ` W ) ) /\ L e. ( 0 ..^ ( # ` W ) ) /\ L < K ) -> ( W cyclShift K ) =/= ( W cyclShift L ) ) )
12 11 imp 
 |-  ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( K e. ( 0 ..^ ( # ` W ) ) /\ L e. ( 0 ..^ ( # ` W ) ) /\ L < K ) ) -> ( W cyclShift K ) =/= ( W cyclShift L ) )
13 12 necomd 
 |-  ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( K e. ( 0 ..^ ( # ` W ) ) /\ L e. ( 0 ..^ ( # ` W ) ) /\ L < K ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) )
14 13 expcom 
 |-  ( ( K e. ( 0 ..^ ( # ` W ) ) /\ L e. ( 0 ..^ ( # ` W ) ) /\ L < K ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
15 14 3expia 
 |-  ( ( K e. ( 0 ..^ ( # ` W ) ) /\ L e. ( 0 ..^ ( # ` W ) ) ) -> ( L < K -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
16 15 ancoms 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( L < K -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
17 10 16 jaod 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( ( K < L \/ L < K ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
18 7 17 sylbid 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( K =/= L -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
19 18 3impia 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K =/= L ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
20 19 com12 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K =/= L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )