| 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 |
|
crctistrl |
|- ( F ( Circuits ` G ) P -> F ( Trails ` G ) P ) |
| 9 |
|
trliswlk |
|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P ) |
| 10 |
|
wlkv |
|- ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) |
| 11 |
|
simp1 |
|- ( ( G e. _V /\ F e. _V /\ P e. _V ) -> G e. _V ) |
| 12 |
9 10 11
|
3syl |
|- ( F ( Trails ` G ) P -> G e. _V ) |
| 13 |
3 8 12
|
3syl |
|- ( ph -> G e. _V ) |
| 14 |
6
|
ovexi |
|- H e. _V |
| 15 |
14
|
a1i |
|- ( ph -> H e. _V ) |
| 16 |
|
ovex |
|- ( 0 ... N ) e. _V |
| 17 |
16
|
mptex |
|- ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) e. _V |
| 18 |
7 17
|
eqeltri |
|- Q e. _V |
| 19 |
18
|
a1i |
|- ( ph -> Q e. _V ) |
| 20 |
13 15 19
|
3jca |
|- ( ph -> ( G e. _V /\ H e. _V /\ Q e. _V ) ) |