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=VtxG
crctcsh.i I=iEdgG
crctcsh.d φFCircuitsGP
crctcsh.n N=F
crctcsh.s φS0..^N
crctcsh.h H=FcyclShiftS
crctcsh.q Q=x0NifxNSPx+SPx+S-N
Assertion crctcshwlk φHWalksGQ

Proof

Step Hyp Ref Expression
1 crctcsh.v V=VtxG
2 crctcsh.i I=iEdgG
3 crctcsh.d φFCircuitsGP
4 crctcsh.n N=F
5 crctcsh.s φS0..^N
6 crctcsh.h H=FcyclShiftS
7 crctcsh.q Q=x0NifxNSPx+SPx+S-N
8 1 2 3 4 5 6 7 crctcshlem4 φS=0H=FQ=P
9 crctistrl FCircuitsGPFTrailsGP
10 trliswlk FTrailsGPFWalksGP
11 3 9 10 3syl φFWalksGP
12 breq12 H=FQ=PHWalksGQFWalksGP
13 11 12 syl5ibrcom φH=FQ=PHWalksGQ
14 13 adantr φS=0H=FQ=PHWalksGQ
15 8 14 mpd φS=0HWalksGQ
16 1 2 3 4 5 6 7 crctcshwlkn0 φS0HWalksGQ
17 15 16 pm2.61dane φHWalksGQ