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\leftrightarrow 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$$