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	|- ( ph -> F ( Circuits ` G ) P )
	crctcsh.n	|- N = ( # ` F )
	crctcsh.s	|- ( ph -> S e. ( 0 ..^ N ) )
	crctcsh.h	|- H = ( F cyclShift S )
	crctcsh.q	|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
Assertion	crctcshwlk	|- ( ph -> H ( Walks ` G ) Q )

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	|- V = ( Vtx ` G )
2		crctcsh.i	|- I = ( iEdg ` G )
3		crctcsh.d	|- ( ph -> F ( Circuits ` G ) P )
4		crctcsh.n	|- N = ( # ` F )
5		crctcsh.s	|- ( ph -> S e. ( 0 ..^ N ) )
6		crctcsh.h	|- H = ( F cyclShift S )
7		crctcsh.q	|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
8	1 2 3 4 5 6 7	crctcshlem4	|- ( ( ph /\ 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	|- ( ph -> F ( Walks ` G ) P )
12		breq12	|- ( ( H = F /\ Q = P ) -> ( H ( Walks ` G ) Q <-> F ( Walks ` G ) P ) )
13	11 12	syl5ibrcom	|- ( ph -> ( ( H = F /\ Q = P ) -> H ( Walks ` G ) Q ) )
14	13	adantr	|- ( ( ph /\ S = 0 ) -> ( ( H = F /\ Q = P ) -> H ( Walks ` G ) Q ) )
15	8 14	mpd	|- ( ( ph /\ S = 0 ) -> H ( Walks ` G ) Q )
16	1 2 3 4 5 6 7	crctcshwlkn0	|- ( ( ph /\ S =/= 0 ) -> H ( Walks ` G ) Q )
17	15 16	pm2.61dane	|- ( ph -> H ( Walks ` G ) Q )