Metamath Proof Explorer


Theorem crctcshwlk

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 V = Vtx G
crctcsh.i I = iEdg G
crctcsh.d φ F Circuits G P
crctcsh.n N = F
crctcsh.s φ S 0 ..^ N
crctcsh.h H = F cyclShift S
crctcsh.q Q = x 0 N if x N S P x + S P x + S - N
Assertion crctcshwlk φ H Walks G Q

Proof

Step Hyp Ref Expression
1 crctcsh.v V = Vtx G
2 crctcsh.i I = iEdg G
3 crctcsh.d φ F Circuits G P
4 crctcsh.n N = F
5 crctcsh.s φ S 0 ..^ N
6 crctcsh.h H = F cyclShift S
7 crctcsh.q Q = x 0 N if x N S P x + S P x + S - N
8 1 2 3 4 5 6 7 crctcshlem4 φ S = 0 H = F Q = P
9 crctistrl F Circuits G P F Trails G P
10 trliswlk F Trails G P F Walks G P
11 3 9 10 3syl φ F Walks G P
12 breq12 H = F Q = P H Walks G Q F Walks G P
13 11 12 syl5ibrcom φ H = F Q = P H Walks G Q
14 13 adantr φ S = 0 H = F Q = P H Walks G Q
15 8 14 mpd φ S = 0 H Walks G Q
16 1 2 3 4 5 6 7 crctcshwlkn0 φ S 0 H Walks G Q
17 15 16 pm2.61dane φ H Walks G Q