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 ⊢φ→W∈WordV∧W∈ℙ
Assertion cshwsdisj ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→Disjn∈0..^WWcyclShiftn

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢φ→W∈WordV∧W∈ℙ
2 orc ⊢n=j→n=j∨WcyclShiftn∩WcyclShiftj=∅
3 2 a1d ⊢n=j→φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→n=j∨WcyclShiftn∩WcyclShiftj=∅
4 simprl ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→φ∧∃i∈0..^WW⁡i≠W⁡0
5 simprrl ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→n∈0..^W
6 simprrr ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→j∈0..^W
7 necom ⊢n≠j↔j≠n
8 7 biimpi ⊢n≠j→j≠n
9 8 adantr ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→j≠n
10 1 cshwshashlem3 ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→n∈0..^W∧j∈0..^W∧j≠n→WcyclShiftn≠WcyclShiftj
11 10 imp ⊢φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W∧j≠n→WcyclShiftn≠WcyclShiftj
12 4 5 6 9 11 syl13anc ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→WcyclShiftn≠WcyclShiftj
13 disjsn2 ⊢WcyclShiftn≠WcyclShiftj→WcyclShiftn∩WcyclShiftj=∅
14 12 13 syl ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→WcyclShiftn∩WcyclShiftj=∅
15 14 olcd ⊢n≠j∧φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→n=j∨WcyclShiftn∩WcyclShiftj=∅
16 15 ex ⊢n≠j→φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→n=j∨WcyclShiftn∩WcyclShiftj=∅
17 3 16 pm2.61ine ⊢φ∧∃i∈0..^WW⁡i≠W⁡0∧n∈0..^W∧j∈0..^W→n=j∨WcyclShiftn∩WcyclShiftj=∅
18 17 ralrimivva ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→∀n∈0..^W∀j∈0..^Wn=j∨WcyclShiftn∩WcyclShiftj=∅
19 oveq2 ⊢n=j→WcyclShiftn=WcyclShiftj
20 19 sneqd ⊢n=j→WcyclShiftn=WcyclShiftj
21 20 disjor ⊢Disjn∈0..^WWcyclShiftn↔∀n∈0..^W∀j∈0..^Wn=j∨WcyclShiftn∩WcyclShiftj=∅
22 18 21 sylibr ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→Disjn∈0..^WWcyclShiftn