Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. 2
⊢ 𝑥 ∈ V |
2 | | vex 3176 |
. 2
⊢ 𝑦 ∈ V |
3 | | erclwwlk.r |
. . . 4
⊢ ∼ =
{〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} |
4 | 3 | erclwwlkeqlen 26340 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
5 | 3 | erclwwlkeq 26339 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)))) |
6 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → 𝑦 ∈ (𝑉 ClWWalks 𝐸)) |
7 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → 𝑥 ∈ (𝑉 ClWWalks 𝐸)) |
8 | | clwwlkprop 26298 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑦 ∈ Word 𝑉)) |
9 | 8 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝑉 ClWWalks 𝐸) → 𝑦 ∈ Word 𝑉) |
10 | 9 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ (#‘𝑥) = (#‘𝑦)) → 𝑦 ∈ Word 𝑉) |
11 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ (#‘𝑥) = (#‘𝑦)) → (#‘𝑥) = (#‘𝑦)) |
12 | 10, 11 | cshwcshid 13424 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ (#‘𝑥) = (#‘𝑦)) → ((𝑛 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑛)) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚))) |
13 | 12 | expd 451 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ (#‘𝑥) = (#‘𝑦)) → (𝑛 ∈ (0...(#‘𝑦)) → (𝑥 = (𝑦 cyclShift 𝑛) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)))) |
14 | 13 | rexlimdv 3012 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚))) |
15 | 14 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → ((#‘𝑥) = (#‘𝑦) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)))) |
16 | 15 | com23 84 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((#‘𝑥) = (#‘𝑦) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)))) |
17 | 16 | 3impia 1253 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑥) = (#‘𝑦) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚))) |
18 | 17 | imp 444 |
. . . . . . . 8
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)) |
19 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑥 cyclShift 𝑛) = (𝑥 cyclShift 𝑚)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑦 = (𝑥 cyclShift 𝑛) ↔ 𝑦 = (𝑥 cyclShift 𝑚))) |
21 | 20 | cbvrexv 3148 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑚)) |
22 | 18, 21 | sylibr 223 |
. . . . . . 7
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)) |
23 | 6, 7, 22 | 3jca 1235 |
. . . . . 6
⊢ (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) |
24 | 3 | erclwwlkeq 26339 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ 𝑥 ∈ V) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)))) |
25 | 24 | ancoms 468 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)))) |
26 | 23, 25 | syl5ibr 235 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) ∧ (#‘𝑥) = (#‘𝑦)) → 𝑦 ∼ 𝑥)) |
27 | 26 | expd 451 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ((𝑥 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑦 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑥) = (#‘𝑦) → 𝑦 ∼ 𝑥))) |
28 | 5, 27 | sylbid 229 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑥) = (#‘𝑦) → 𝑦 ∼ 𝑥))) |
29 | 4, 28 | mpdd 42 |
. 2
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥)) |
30 | 1, 2, 29 | mp2an 704 |
1
⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥) |