Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . . 5
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) |
2 | | erclwwlkn.r |
. . . . 5
⊢ ∼ =
{〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} |
3 | 1, 2 | eclclwwlkn1 26359 |
. . . 4
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) ↔
∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
4 | | rabeq 3166 |
. . . . . . . . . 10
⊢ (𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
6 | | prmnn 15226 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
7 | 6 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ0) |
8 | 7 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
9 | 1 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
10 | 9 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑊 → 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
11 | | clwwlknscsh 26347 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
12 | 8, 10, 11 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
13 | 5, 12 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
14 | 13 | eqeq2d 2620 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
15 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ) |
16 | | clwwlknprop 26300 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁))) |
17 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) ∧ 𝑁 ∈ ℕ) → 𝑥 ∈ Word 𝑉) |
18 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
19 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 = (#‘𝑥) → (𝑁 = 0 ↔ (#‘𝑥) = 0)) |
20 | 19 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑥) = 𝑁 → (𝑁 = 0 ↔ (#‘𝑥) = 0)) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑥) = 𝑁) → (𝑁 = 0 ↔ (#‘𝑥) = 0)) |
22 | | hasheq0 13015 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ Word 𝑉 → ((#‘𝑥) = 0 ↔ 𝑥 = ∅)) |
23 | 21, 22 | sylan9bbr 733 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑁 = 0 ↔ 𝑥 = ∅)) |
24 | 23 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑁 ≠ 0 ↔ 𝑥 ≠ ∅)) |
25 | 24 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ≠ 0 → ((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → 𝑥 ≠ ∅)) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ≠ 0) →
((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → 𝑥 ≠ ∅)) |
27 | 18, 26 | sylbi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → 𝑥 ≠ ∅)) |
28 | 27 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) ∧ 𝑁 ∈ ℕ) → 𝑥 ≠ ∅) |
29 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑥) = 𝑁 ↔ 𝑁 = (#‘𝑥)) |
30 | 29 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑥) = 𝑁 → 𝑁 = (#‘𝑥)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑥) = 𝑁) → 𝑁 = (#‘𝑥)) |
32 | 31 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) ∧ 𝑁 ∈ ℕ) → 𝑁 = (#‘𝑥)) |
33 | 17, 28, 32 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑁 ∈ ℕ → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
35 | 34 | 3adant1 1072 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑁 ∈ ℕ → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
36 | 16, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
37 | 36 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
38 | 9, 37 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
39 | 15, 38 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
40 | 39 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥))) |
41 | | scshwfzeqfzo 13423 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word 𝑉 ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
43 | 42 | eqeq2d 2620 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘{𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
45 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → 𝑉 USGrph 𝐸) |
46 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑥) ∈
ℙ → (#‘𝑥)
∈ (ℤ≥‘2)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (#‘𝑥) ∈
(ℤ≥‘2)) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → (#‘𝑥) ∈
(ℤ≥‘2)) |
49 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) |
50 | | usg2cwwkdifex 26349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ (ℤ≥‘2)
∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) → ∃𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0)) |
51 | 45, 48, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → ∃𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0)) |
52 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift 𝑚)) |
53 | 52 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift 𝑚))) |
54 | 53 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑛 ∈
(0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)) |
55 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ 𝑢 = (𝑥 cyclShift 𝑚))) |
56 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢) |
57 | 55, 56 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢)) |
58 | 57 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑢 → (∃𝑚 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
59 | 54, 58 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
60 | 59 | cbvrabv 3172 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} = {𝑢 ∈ Word 𝑉 ∣ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢} |
61 | 60 | cshwshashnsame 15648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) ∈ ℙ) → (∃𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0) → (#‘{𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥))) |
62 | 61 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → (∃𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0) → (#‘{𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥))) |
63 | 51, 62 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) → (#‘{𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥)) |
64 | 44, 63 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ Word 𝑉 ∧ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ)) ∧ 𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → (#‘𝑈) = (#‘𝑥)) |
65 | 64 | exp41 636 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Word 𝑉 → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥))))) |
66 | 65 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥))))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑥) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥))) |
68 | 67 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑥) → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)))) |
69 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑥) → (𝑁 ∈ ℙ ↔ (#‘𝑥) ∈
ℙ)) |
70 | 69 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑥) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ↔ (𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ))) |
71 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 = (#‘𝑥) → (0..^𝑁) = (0..^(#‘𝑥))) |
72 | 71 | rexeqdv 3122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = (#‘𝑥) → (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |
73 | 72 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑥) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑥) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
75 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑥) → ((#‘𝑈) = 𝑁 ↔ (#‘𝑈) = (#‘𝑥))) |
76 | 74, 75 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑥) → ((𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁) ↔ (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥)))) |
77 | 70, 76 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑥) → (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)) ↔ ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥))))) |
78 | 68, 77 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (#‘𝑥) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥)))))) |
79 | 78 | eqcoms 2618 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑥) = 𝑁 → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥)))))) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑥) = 𝑁) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥)))))) |
81 | 80 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(#‘𝑥)) → ((𝑉 USGrph 𝐸 ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘𝑥)))))) |
82 | 66, 81 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑥) = 𝑁)) → (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)))) |
83 | 16, 82 | mpcom 37 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) |
84 | 9, 83 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁))) |
85 | 84 | impcom 445 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)) |
86 | 43, 85 | sylbid 229 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)) |
87 | 14, 86 | sylbid 229 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)) |
88 | 87 | rexlimdva 3013 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = 𝑁)) |
89 | 88 | com12 32 |
. . . 4
⊢
(∃𝑥 ∈
𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (#‘𝑈) = 𝑁)) |
90 | 3, 89 | syl6bi 242 |
. . 3
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (#‘𝑈) = 𝑁))) |
91 | 90 | pm2.43i 50 |
. 2
⊢ (𝑈 ∈ (𝑊 / ∼ ) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (#‘𝑈) = 𝑁)) |
92 | 91 | com12 32 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 ∈ (𝑊 / ∼ ) →
(#‘𝑈) = 𝑁)) |