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 biimpi 
 |-  ( n =/= j -> j =/= n )
9 8 adantr 
 |-  ( ( n =/= j /\ ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ ( n e. ( 0 ..^ ( # ` W ) ) /\ j e. ( 0 ..^ ( # ` W ) ) ) ) ) -> j =/= n )
10 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 ) ) )
11 10 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 ) )
12 4 5 6 9 11 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 ) )
13 disjsn2 
 |-  ( ( W cyclShift n ) =/= ( W cyclShift j ) -> ( { ( W cyclShift n ) } i^i { ( W cyclShift j ) } ) = (/) )
14 12 13 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 ) } ) = (/) )
15 14 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 ) } ) = (/) ) )
16 15 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 ) } ) = (/) ) ) )
17 3 16 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 ) } ) = (/) ) )
18 17 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 ) } ) = (/) ) )
19 oveq2 
 |-  ( n = j -> ( W cyclShift n ) = ( W cyclShift j ) )
20 19 sneqd 
 |-  ( n = j -> { ( W cyclShift n ) } = { ( W cyclShift j ) } )
21 20 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 ) } ) = (/) ) )
22 18 21 sylibr 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> Disj_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )