Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. 2
⊢ 𝑥 ∈ V |
2 | | vex 3176 |
. 2
⊢ 𝑦 ∈ V |
3 | | vex 3176 |
. 2
⊢ 𝑧 ∈ V |
4 | | erclwwlk.r |
. . . . . 6
⊢ ∼ =
{〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} |
5 | 4 | erclwwlkeqlen 26340 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
6 | 5 | 3adant3 1074 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
7 | 4 | erclwwlkeqlen 26340 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
8 | 7 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
9 | 4 | erclwwlkeq 26339 |
. . . . . . . 8
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)))) |
10 | 9 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)))) |
11 | 4 | erclwwlkeq 26339 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)))) |
12 | 11 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)))) |
13 | | simpr1 1060 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → 𝑥 ∈ (𝑉 ClWWalks 𝐸)) |
14 | | simplr2 1097 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → 𝑧 ∈ (𝑉 ClWWalks 𝐸)) |
15 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (𝑦 cyclShift 𝑛) = (𝑦 cyclShift 𝑚)) |
16 | 15 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑚 → (𝑥 = (𝑦 cyclShift 𝑛) ↔ 𝑥 = (𝑦 cyclShift 𝑚))) |
17 | 16 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃𝑛 ∈
(0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑚)) |
18 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift 𝑘)) |
19 | 18 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑘 → (𝑦 = (𝑧 cyclShift 𝑛) ↔ 𝑦 = (𝑧 cyclShift 𝑘))) |
20 | 19 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑛 ∈
(0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) ↔ ∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘)) |
21 | | clwwlkprop 26298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑧 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑧 ∈ Word 𝑉)) |
22 | 21 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈ (𝑉 ClWWalks 𝐸) → 𝑧 ∈ Word 𝑉) |
23 | 22 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑧 ∈ Word 𝑉) |
24 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) |
25 | 23, 24 | cshwcsh2id 13425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
26 | 25 | expdcom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
27 | 26 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
28 | 27 | expdcom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ (0...(#‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
29 | 28 | com4t 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...(#‘𝑦))) → ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑚 ∈ (0...(#‘𝑦)) → ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
31 | 30 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑚 ∈ (0...(#‘𝑦)) → (𝑥 = (𝑦 cyclShift 𝑚) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
32 | 31 | imp41 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝑥 ∈
(𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
33 | 32 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑥 ∈
(𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
35 | 34 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
36 | 20, 35 | syl7bi 244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
37 | 17, 36 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
38 | 37 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → (𝑧 ∈ (𝑉 ClWWalks 𝐸) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
39 | 38 | com15 99 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑛 ∈
(0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → (𝑧 ∈ (𝑉 ClWWalks 𝐸) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
40 | 39 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
41 | 40 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
42 | 41 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
43 | 42 | com13 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
44 | 43 | 3impia 1253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
45 | 44 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
46 | 13, 14, 45 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
47 | 4 | erclwwlkeq 26339 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
48 | 47 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
49 | 46, 48 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)) |
50 | 49 | exp31 628 |
. . . . . . . . . . . 12
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)))) |
51 | 50 | com24 93 |
. . . . . . . . . . 11
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))) |
52 | 51 | ex 449 |
. . . . . . . . . 10
⊢
((#‘𝑦) =
(#‘𝑧) →
((#‘𝑥) =
(#‘𝑦) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
53 | 52 | com4t 91 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
54 | 12, 53 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
55 | 54 | com25 97 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑧 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
56 | 10, 55 | sylbid 229 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
57 | 8, 56 | mpdd 42 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧)))) |
58 | 57 | com24 93 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑥) = (#‘𝑦) → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧)))) |
59 | 6, 58 | mpdd 42 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))) |
60 | 59 | impd 446 |
. 2
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)) |
61 | 1, 2, 3, 60 | mp3an 1416 |
1
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) |