| 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 |
10 14
|
syl |
|- ( F ( Trails ` G ) P -> ( F e. Word dom I /\ Fun `' F ) ) |
| 16 |
3 9 15
|
3syl |
|- ( ph -> ( F e. Word dom I /\ Fun `' F ) ) |
| 17 |
|
elfzoelz |
|- ( S e. ( 0 ..^ N ) -> S e. ZZ ) |
| 18 |
5 17
|
syl |
|- ( ph -> S e. ZZ ) |
| 19 |
|
df-3an |
|- ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ S e. ZZ ) ) |
| 20 |
16 18 19
|
sylanbrc |
|- ( ph -> ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) ) |
| 21 |
|
cshinj |
|- ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) -> ( H = ( F cyclShift S ) -> Fun `' H ) ) |
| 22 |
20 6 21
|
mpisyl |
|- ( ph -> Fun `' H ) |
| 23 |
|
istrl |
|- ( H ( Trails ` G ) Q <-> ( H ( Walks ` G ) Q /\ Fun `' H ) ) |
| 24 |
8 22 23
|
sylanbrc |
|- ( ph -> H ( Trails ` G ) Q ) |