Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. 2
⊢ 𝑥 ∈ V |
2 | | vex 3176 |
. 2
⊢ 𝑦 ∈ V |
3 | | vex 3176 |
. 2
⊢ 𝑧 ∈ V |
4 | | erclwwlks.r |
. . . . . 6
⊢ ∼ =
{〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalkS‘𝐺) ∧ 𝑤 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} |
5 | 4 | erclwwlkseqlen 41240 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
6 | 5 | 3adant3 1074 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
7 | 4 | erclwwlkseqlen 41240 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
8 | 7 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
9 | 4 | erclwwlkseq 41239 |
. . . . . . . 8
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)))) |
10 | 9 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)))) |
11 | 4 | erclwwlkseq 41239 |
. . . . . . . . . 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 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
22 | 21 | clwwlkbp 41191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ (ClWWalkS‘𝐺) → (𝐺 ∈ V ∧ 𝑧 ∈ Word (Vtx‘𝐺) ∧ 𝑧 ≠ ∅)) |
23 | 22 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ (ClWWalkS‘𝐺) → 𝑧 ∈ Word (Vtx‘𝐺)) |
24 | 23 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑧 ∈ Word (Vtx‘𝐺)) |
25 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) |
26 | 24, 25 | cshwcsh2id 13425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
27 | 26 | exp5l 644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑚 ∈ (0...(#‘𝑦)) → (𝑥 = (𝑦 cyclShift 𝑚) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
28 | 27 | imp41 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝑥 ∈
(ClWWalkS‘𝐺) ∧
𝑦 ∈
(ClWWalkS‘𝐺)) ∧
𝑧 ∈
(ClWWalkS‘𝐺)) ∧
((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
29 | 28 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑥 ∈
(ClWWalkS‘𝐺) ∧
𝑦 ∈
(ClWWalkS‘𝐺)) ∧
𝑧 ∈
(ClWWalkS‘𝐺)) ∧
((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑥 ∈
(ClWWalkS‘𝐺) ∧
𝑦 ∈
(ClWWalkS‘𝐺)) ∧
𝑧 ∈
(ClWWalkS‘𝐺)) ∧
((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦))) ∧ 𝑚 ∈ (0...(#‘𝑦))) → (𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
31 | 30 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
32 | 20, 31 | syl7bi 244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
33 | 17, 32 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) ∧ 𝑧 ∈ (ClWWalkS‘𝐺)) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
34 | 33 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → (𝑧 ∈ (ClWWalkS‘𝐺) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
35 | 34 | com15 99 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑛 ∈
(0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → (𝑧 ∈ (ClWWalkS‘𝐺) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))) |
36 | 35 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
37 | 36 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))) |
38 | 37 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
39 | 38 | com13 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺)) → (∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
40 | 39 | 3impia 1253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
41 | 40 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
42 | 13, 14, 41 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
43 | 4 | erclwwlkseq 41239 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
44 | 43 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))) |
45 | 42, 44 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)) |
46 | 45 | exp31 628 |
. . . . . . . . . . . 12
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)))) |
47 | 46 | com24 93 |
. . . . . . . . . . 11
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))) |
48 | 47 | ex 449 |
. . . . . . . . . 10
⊢
((#‘𝑦) =
(#‘𝑧) →
((#‘𝑥) =
(#‘𝑦) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
49 | 48 | com4t 91 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalkS‘𝐺) ∧ 𝑦 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
50 | 12, 49 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
51 | 50 | com25 97 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑦 ∈ (ClWWalkS‘𝐺) ∧ 𝑧 ∈ (ClWWalkS‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
52 | 10, 51 | sylbid 229 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
53 | 8, 52 | mpdd 42 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧)))) |
54 | 53 | com24 93 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑥) = (#‘𝑦) → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧)))) |
55 | 6, 54 | mpdd 42 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))) |
56 | 55 | impd 446 |
. 2
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)) |
57 | 1, 2, 3, 56 | mp3an 1416 |
1
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) |