# 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 biimpi ( 𝑛𝑗𝑗𝑛 )
9 8 adantr ( ( 𝑛𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑗𝑛 )
10 1 cshwshashlem3 ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗𝑛 ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) ) )
11 10 imp ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗𝑛 ) ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) )
12 4 5 6 9 11 syl13anc ( ( 𝑛𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) )
13 disjsn2 ( ( 𝑊 cyclShift 𝑛 ) ≠ ( 𝑊 cyclShift 𝑗 ) → ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ )
14 12 13 syl ( ( 𝑛𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ )
15 14 olcd ( ( 𝑛𝑗 ∧ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
16 15 ex ( 𝑛𝑗 → ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) ) )
17 3 16 pm2.61ine ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
18 17 ralrimivva ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
19 oveq2 ( 𝑛 = 𝑗 → ( 𝑊 cyclShift 𝑛 ) = ( 𝑊 cyclShift 𝑗 ) )
20 19 sneqd ( 𝑛 = 𝑗 → { ( 𝑊 cyclShift 𝑛 ) } = { ( 𝑊 cyclShift 𝑗 ) } )
21 20 disjor ( Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ↔ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑛 = 𝑗 ∨ ( { ( 𝑊 cyclShift 𝑛 ) } ∩ { ( 𝑊 cyclShift 𝑗 ) } ) = ∅ ) )
22 18 21 sylibr ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )