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 ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
Assertion cshwsdisj ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
2 orc ⊢ ( 𝑛 = 𝑗 → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
3 2 a1d ⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) ) )
4 simprl ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) )
5 simprrl ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 simprrr ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 necom ⊢ ( 𝑛 ≠ 𝑗 ↔ 𝑗 ≠ 𝑛 )
8 7 birani ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑗 ≠ 𝑛 )
9 1 cshwshashlem3 ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ≠ 𝑛 ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) ) )
10 9 imp ⊢ ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ≠ 𝑛 ) ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) )
11 4 5 6 8 10 syl13anc ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) )
12 disjsn2 ⊢ ( ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) → ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ )
13 11 12 syl ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ )
14 13 olcd ⊢ ( ( 𝑛 ≠ 𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
15 14 ex ⊢ ( 𝑛 ≠ 𝑗 → ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) ) )
16 3 15 pm2.61ine ⊢ ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
17 16 ralrimivva ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
18 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑊 cyclShift 𝑛 ) = ( 𝑊 cyclShift 𝑗 ) )
19 18 sneqd ⊢ ( 𝑛 = 𝑗 → { ( 𝑊 cyclShift 𝑛 ) } = { ( 𝑊 cyclShift 𝑗 ) } )
20 19 disjor ⊢ ( Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ↔ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
21 17 20 sylibr ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )