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 ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
Assertion cshwrepswhash1 ⊢ A ∈ V ∧ N ∈ ℕ ∧ W = A repeatS N → M = 1

Proof

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