Metamath Proof Explorer

Theorem cshwrepswhash1

Description: The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018) (Revised by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m ⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshwrepswhash1 ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ♯ ‘ 𝑀 ) = 1 )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 repsdf2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) )
4 2 3 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) )
5 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → 𝑊 ∈ Word 𝑉 )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) → 𝑊 ∈ Word 𝑉 )
7 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
8 7 eqcoms ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
9 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
10 9 biimpri ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 8 10 biimtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12 11 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
13 12 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
14 13 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
15 14 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 cshw0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )
17 6 16 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) → ( 𝑊 cyclShift 0 ) = 𝑊 )
18 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑊 cyclShift 𝑛 ) = ( 𝑊 cyclShift 0 ) )
19 18 eqeq1d ⊢ ( 𝑛 = 0 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑊 ↔ ( 𝑊 cyclShift 0 ) = 𝑊 ) )
20 19 rspcev ⊢ ( ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 0 ) = 𝑊 ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 )
21 15 17 20 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 )
22 eqeq2 ⊢ ( 𝑤 = 𝑊 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) )
23 22 rexbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) )
24 23 rspcev ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) → ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
25 6 21 24 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) ) → ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
26 25 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) )
27 4 26 sylbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) → ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) )
28 27 3impia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
29 repsw ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
30 2 29 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
31 30 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
32 simpll3 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 = ( 𝐴 repeatS 𝑁 ) )
33 32 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑛 ) = ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) )
34 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝐴 ∈ 𝑉 )
35 34 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐴 ∈ 𝑉 )
36 2 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝑁 ∈ ℕ0 )
37 36 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℕ0 )
38 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑛 ∈ ℤ )
39 38 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑛 ∈ ℤ )
40 repswcshw ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
41 35 37 39 40 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
42 33 41 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
43 42 eqeq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑛 ) = 𝑢 ↔ ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
44 43 biimpd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
45 44 rexlimdva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
46 45 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
47 eqeq1 ⊢ ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( 𝑤 = 𝑢 ↔ ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
48 47 imbi2d ⊢ ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → 𝑤 = 𝑢 ) ↔ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) )
49 48 ralbidv ⊢ ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → 𝑤 = 𝑢 ) ↔ ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) )
50 49 rspcev ⊢ ( ( ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 ∧ ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) → ∃ 𝑤 ∈ Word 𝑉 ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → 𝑤 = 𝑢 ) )
51 31 46 50 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑤 ∈ Word 𝑉 ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → 𝑤 = 𝑢 ) )
52 eqeq2 ⊢ ( 𝑤 = 𝑢 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( 𝑊 cyclShift 𝑛 ) = 𝑢 ) )
53 52 rexbidv ⊢ ( 𝑤 = 𝑢 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 ) )
54 53 reu7 ⊢ ( ∃! 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( ∃ 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ∧ ∃ 𝑤 ∈ Word 𝑉 ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → 𝑤 = 𝑢 ) ) )
55 28 51 54 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃! 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
56 reusn ⊢ ( ∃! 𝑤 ∈ Word 𝑉 ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
57 55 56 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
58 1 eqeq1i ⊢ ( 𝑀 = { 𝑟 } ↔ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
59 58 exbii ⊢ ( ∃ 𝑟 𝑀 = { 𝑟 } ↔ ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
60 57 59 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑟 𝑀 = { 𝑟 } )
61 1 cshwsex ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑀 ∈ V )
62 61 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝐴 ) → 𝑀 ∈ V )
63 4 62 biimtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) → 𝑀 ∈ V ) )
64 63 3impia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝑀 ∈ V )
65 hash1snb ⊢ ( 𝑀 ∈ V → ( ( ♯ ‘ 𝑀 ) = 1 ↔ ∃ 𝑟 𝑀 = { 𝑟 } ) )
66 64 65 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ( ♯ ‘ 𝑀 ) = 1 ↔ ∃ 𝑟 𝑀 = { 𝑟 } ) )
67 60 66 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ♯ ‘ 𝑀 ) = 1 )