Step | Hyp | Ref
| Expression |
1 | | erclwwlksn.w |
. . . . 5
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) |
2 | | erclwwlksn.r |
. . . . 5
⊢ ∼ =
{〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} |
3 | 1, 2 | eclclwwlksn1 26952 |
. . . 4
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) ↔
∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
4 | | rabeq 3192 |
. . . . . . . . . 10
⊢ (𝑊 = (𝑁 ClWWalksN 𝐺) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
6 | | prmnn 15388 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
7 | 6 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ0) |
8 | 1 | eleq2i 2693 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) |
9 | 8 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑊 → 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) |
10 | | clwwlksnscsh 26940 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) → {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
11 | 7, 9, 10 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
12 | 5, 11 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
13 | 12 | eqeq2d 2632 |
. . . . . . 7
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
14 | | simpll 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑥 ∈ Word (Vtx‘𝐺)) |
15 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
16 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 = (#‘𝑥) → (𝑁 = 0 ↔ (#‘𝑥) = 0)) |
17 | 16 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑥) = 𝑁 → (𝑁 = 0 ↔ (#‘𝑥) = 0)) |
18 | | hasheq0 13154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ Word (Vtx‘𝐺) → ((#‘𝑥) = 0 ↔ 𝑥 = ∅)) |
19 | 17, 18 | sylan9bbr 737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → (𝑁 = 0 ↔ 𝑥 = ∅)) |
20 | 19 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → (𝑁 ≠ 0 ↔ 𝑥 ≠ ∅)) |
21 | 20 | biimpcd 239 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ≠ 0 → ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → 𝑥 ≠ ∅)) |
22 | 15, 21 | simplbiim 659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → 𝑥 ≠ ∅)) |
23 | 22 | impcom 446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑥 ≠ ∅) |
24 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → (#‘𝑥) = 𝑁) |
25 | 24 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑁 = (#‘𝑥)) |
26 | 14, 23, 25 | 3jca 1242 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥))) |
27 | 26 | ex 450 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → (𝑁 ∈ ℕ → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
28 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
29 | 28 | clwwlknbp 26885 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁)) |
30 | 27, 29 | syl11 33 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
31 | 8, 30 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℙ → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)))) |
33 | 32 | imp 445 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥))) |
34 | | scshwfzeqfzo 13572 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (#‘𝑥)) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
36 | 35 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
37 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift 𝑚)) |
38 | 37 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift 𝑚))) |
39 | 38 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑛 ∈
(0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)) |
40 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ 𝑢 = (𝑥 cyclShift 𝑚))) |
41 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢) |
42 | 40, 41 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢)) |
43 | 42 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑢 → (∃𝑚 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
44 | 39, 43 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑢 → (∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
45 | 44 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} = {𝑢 ∈ Word (Vtx‘𝐺) ∣ ∃𝑚 ∈ (0..^(#‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢} |
46 | 45 | cshwshash 15811 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) →
((#‘{𝑦 ∈ Word
(Vtx‘𝐺) ∣
∃𝑛 ∈
(0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥) ∨ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) ∧ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → ((#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥) ∨ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1)) |
48 | 47 | orcomd 403 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) ∧ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → ((#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1 ∨ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥))) |
49 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (#‘𝑈) = (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
50 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ↔ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1)) |
51 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = (#‘𝑥) ↔ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥))) |
52 | 50, 51 | orbi12d 746 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)) ↔ ((#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1 ∨ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥)))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) ∧ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → (((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)) ↔ ((#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = 1 ∨ (#‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (#‘𝑥)))) |
54 | 48, 53 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) ∧ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥))) |
55 | 54 | ex 450 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)))) |
56 | 55 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Word (Vtx‘𝐺) → ((#‘𝑥) ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥))))) |
57 | 56 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → ((#‘𝑥) ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥))))) |
58 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (#‘𝑥) → (𝑁 ∈ ℙ ↔ (#‘𝑥) ∈
ℙ)) |
59 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑥) → (0..^𝑁) = (0..^(#‘𝑥))) |
60 | 59 | rexeqdv 3145 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑥) → (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |
61 | 60 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑥) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) |
62 | 61 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑥) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
63 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑥) → ((#‘𝑈) = 𝑁 ↔ (#‘𝑈) = (#‘𝑥))) |
64 | 63 | orbi2d 738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑥) → (((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁) ↔ ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)))) |
65 | 62, 64 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (#‘𝑥) → ((𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁)) ↔ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥))))) |
66 | 58, 65 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = (#‘𝑥) → ((𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) ↔ ((#‘𝑥) ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)))))) |
67 | 66 | eqcoms 2630 |
. . . . . . . . . . . . 13
⊢
((#‘𝑥) = 𝑁 → ((𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) ↔ ((#‘𝑥) ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)))))) |
68 | 67 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → ((𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) ↔ ((#‘𝑥) ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = (#‘𝑥)))))) |
69 | 57, 68 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑥) = 𝑁) → (𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁)))) |
70 | 29, 69 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁)))) |
71 | 70, 1 | eleq2s 2719 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → (𝑁 ∈ ℙ → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁)))) |
72 | 71 | impcom 446 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) |
73 | 36, 72 | sylbid 230 |
. . . . . . 7
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) |
74 | 13, 73 | sylbid 230 |
. . . . . 6
⊢ ((𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) |
75 | 74 | rexlimdva 3031 |
. . . . 5
⊢ (𝑁 ∈ ℙ →
(∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) |
76 | 75 | com12 32 |
. . . 4
⊢
(∃𝑥 ∈
𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (𝑁 ∈ ℙ → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁))) |
77 | 3, 76 | syl6bi 243 |
. . 3
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) → (𝑁 ∈ ℙ →
((#‘𝑈) = 1 ∨
(#‘𝑈) = 𝑁)))) |
78 | 77 | pm2.43i 52 |
. 2
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑁 ∈ ℙ →
((#‘𝑈) = 1 ∨
(#‘𝑈) = 𝑁))) |
79 | 78 | impcom 446 |
1
⊢ ((𝑁 ∈ ℙ ∧ 𝑈 ∈ (𝑊 / ∼ )) →
((#‘𝑈) = 1 ∨
(#‘𝑈) = 𝑁)) |