Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | crctcsh.v | |
|
crctcsh.i | |
||
crctcsh.d | |
||
crctcsh.n | |
||
crctcsh.s | |
||
crctcsh.h | |
||
crctcsh.q | |
||
Assertion | crctcshwlk | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crctcsh.v | |
|
2 | crctcsh.i | |
|
3 | crctcsh.d | |
|
4 | crctcsh.n | |
|
5 | crctcsh.s | |
|
6 | crctcsh.h | |
|
7 | crctcsh.q | |
|
8 | 1 2 3 4 5 6 7 | crctcshlem4 | |
9 | crctistrl | |
|
10 | trliswlk | |
|
11 | 3 9 10 | 3syl | |
12 | breq12 | |
|
13 | 11 12 | syl5ibrcom | |
14 | 13 | adantr | |
15 | 8 14 | mpd | |
16 | 1 2 3 4 5 6 7 | crctcshwlkn0 | |
17 | 15 16 | pm2.61dane | |