Description: Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | trlsegvdeg.v | |- V = ( Vtx ` G ) |
|
| trlsegvdeg.i | |- I = ( iEdg ` G ) |
||
| trlsegvdeg.f | |- ( ph -> Fun I ) |
||
| trlsegvdeg.n | |- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
||
| trlsegvdeg.u | |- ( ph -> U e. V ) |
||
| trlsegvdeg.w | |- ( ph -> F ( Trails ` G ) P ) |
||
| trlsegvdeg.vx | |- ( ph -> ( Vtx ` X ) = V ) |
||
| trlsegvdeg.vy | |- ( ph -> ( Vtx ` Y ) = V ) |
||
| trlsegvdeg.vz | |- ( ph -> ( Vtx ` Z ) = V ) |
||
| trlsegvdeg.ix | |- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) ) |
||
| trlsegvdeg.iy | |- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) |
||
| trlsegvdeg.iz | |- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) ) |
||
| Assertion | trlsegvdeglem2 | |- ( ph -> Fun ( iEdg ` X ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trlsegvdeg.v | |- V = ( Vtx ` G ) |
|
| 2 | trlsegvdeg.i | |- I = ( iEdg ` G ) |
|
| 3 | trlsegvdeg.f | |- ( ph -> Fun I ) |
|
| 4 | trlsegvdeg.n | |- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
|
| 5 | trlsegvdeg.u | |- ( ph -> U e. V ) |
|
| 6 | trlsegvdeg.w | |- ( ph -> F ( Trails ` G ) P ) |
|
| 7 | trlsegvdeg.vx | |- ( ph -> ( Vtx ` X ) = V ) |
|
| 8 | trlsegvdeg.vy | |- ( ph -> ( Vtx ` Y ) = V ) |
|
| 9 | trlsegvdeg.vz | |- ( ph -> ( Vtx ` Z ) = V ) |
|
| 10 | trlsegvdeg.ix | |- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) ) |
|
| 11 | trlsegvdeg.iy | |- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) |
|
| 12 | trlsegvdeg.iz | |- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) ) |
|
| 13 | funres | |- ( Fun I -> Fun ( I |` ( F " ( 0 ..^ N ) ) ) ) |
|
| 14 | 3 13 | syl | |- ( ph -> Fun ( I |` ( F " ( 0 ..^ N ) ) ) ) |
| 15 | 10 | funeqd | |- ( ph -> ( Fun ( iEdg ` X ) <-> Fun ( I |` ( F " ( 0 ..^ N ) ) ) ) ) |
| 16 | 14 15 | mpbird | |- ( ph -> Fun ( iEdg ` X ) ) |