Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | repsdf2 13376 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝐴 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴))) |
3 | 1, 2 | sylan2 490 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 = (𝐴 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴))) |
4 | | simp1 1054 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → 𝑊 ∈ Word 𝑉) |
5 | 4 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴)) → 𝑊 ∈ Word 𝑉) |
6 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑊) → (𝑁 ∈ ℕ ↔ (#‘𝑊) ∈
ℕ)) |
7 | 6 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) = 𝑁 → (𝑁 ∈ ℕ ↔ (#‘𝑊) ∈
ℕ)) |
8 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
(0..^(#‘𝑊)) ↔
(#‘𝑊) ∈
ℕ) |
9 | 8 | biimpri 217 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ → 0 ∈ (0..^(#‘𝑊))) |
10 | 7, 9 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) = 𝑁 → (𝑁 ∈ ℕ → 0 ∈
(0..^(#‘𝑊)))) |
11 | 10 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → (𝑁 ∈ ℕ → 0 ∈
(0..^(#‘𝑊)))) |
12 | 11 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → 0 ∈ (0..^(#‘𝑊)))) |
13 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → 0 ∈ (0..^(#‘𝑊)))) |
14 | 13 | imp 444 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴)) → 0 ∈ (0..^(#‘𝑊))) |
15 | | cshw0 13391 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 0) = 𝑊) |
16 | 5, 15 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴)) → (𝑊 cyclShift 0) = 𝑊) |
17 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝑊 cyclShift 𝑛) = (𝑊 cyclShift 0)) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → ((𝑊 cyclShift 𝑛) = 𝑊 ↔ (𝑊 cyclShift 0) = 𝑊)) |
19 | 18 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((0
∈ (0..^(#‘𝑊))
∧ (𝑊 cyclShift 0) =
𝑊) → ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑊) |
20 | 14, 16, 19 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴)) → ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑊) |
21 | | eqeq2 2621 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → ((𝑊 cyclShift 𝑛) = 𝑤 ↔ (𝑊 cyclShift 𝑛) = 𝑊)) |
22 | 21 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑊)) |
23 | 22 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑊) → ∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
24 | 5, 20, 23 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴)) → ∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
25 | 24 | ex 449 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → ∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)) |
26 | 3, 25 | sylbid 229 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 = (𝐴 repeatS 𝑁) → ∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)) |
27 | 26 | 3impia 1253 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
28 | | repsw 13373 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴 repeatS 𝑁) ∈ Word 𝑉) |
29 | 1, 28 | sylan2 490 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝐴 repeatS 𝑁) ∈ Word 𝑉) |
30 | 29 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → (𝐴 repeatS 𝑁) ∈ Word 𝑉) |
31 | | simpll3 1095 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → 𝑊 = (𝐴 repeatS 𝑁)) |
32 | 31 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑛) = ((𝐴 repeatS 𝑁) cyclShift 𝑛)) |
33 | | simp1 1054 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → 𝐴 ∈ 𝑉) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → 𝐴 ∈ 𝑉) |
35 | 1 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → 𝑁 ∈
ℕ0) |
36 | 35 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → 𝑁 ∈
ℕ0) |
37 | | elfzoelz 12339 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (0..^(#‘𝑊)) → 𝑛 ∈ ℤ) |
38 | 37 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → 𝑛 ∈ ℤ) |
39 | | repswcshw 13409 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ) → ((𝐴 repeatS 𝑁) cyclShift 𝑛) = (𝐴 repeatS 𝑁)) |
40 | 34, 36, 38, 39 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → ((𝐴 repeatS 𝑁) cyclShift 𝑛) = (𝐴 repeatS 𝑁)) |
41 | 32, 40 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑛) = (𝐴 repeatS 𝑁)) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑛) = 𝑢 ↔ (𝐴 repeatS 𝑁) = 𝑢)) |
43 | 42 | biimpd 218 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) ∧ 𝑛 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢)) |
44 | 43 | rexlimdva 3013 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) ∧ 𝑢 ∈ Word 𝑉) → (∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢)) |
45 | 44 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢)) |
46 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑤 = (𝐴 repeatS 𝑁) → (𝑤 = 𝑢 ↔ (𝐴 repeatS 𝑁) = 𝑢)) |
47 | 46 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑤 = (𝐴 repeatS 𝑁) → ((∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → 𝑤 = 𝑢) ↔ (∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢))) |
48 | 47 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑤 = (𝐴 repeatS 𝑁) → (∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → 𝑤 = 𝑢) ↔ ∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢))) |
49 | 48 | rspcev 3282 |
. . . . . 6
⊢ (((𝐴 repeatS 𝑁) ∈ Word 𝑉 ∧ ∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → (𝐴 repeatS 𝑁) = 𝑢)) → ∃𝑤 ∈ Word 𝑉∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → 𝑤 = 𝑢)) |
50 | 30, 45, 49 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∃𝑤 ∈ Word 𝑉∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → 𝑤 = 𝑢)) |
51 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑤 = 𝑢 → ((𝑊 cyclShift 𝑛) = 𝑤 ↔ (𝑊 cyclShift 𝑛) = 𝑢)) |
52 | 51 | rexbidv 3034 |
. . . . . 6
⊢ (𝑤 = 𝑢 → (∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢)) |
53 | 52 | reu7 3368 |
. . . . 5
⊢
(∃!𝑤 ∈
Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 ↔ (∃𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 ∧ ∃𝑤 ∈ Word 𝑉∀𝑢 ∈ Word 𝑉(∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑢 → 𝑤 = 𝑢))) |
54 | 27, 50, 53 | sylanbrc 695 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∃!𝑤 ∈ Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
55 | | reusn 4206 |
. . . 4
⊢
(∃!𝑤 ∈
Word 𝑉∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 ↔ ∃𝑟{𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑟}) |
56 | 54, 55 | sylib 207 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∃𝑟{𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑟}) |
57 | | cshwrepswhash1.m |
. . . . 5
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} |
58 | 57 | eqeq1i 2615 |
. . . 4
⊢ (𝑀 = {𝑟} ↔ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑟}) |
59 | 58 | exbii 1764 |
. . 3
⊢
(∃𝑟 𝑀 = {𝑟} ↔ ∃𝑟{𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑟}) |
60 | 56, 59 | sylibr 223 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ∃𝑟 𝑀 = {𝑟}) |
61 | 57 | cshwsex 15645 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → 𝑀 ∈ V) |
62 | 61 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝐴) → 𝑀 ∈ V) |
63 | 3, 62 | syl6bi 242 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 = (𝐴 repeatS 𝑁) → 𝑀 ∈ V)) |
64 | 63 | 3impia 1253 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → 𝑀 ∈ V) |
65 | | hash1snb 13068 |
. . 3
⊢ (𝑀 ∈ V → ((#‘𝑀) = 1 ↔ ∃𝑟 𝑀 = {𝑟})) |
66 | 64, 65 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → ((#‘𝑀) = 1 ↔ ∃𝑟 𝑀 = {𝑟})) |
67 | 60, 66 | mpbird 246 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → (#‘𝑀) = 1) |