| 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 |
|
crctiswlk |
|- ( F ( Circuits ` G ) P -> F ( Walks ` G ) P ) |
| 8 |
2
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| 9 |
3 7 8
|
3syl |
|- ( ph -> F e. Word dom I ) |
| 10 |
|
elfzoelz |
|- ( S e. ( 0 ..^ N ) -> S e. ZZ ) |
| 11 |
5 10
|
syl |
|- ( ph -> S e. ZZ ) |
| 12 |
|
cshwlen |
|- ( ( F e. Word dom I /\ S e. ZZ ) -> ( # ` ( F cyclShift S ) ) = ( # ` F ) ) |
| 13 |
9 11 12
|
syl2anc |
|- ( ph -> ( # ` ( F cyclShift S ) ) = ( # ` F ) ) |
| 14 |
6
|
fveq2i |
|- ( # ` H ) = ( # ` ( F cyclShift S ) ) |
| 15 |
13 14 4
|
3eqtr4g |
|- ( ph -> ( # ` H ) = N ) |