Metamath Proof Explorer

Theorem cshwshashlem3

Description: If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (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 cshwshashlem3 ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ≠ 𝐿 ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
2 elfzoelz ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐾 ∈ ℤ )
3 2 zred ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐾 ∈ ℝ )
4 elfzoelz ⊢ ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℤ )
5 4 zred ⊢ ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℝ )
6 lttri2 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝐾 ≠ 𝐿 ↔ ( 𝐾 < 𝐿 ∨ 𝐿 < 𝐾 ) ) )
7 3 5 6 syl2anr ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐾 ≠ 𝐿 ↔ ( 𝐾 < 𝐿 ∨ 𝐿 < 𝐾 ) ) )
8 1 cshwshashlem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 < 𝐿 ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )
9 8 com12 ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 < 𝐿 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )
10 9 3expia ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐾 < 𝐿 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) ) )
11 1 cshwshashlem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 < 𝐾 ) → ( 𝑊 cyclShift 𝐾 ) ≠ ( 𝑊 cyclShift 𝐿 ) ) )
12 11 imp ⊢ ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 < 𝐾 ) ) → ( 𝑊 cyclShift 𝐾 ) ≠ ( 𝑊 cyclShift 𝐿 ) )
13 12 necomd ⊢ ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 < 𝐾 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) )
14 13 expcom ⊢ ( ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 < 𝐾 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )
15 14 3expia ⊢ ( ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 < 𝐾 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) ) )
16 15 ancoms ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 < 𝐾 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) ) )
17 10 16 jaod ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐾 < 𝐿 ∨ 𝐿 < 𝐾 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) ) )
18 7 17 sylbid ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐾 ≠ 𝐿 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) ) )
19 18 3impia ⊢ ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ≠ 𝐿 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )
20 19 com12 ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ≠ 𝐿 ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )