Step | Hyp | Ref
| Expression |
1 | | erclwwlk.r |
. . . 4
β’ βΌ =
{β¨π’, π€β© β£ (π’ β (ClWWalksβπΊ) β§ π€ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} |
2 | 1 | erclwwlkeqlen 29272 |
. . 3
β’ ((π₯ β V β§ π¦ β V) β (π₯ βΌ π¦ β (β―βπ₯) = (β―βπ¦))) |
3 | 1 | erclwwlkeq 29271 |
. . . 4
β’ ((π₯ β V β§ π¦ β V) β (π₯ βΌ π¦ β (π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)))) |
4 | | simpl2 1193 |
. . . . . . 7
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β π¦ β (ClWWalksβπΊ)) |
5 | | simpl1 1192 |
. . . . . . 7
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β π₯ β (ClWWalksβπΊ)) |
6 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(VtxβπΊ) =
(VtxβπΊ) |
7 | 6 | clwwlkbp 29238 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (ClWWalksβπΊ) β (πΊ β V β§ π¦ β Word (VtxβπΊ) β§ π¦ β β
)) |
8 | 7 | simp2d 1144 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (ClWWalksβπΊ) β π¦ β Word (VtxβπΊ)) |
9 | 8 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β§ (β―βπ₯) = (β―βπ¦)) β π¦ β Word (VtxβπΊ)) |
10 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β§ (β―βπ₯) = (β―βπ¦)) β (β―βπ₯) = (β―βπ¦)) |
11 | 9, 10 | cshwcshid 14778 |
. . . . . . . . . . . . . 14
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β§ (β―βπ₯) = (β―βπ¦)) β ((π β (0...(β―βπ¦)) β§ π₯ = (π¦ cyclShift π)) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π))) |
12 | 11 | expd 417 |
. . . . . . . . . . . . 13
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β§ (β―βπ₯) = (β―βπ¦)) β (π β (0...(β―βπ¦)) β (π₯ = (π¦ cyclShift π) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)))) |
13 | 12 | rexlimdv 3154 |
. . . . . . . . . . . 12
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β§ (β―βπ₯) = (β―βπ¦)) β (βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π))) |
14 | 13 | ex 414 |
. . . . . . . . . . 11
β’ ((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β ((β―βπ₯) = (β―βπ¦) β (βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)))) |
15 | 14 | com23 86 |
. . . . . . . . . 10
β’ ((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ)) β (βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π) β ((β―βπ₯) = (β―βπ¦) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)))) |
16 | 15 | 3impia 1118 |
. . . . . . . . 9
β’ ((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β ((β―βπ₯) = (β―βπ¦) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π))) |
17 | 16 | imp 408 |
. . . . . . . 8
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)) |
18 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π = π β (π₯ cyclShift π) = (π₯ cyclShift π)) |
19 | 18 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π β (π¦ = (π₯ cyclShift π) β π¦ = (π₯ cyclShift π))) |
20 | 19 | cbvrexvw 3236 |
. . . . . . . 8
β’
(βπ β
(0...(β―βπ₯))π¦ = (π₯ cyclShift π) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)) |
21 | 17, 20 | sylibr 233 |
. . . . . . 7
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)) |
22 | 4, 5, 21 | 3jca 1129 |
. . . . . 6
β’ (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β (π¦ β (ClWWalksβπΊ) β§ π₯ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π))) |
23 | 1 | erclwwlkeq 29271 |
. . . . . . 7
β’ ((π¦ β V β§ π₯ β V) β (π¦ βΌ π₯ β (π¦ β (ClWWalksβπΊ) β§ π₯ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)))) |
24 | 23 | ancoms 460 |
. . . . . 6
β’ ((π₯ β V β§ π¦ β V) β (π¦ βΌ π₯ β (π¦ β (ClWWalksβπΊ) β§ π₯ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ₯))π¦ = (π₯ cyclShift π)))) |
25 | 22, 24 | imbitrrid 245 |
. . . . 5
β’ ((π₯ β V β§ π¦ β V) β (((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β§ (β―βπ₯) = (β―βπ¦)) β π¦ βΌ π₯)) |
26 | 25 | expd 417 |
. . . 4
β’ ((π₯ β V β§ π¦ β V) β ((π₯ β (ClWWalksβπΊ) β§ π¦ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ¦))π₯ = (π¦ cyclShift π)) β ((β―βπ₯) = (β―βπ¦) β π¦ βΌ π₯))) |
27 | 3, 26 | sylbid 239 |
. . 3
β’ ((π₯ β V β§ π¦ β V) β (π₯ βΌ π¦ β ((β―βπ₯) = (β―βπ¦) β π¦ βΌ π₯))) |
28 | 2, 27 | mpdd 43 |
. 2
β’ ((π₯ β V β§ π¦ β V) β (π₯ βΌ π¦ β π¦ βΌ π₯)) |
29 | 28 | el2v 3483 |
1
β’ (π₯ βΌ π¦ β π¦ βΌ π₯) |