Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. 2
⊢ 𝑥 ∈ V |
2 | | vex 3176 |
. 2
⊢ 𝑦 ∈ V |
3 | | vex 3176 |
. 2
⊢ 𝑧 ∈ V |
4 | | erclwwlkn.w |
. . . . . 6
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) |
5 | | erclwwlkn.r |
. . . . . 6
⊢ ∼ =
{〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} |
6 | 4, 5 | erclwwlkneqlen 26352 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
7 | 6 | 3adant3 1074 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (#‘𝑥) = (#‘𝑦))) |
8 | 4, 5 | erclwwlkneqlen 26352 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
9 | 8 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (#‘𝑦) = (#‘𝑧))) |
10 | 4, 5 | erclwwlkneq 26351 |
. . . . . . . 8
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)))) |
11 | 10 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)))) |
12 | 4, 5 | erclwwlkneq 26351 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)))) |
13 | 12 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)))) |
14 | | simpr1 1060 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → 𝑥 ∈ 𝑊) |
15 | | simplr2 1097 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → 𝑧 ∈ 𝑊) |
16 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (𝑦 cyclShift 𝑛) = (𝑦 cyclShift 𝑚)) |
17 | 16 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑚 → (𝑥 = (𝑦 cyclShift 𝑛) ↔ 𝑥 = (𝑦 cyclShift 𝑚))) |
18 | 17 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃𝑛 ∈
(0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚)) |
19 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift 𝑘)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑘 → (𝑦 = (𝑧 cyclShift 𝑛) ↔ 𝑦 = (𝑧 cyclShift 𝑘))) |
21 | 20 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑛 ∈
(0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) ↔ ∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘)) |
22 | | clwwlknprop 26300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑧 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑧) = 𝑁))) |
23 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((#‘𝑧) = 𝑁 ↔ 𝑁 = (#‘𝑧)) |
24 | 23 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((#‘𝑧) = 𝑁 → 𝑁 = (#‘𝑧)) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑧) = 𝑁) → 𝑁 = (#‘𝑧)) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑧 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑧) = 𝑁)) → 𝑁 = (#‘𝑧)) |
27 | 22, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑁 = (#‘𝑧)) |
28 | 27, 4 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑧 ∈ 𝑊 → 𝑁 = (#‘𝑧)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) → 𝑁 = (#‘𝑧)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑁 = (#‘𝑧)) |
31 | 22 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑧 ∈ Word 𝑉) |
32 | 31, 4 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑧 ∈ 𝑊 → 𝑧 ∈ Word 𝑉) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) → 𝑧 ∈ Word 𝑉) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑧 ∈ Word 𝑉) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → 𝑧 ∈ Word 𝑉) |
36 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) |
37 | 35, 36 | cshwcsh2id 13425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
38 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑁 = (#‘𝑧) → (0...𝑁) = (0...(#‘𝑧))) |
39 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝑧) =
(#‘𝑦) →
(0...(#‘𝑧)) =
(0...(#‘𝑦))) |
40 | 39 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((#‘𝑦) =
(#‘𝑧) →
(0...(#‘𝑧)) =
(0...(#‘𝑦))) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) →
(0...(#‘𝑧)) =
(0...(#‘𝑦))) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (0...(#‘𝑧)) = (0...(#‘𝑦))) |
43 | 38, 42 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (0...𝑁) = (0...(#‘𝑦))) |
44 | 43 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (𝑚 ∈ (0...𝑁) ↔ 𝑚 ∈ (0...(#‘𝑦)))) |
45 | 44 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)))) |
46 | 38 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 = (#‘𝑧) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...(#‘𝑧)))) |
47 | 46 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑁 = (#‘𝑧) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) ↔ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)))) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) ↔ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)))) |
49 | 45, 48 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) ↔ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))))) |
50 | 38 | rexeqdv 3122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 = (#‘𝑧) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
52 | 37, 49, 51 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 = (#‘𝑧) ∧ (((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
53 | 30, 52 | mpancom 700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
54 | 53 | expdcom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
55 | 54 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
56 | 55 | expdcom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))) |
57 | 56 | com4t 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))) |
58 | 57 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑦 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))) |
59 | 58 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑚 ∈ (0...𝑁) → (𝑥 = (𝑦 cyclShift 𝑚) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))) |
60 | 59 | imp41 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝑥 ∈
𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
61 | 60 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
63 | 62 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
64 | 21, 63 | syl7bi 244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
65 | 18, 64 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ 𝑧 ∈ 𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
66 | 65 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → (𝑧 ∈ 𝑊 → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))) |
67 | 66 | com15 99 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑛 ∈
(0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → (𝑧 ∈ 𝑊 → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))) |
68 | 67 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))) |
69 | 68 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))) |
70 | 69 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
71 | 70 | com13 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
72 | 71 | 3impia 1253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
73 | 72 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)) |
74 | 14, 15, 73 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → (𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))) |
75 | 4, 5 | erclwwlkneq 26351 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
76 | 75 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))) |
77 | 74, 76 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢
(((((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) ∧ (𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)) |
78 | 77 | exp31 628 |
. . . . . . . . . . . 12
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧)))) |
79 | 78 | com24 93 |
. . . . . . . . . . 11
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))) |
80 | 79 | ex 449 |
. . . . . . . . . 10
⊢
((#‘𝑦) =
(#‘𝑧) →
((#‘𝑥) =
(#‘𝑦) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
81 | 80 | com4t 91 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
82 | 13, 81 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))) |
83 | 82 | com25 97 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
84 | 11, 83 | sylbid 229 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))) |
85 | 9, 84 | mpdd 42 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((#‘𝑥) = (#‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧)))) |
86 | 85 | com24 93 |
. . . 4
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((#‘𝑥) = (#‘𝑦) → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧)))) |
87 | 7, 86 | mpdd 42 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))) |
88 | 87 | impd 446 |
. 2
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)) |
89 | 1, 2, 3, 88 | mp3an 1416 |
1
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) |