# 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}=\mathrm{Vtx}\left({G}\right)$
crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
crctcsh.n ${⊢}{N}=\left|{F}\right|$
crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
Assertion crctcshwlk ${⊢}{\phi }\to {H}\mathrm{Walks}\left({G}\right){Q}$

### Proof

Step Hyp Ref Expression
1 crctcsh.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
4 crctcsh.n ${⊢}{N}=\left|{F}\right|$
5 crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
6 crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
7 crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
8 1 2 3 4 5 6 7 crctcshlem4 ${⊢}\left({\phi }\wedge {S}=0\right)\to \left({H}={F}\wedge {Q}={P}\right)$
9 crctistrl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
10 trliswlk ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
11 3 9 10 3syl ${⊢}{\phi }\to {F}\mathrm{Walks}\left({G}\right){P}$
12 breq12 ${⊢}\left({H}={F}\wedge {Q}={P}\right)\to \left({H}\mathrm{Walks}\left({G}\right){Q}↔{F}\mathrm{Walks}\left({G}\right){P}\right)$
13 11 12 syl5ibrcom ${⊢}{\phi }\to \left(\left({H}={F}\wedge {Q}={P}\right)\to {H}\mathrm{Walks}\left({G}\right){Q}\right)$
14 13 adantr ${⊢}\left({\phi }\wedge {S}=0\right)\to \left(\left({H}={F}\wedge {Q}={P}\right)\to {H}\mathrm{Walks}\left({G}\right){Q}\right)$
15 8 14 mpd ${⊢}\left({\phi }\wedge {S}=0\right)\to {H}\mathrm{Walks}\left({G}\right){Q}$
16 1 2 3 4 5 6 7 crctcshwlkn0 ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {H}\mathrm{Walks}\left({G}\right){Q}$
17 15 16 pm2.61dane ${⊢}{\phi }\to {H}\mathrm{Walks}\left({G}\right){Q}$