| Step | Hyp | Ref
| Expression |
| 1 | | erclwwlkn.w |
. . . . 5
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) |
| 2 | | erclwwlkn.r |
. . . . 5
⊢ ∼ =
{〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} |
| 3 | 1, 2 | eclclwwlkn1 30094 |
. . . 4
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) ↔
∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
| 4 | | rabeq 3451 |
. . . . . . . . . 10
⊢ (𝑊 = (𝑁 ClWWalksN 𝐺) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 6 | | prmnn 16711 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
| 7 | 6 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ0) |
| 8 | 7 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
| 9 | 1 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) |
| 10 | 9 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑊 → 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) |
| 11 | | clwwlknscsh 30081 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (𝑁 ClWWalksN 𝐺)) → {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 12 | 8, 10, 11 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 13 | 5, 12 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 14 | 13 | eqeq2d 2748 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
| 15 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ) |
| 16 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑥 ∈ Word (Vtx‘𝐺)) |
| 17 | | elnnne0 12540 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
| 18 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 = (♯‘𝑥) → (𝑁 = 0 ↔ (♯‘𝑥) = 0)) |
| 19 | 18 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑥) =
𝑁 → (𝑁 = 0 ↔ (♯‘𝑥) = 0)) |
| 20 | | hasheq0 14402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ Word (Vtx‘𝐺) → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅)) |
| 21 | 19, 20 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → (𝑁 = 0 ↔ 𝑥 = ∅)) |
| 22 | 21 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → (𝑁 ≠ 0 ↔ 𝑥 ≠ ∅)) |
| 23 | 22 | biimpcd 249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ≠ 0 → ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → 𝑥 ≠ ∅)) |
| 24 | 17, 23 | simplbiim 504 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → 𝑥 ≠ ∅)) |
| 25 | 24 | impcom 407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑥 ≠ ∅) |
| 26 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → (♯‘𝑥) = 𝑁) |
| 27 | 26 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑁 = (♯‘𝑥)) |
| 28 | 16, 25, 27 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥))) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → (𝑁 ∈ ℕ → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥)))) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 31 | 30 | clwwlknbp 30054 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁)) |
| 32 | 29, 31 | syl11 33 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥)))) |
| 33 | 9, 32 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥)))) |
| 34 | 15, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑥 ∈ 𝑊 → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥)))) |
| 35 | 34 | imp 406 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥))) |
| 36 | | scshwfzeqfzo 14865 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = (♯‘𝑥)) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)}) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) |
| 39 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
| 40 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) → 𝐺 ∈
UMGraph) |
| 41 | | prmuz2 16733 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑥)
∈ ℙ → (♯‘𝑥) ∈
(ℤ≥‘2)) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ UMGraph ∧
(♯‘𝑥) ∈
ℙ) → (♯‘𝑥) ∈
(ℤ≥‘2)) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) →
(♯‘𝑥) ∈
(ℤ≥‘2)) |
| 44 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) → 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) |
| 45 | | umgr2cwwkdifex 30084 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ UMGraph ∧
(♯‘𝑥) ∈
(ℤ≥‘2) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) → ∃𝑖 ∈ (0..^(♯‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0)) |
| 46 | 40, 43, 44, 45 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) →
∃𝑖 ∈
(0..^(♯‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0)) |
| 47 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift 𝑚)) |
| 48 | 47 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift 𝑚))) |
| 49 | 48 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑛 ∈
(0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)) |
| 50 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ 𝑢 = (𝑥 cyclShift 𝑚))) |
| 51 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢) |
| 52 | 50, 51 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑢 → (𝑦 = (𝑥 cyclShift 𝑚) ↔ (𝑥 cyclShift 𝑚) = 𝑢)) |
| 53 | 52 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑢 → (∃𝑚 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑚) ↔ ∃𝑚 ∈ (0..^(♯‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
| 54 | 49, 53 | bitrid 283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0..^(♯‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢)) |
| 55 | 54 | cbvrabv 3447 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈
(0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} = {𝑢 ∈ Word (Vtx‘𝐺) ∣ ∃𝑚 ∈ (0..^(♯‘𝑥))(𝑥 cyclShift 𝑚) = 𝑢} |
| 56 | 55 | cshwshashnsame 17141 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) ∈ ℙ) →
(∃𝑖 ∈
(0..^(♯‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0) → (♯‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈
(0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (♯‘𝑥))) |
| 57 | 56 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) →
(∃𝑖 ∈
(0..^(♯‘𝑥))(𝑥‘𝑖) ≠ (𝑥‘0) → (♯‘{𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈
(0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (♯‘𝑥))) |
| 58 | 46, 57 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) →
(♯‘{𝑦 ∈
Word (Vtx‘𝐺) ∣
∃𝑛 ∈
(0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) = (♯‘𝑥)) |
| 59 | 39, 58 | sylan9eqr 2799 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ Word (Vtx‘𝐺) ∧ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺)) ∧ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ)) ∧ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) → (♯‘𝑈) = (♯‘𝑥)) |
| 60 | 59 | exp41 434 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Word (Vtx‘𝐺) → (𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥))))) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → (𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥))))) |
| 62 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (♯‘𝑥) → (𝑁 ClWWalksN 𝐺) = ((♯‘𝑥) ClWWalksN 𝐺)) |
| 63 | 62 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (♯‘𝑥) → (𝑥 ∈ (𝑁 ClWWalksN 𝐺) ↔ 𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺))) |
| 64 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (♯‘𝑥) → (𝑁 ∈ ℙ ↔ (♯‘𝑥) ∈
ℙ)) |
| 65 | 64 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (♯‘𝑥) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ↔ (𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈
ℙ))) |
| 66 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = (♯‘𝑥) → (0..^𝑁) = (0..^(♯‘𝑥))) |
| 67 | 66 | rexeqdv 3327 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (♯‘𝑥) → (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |
| 68 | 67 | rabbidv 3444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (♯‘𝑥) → {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)}) |
| 69 | 68 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (♯‘𝑥) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} ↔ 𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)})) |
| 70 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (♯‘𝑥) → ((♯‘𝑈) = 𝑁 ↔ (♯‘𝑈) = (♯‘𝑥))) |
| 71 | 69, 70 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (♯‘𝑥) → ((𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁) ↔ (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥)))) |
| 72 | 65, 71 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (♯‘𝑥) → (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)) ↔ ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥))))) |
| 73 | 63, 72 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = (♯‘𝑥) → ((𝑥 ∈ (𝑁 ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥)))))) |
| 74 | 73 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑥) =
𝑁 → ((𝑥 ∈ (𝑁 ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥)))))) |
| 75 | 74 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → ((𝑥 ∈ (𝑁 ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁))) ↔ (𝑥 ∈ ((♯‘𝑥) ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ (♯‘𝑥) ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = (♯‘𝑥)))))) |
| 76 | 61, 75 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑥) = 𝑁) → (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)))) |
| 77 | 31, 76 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑁 ClWWalksN 𝐺) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁))) |
| 78 | 77, 1 | eleq2s 2859 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁))) |
| 79 | 78 | impcom 407 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)) |
| 80 | 38, 79 | sylbid 240 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)) |
| 81 | 14, 80 | sylbid 240 |
. . . . . 6
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑥 ∈ 𝑊) → (𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)) |
| 82 | 81 | rexlimdva 3155 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) →
(∃𝑥 ∈ 𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → (♯‘𝑈) = 𝑁)) |
| 83 | 82 | com12 32 |
. . . 4
⊢
(∃𝑥 ∈
𝑊 𝑈 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)} → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (♯‘𝑈) = 𝑁)) |
| 84 | 3, 83 | biimtrdi 253 |
. . 3
⊢ (𝑈 ∈ (𝑊 / ∼ ) → (𝑈 ∈ (𝑊 / ∼ ) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) →
(♯‘𝑈) = 𝑁))) |
| 85 | 84 | pm2.43i 52 |
. 2
⊢ (𝑈 ∈ (𝑊 / ∼ ) → ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) →
(♯‘𝑈) = 𝑁)) |
| 86 | 85 | com12 32 |
1
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 ∈ (𝑊 / ∼ ) →
(♯‘𝑈) = 𝑁)) |