Metamath Proof Explorer

Theorem cshwsdisj

Description: The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (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 cshwsdisj 
|- ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> Disj_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )

Proof

Step Hyp Ref Expression
1 cshwshash.0 
 |-  ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
2 orc 
 |-  ( n = j -> ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) )
3 2 a1d 
 |-  ( n = j -> ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) -> ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) ) )
4 simprl 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) )
5 simprrl 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> n e. ( 0 ..^ ( # ` W ) ) )
6 simprrr 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> j e. ( 0 ..^ ( # ` W ) ) )
7 necom 
 |-  ( n =/= j <-> j =/= n )
8 7 birani 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> j =/= n )
9 1 cshwshashlem3 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) /\ j =/= n ) -> ( W cyclShift n ) =/= ( W cyclShift j ) ) )
10 9 imp 
 |-  ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) /\ j =/= n ) ) -> ( W cyclShift n ) =/= ( W cyclShift j ) )
11 4 5 6 8 10 syl13anc 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W cyclShift n ) =/= ( W cyclShift j ) )
12 disjsn2 
 |-  ( ( W cyclShift n ) =/= ( W cyclShift j ) -> ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) )
13 11 12 syl 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) )
14 13 olcd 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) )
15 14 ex 
 |-  ( n =/= j -> ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) -> ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) ) )
16 3 15 pm2.61ine 
 |-  ( ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) -> ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) )
17 16 ralrimivva 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> A. n e. ( 0 ..^ ( # ` W ) ) A. j e. ( 0 ..^ ( # ` W ) ) ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) )
18 oveq2 
 |-  ( n = j -> ( W cyclShift n ) = ( W cyclShift j ) )
19 18 sneqd 
 |-  ( n = j -> { ( W cyclShift n ) } = { ( W cyclShift j ) } )
20 19 disjor 
 |-  ( Disj_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } <-> A. n e. ( 0 ..^ ( # ` W ) ) A. j e. ( 0 ..^ ( # ` W ) ) ( n = j \/ ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) ) )
21 17 20 sylibr 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> Disj_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )