crctcshwlk

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

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

Metamath Proof Explorer