Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . 4
β’ (π’ = π β (π’ β (ClWWalksβπΊ) β π β (ClWWalksβπΊ))) |
2 | 1 | adantr 482 |
. . 3
β’ ((π’ = π β§ π€ = π) β (π’ β (ClWWalksβπΊ) β π β (ClWWalksβπΊ))) |
3 | | eleq1 2822 |
. . . 4
β’ (π€ = π β (π€ β (ClWWalksβπΊ) β π β (ClWWalksβπΊ))) |
4 | 3 | adantl 483 |
. . 3
β’ ((π’ = π β§ π€ = π) β (π€ β (ClWWalksβπΊ) β π β (ClWWalksβπΊ))) |
5 | | fveq2 6846 |
. . . . . 6
β’ (π€ = π β (β―βπ€) = (β―βπ)) |
6 | 5 | oveq2d 7377 |
. . . . 5
β’ (π€ = π β (0...(β―βπ€)) = (0...(β―βπ))) |
7 | 6 | adantl 483 |
. . . 4
β’ ((π’ = π β§ π€ = π) β (0...(β―βπ€)) = (0...(β―βπ))) |
8 | | simpl 484 |
. . . . 5
β’ ((π’ = π β§ π€ = π) β π’ = π) |
9 | | oveq1 7368 |
. . . . . 6
β’ (π€ = π β (π€ cyclShift π) = (π cyclShift π)) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π’ = π β§ π€ = π) β (π€ cyclShift π) = (π cyclShift π)) |
11 | 8, 10 | eqeq12d 2749 |
. . . 4
β’ ((π’ = π β§ π€ = π) β (π’ = (π€ cyclShift π) β π = (π cyclShift π))) |
12 | 7, 11 | rexeqbidv 3319 |
. . 3
β’ ((π’ = π β§ π€ = π) β (βπ β (0...(β―βπ€))π’ = (π€ cyclShift π) β βπ β (0...(β―βπ))π = (π cyclShift π))) |
13 | 2, 4, 12 | 3anbi123d 1437 |
. 2
β’ ((π’ = π β§ π€ = π) β ((π’ β (ClWWalksβπΊ) β§ π€ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π)) β (π β (ClWWalksβπΊ) β§ π β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ))π = (π cyclShift π)))) |
14 | | erclwwlk.r |
. 2
β’ βΌ =
{β¨π’, π€β© β£ (π’ β (ClWWalksβπΊ) β§ π€ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} |
15 | 13, 14 | brabga 5495 |
1
β’ ((π β π β§ π β π) β (π βΌ π β (π β (ClWWalksβπΊ) β§ π β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ))π = (π cyclShift π)))) |