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 biimpi ⊢ n ≠ j → j ≠ n
9 8 adantr ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → j ≠ n
10 1 cshwshashlem3 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W ∧ j ≠ n → W cyclShift n ≠ W cyclShift j
11 10 imp ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W ∧ j ≠ n → W cyclShift n ≠ W cyclShift j
12 4 5 6 9 11 syl13anc ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → W cyclShift n ≠ W cyclShift j
13 disjsn2 ⊢ W cyclShift n ≠ W cyclShift j → W cyclShift n ∩ W cyclShift j = ∅
14 12 13 syl ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → W cyclShift n ∩ W cyclShift j = ∅
15 14 olcd ⊢ n ≠ j ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
16 15 ex ⊢ n ≠ j → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
17 3 16 pm2.61ine ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W ∧ j ∈ 0 ..^ W → n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
18 17 ralrimivva ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ∀ n ∈ 0 ..^ W ∀ j ∈ 0 ..^ W n = j ∨ W cyclShift n ∩ 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 ∈ 0 ..^ W W cyclShift n ↔ ∀ n ∈ 0 ..^ W ∀ j ∈ 0 ..^ W n = j ∨ W cyclShift n ∩ W cyclShift j = ∅
22 18 21 sylibr ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → Disj n ∈ 0 ..^ W W cyclShift n