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 ∈ Word V ∧ W ∈ ℙ
Assertion cshwsdisj ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → Disj n ∈ 0 ..^ W W cyclShift n

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢ φ → W ∈ Word V ∧ W ∈ ℙ
2 orc ⊢ n = j → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
3 2 a1d ⊢ n = j → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
4 simprl ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0
5 simprrl ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n ∈ 0 ..^ W
6 simprrr ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → j ∈ 0 ..^ W
7 necom ⊢ n ≠ j ↔ j ≠ n
8 7 birani ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → j ≠ n
9 1 cshwshashlem3 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W ∧ j ≠ n → W cyclShift n ≠ W cyclShift j
10 9 imp ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W ∧ j ≠ n → W cyclShift n ≠ W cyclShift j
11 4 5 6 8 10 syl13anc ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → W cyclShift n ≠ W cyclShift j
12 disjsn2 ⊢ W cyclShift n ≠ W cyclShift j → W cyclShift n ∩ W cyclShift j = ∅
13 11 12 syl ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → W cyclShift n ∩ W cyclShift j = ∅
14 13 olcd ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
15 14 ex ⊢ n ≠ j → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
16 3 15 pm2.61ine ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
17 16 ralrimivva ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ∀ n ∈ 0 ..^ W ∀ j ∈ 0 ..^ W n = j ∨ W cyclShift n ∩ 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 ∈ 0 ..^ W W cyclShift n ↔ ∀ n ∈ 0 ..^ W ∀ j ∈ 0 ..^ W n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
21 17 20 sylibr ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → Disj n ∈ 0 ..^ W W cyclShift n