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

Metamath Proof Explorer

Theorem crctcshtrl

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a trail <. H , Q >. . (Contributed by AV, 14-Mar-2021) (Proof shortened by AV, 30-Oct-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 crctcshtrl 
|- ( ph -> H ( Trails ` 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 crctcshwlk 
 |-  ( ph -> H ( Walks ` G ) Q )
9 crctistrl 
 |-  ( F ( Circuits ` G ) P -> F ( Trails ` G ) P )
10 2 trlf1 
 |-  ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
11 df-f1 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) )
12 iswrdi 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F e. Word dom I )
13 12 anim1i 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) -> ( F e. Word dom I /\ Fun `' F ) )
14 11 13 sylbi 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( F e. Word dom I /\ Fun `' F ) )
15 3 9 10 14 4syl 
 |-  ( ph -> ( F e. Word dom I /\ Fun `' F ) )
16 elfzoelz 
 |-  ( S e. ( 0 ..^ N ) -> S e. ZZ )
17 5 16 syl 
 |-  ( ph -> S e. ZZ )
18 df-3an 
 |-  ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ S e. ZZ ) )
19 15 17 18 sylanbrc 
 |-  ( ph -> ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) )
20 cshinj 
 |-  ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) -> ( H = ( F cyclShift S ) -> Fun `' H ) )
21 19 6 20 mpisyl 
 |-  ( ph -> Fun `' H )
22 istrl 
 |-  ( H ( Trails ` G ) Q <-> ( H ( Walks ` G ) Q /\ Fun `' H ) )
23 8 21 22 sylanbrc 
 |-  ( ph -> H ( Trails ` G ) Q )