Step |
Hyp |
Ref |
Expression |
1 |
|
cshwrepswhash1.m |
⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } |
2 |
|
repswsymballbi |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) ) |
3 |
2
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) ) |
4 |
|
prmnn |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℙ → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
5 |
4
|
nnge1d |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℙ → 1 ≤ ( ♯ ‘ 𝑊 ) ) |
6 |
|
wrdsymb1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
7 |
5 6
|
sylan2 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
8 |
7
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
9 |
4
|
ad2antlr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
10 |
|
simpr |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) |
11 |
1
|
cshwrepswhash1 |
⊢ ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑀 ) = 1 ) |
12 |
8 9 10 11
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑀 ) = 1 ) |
13 |
12
|
ex |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑀 ) = 1 ) ) |
14 |
3 13
|
sylbird |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = 1 ) ) |
15 |
|
olc |
⊢ ( ( ♯ ‘ 𝑀 ) = 1 → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) |
16 |
14 15
|
syl6com |
⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) ) |
17 |
|
rexnal |
⊢ ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) |
18 |
|
df-ne |
⊢ ( ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ¬ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) |
19 |
18
|
bicomi |
⊢ ( ¬ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) |
20 |
19
|
rexbii |
⊢ ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) |
21 |
17 20
|
bitr3i |
⊢ ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) |
22 |
1
|
cshwshashnsame |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ) ) |
23 |
|
orc |
⊢ ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) |
24 |
22 23
|
syl6com |
⊢ ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) ) |
25 |
21 24
|
sylbi |
⊢ ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) ) |
26 |
16 25
|
pm2.61i |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) |