This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 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 )