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

Metamath Proof Explorer

Theorem eupth2lem3

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypotheses eupth2.v 
|- V = ( Vtx ` G )
eupth2.i 
|- I = ( iEdg ` G )
eupth2.g 
|- ( ph -> G e. UPGraph )
eupth2.f 
|- ( ph -> Fun I )
eupth2.p 
|- ( ph -> F ( EulerPaths ` G ) P )
eupth2.h 
|- H = <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >.
eupth2.x 
|- X = <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >.
eupth2.n 
|- ( ph -> N e. NN0 )
eupth2.l 
|- ( ph -> ( N + 1 ) <_ ( # ` F ) )
eupth2.u 
|- ( ph -> U e. V )
eupth2.o 
|- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` H ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
Assertion eupth2lem3 
|- ( ph -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 eupth2.v 
 |-  V = ( Vtx ` G )
2 eupth2.i 
 |-  I = ( iEdg ` G )
3 eupth2.g 
 |-  ( ph -> G e. UPGraph )
4 eupth2.f 
 |-  ( ph -> Fun I )
5 eupth2.p 
 |-  ( ph -> F ( EulerPaths ` G ) P )
6 eupth2.h 
 |-  H = <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >.
7 eupth2.x 
 |-  X = <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >.
8 eupth2.n 
 |-  ( ph -> N e. NN0 )
9 eupth2.l 
 |-  ( ph -> ( N + 1 ) <_ ( # ` F ) )
10 eupth2.u 
 |-  ( ph -> U e. V )
11 eupth2.o 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` H ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
12 eupthiswlk 
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
13 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
14 5 12 13 3syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
15 nn0p1elfzo 
 |-  ( ( N e. NN0 /\ ( # ` F ) e. NN0 /\ ( N + 1 ) <_ ( # ` F ) ) -> N e. ( 0 ..^ ( # ` F ) ) )
16 8 14 9 15 syl3anc 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
17 eupthistrl 
 |-  ( F ( EulerPaths ` G ) P -> F ( Trails ` G ) P )
18 5 17 syl 
 |-  ( ph -> F ( Trails ` G ) P )
19 6 fveq2i 
 |-  ( Vtx ` H ) = ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >. )
20 1 fvexi 
 |-  V e. _V
21 2 fvexi 
 |-  I e. _V
22 21 resex 
 |-  ( I |` ( F " ( 0 ..^ N ) ) ) e. _V
23 20 22 opvtxfvi 
 |-  ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >. ) = V
24 19 23 eqtri 
 |-  ( Vtx ` H ) = V
25 24 a1i 
 |-  ( ph -> ( Vtx ` H ) = V )
26 snex 
 |-  { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } e. _V
27 20 26 opvtxfvi 
 |-  ( Vtx ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = V
28 27 a1i 
 |-  ( ph -> ( Vtx ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = V )
29 7 fveq2i 
 |-  ( Vtx ` X ) = ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. )
30 21 resex 
 |-  ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) e. _V
31 20 30 opvtxfvi 
 |-  ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. ) = V
32 29 31 eqtri 
 |-  ( Vtx ` X ) = V
33 32 a1i 
 |-  ( ph -> ( Vtx ` X ) = V )
34 6 fveq2i 
 |-  ( iEdg ` H ) = ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >. )
35 20 22 opiedgfvi 
 |-  ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ N ) ) ) >. ) = ( I |` ( F " ( 0 ..^ N ) ) )
36 34 35 eqtri 
 |-  ( iEdg ` H ) = ( I |` ( F " ( 0 ..^ N ) ) )
37 36 a1i 
 |-  ( ph -> ( iEdg ` H ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
38 20 26 opiedgfvi 
 |-  ( iEdg ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. }
39 38 a1i 
 |-  ( ph -> ( iEdg ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
40 7 fveq2i 
 |-  ( iEdg ` X ) = ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. )
41 20 30 opiedgfvi 
 |-  ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. ) = ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) )
42 40 41 eqtri 
 |-  ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) )
43 8 nn0zd 
 |-  ( ph -> N e. ZZ )
44 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
45 44 eqcomd 
 |-  ( N e. ZZ -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
46 43 45 syl 
 |-  ( ph -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
47 46 imaeq2d 
 |-  ( ph -> ( F " ( 0 ..^ ( N + 1 ) ) ) = ( F " ( 0 ... N ) ) )
48 47 reseq2d 
 |-  ( ph -> ( I |` ( F " ( 0 ..^ ( N + 1 ) ) ) ) = ( I |` ( F " ( 0 ... N ) ) ) )
49 42 48 eqtrid 
 |-  ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ... N ) ) ) )
50 2fveq3 
 |-  ( k = N -> ( I ` ( F ` k ) ) = ( I ` ( F ` N ) ) )
51 fveq2 
 |-  ( k = N -> ( P ` k ) = ( P ` N ) )
52 fvoveq1 
 |-  ( k = N -> ( P ` ( k + 1 ) ) = ( P ` ( N + 1 ) ) )
53 51 52 preq12d 
 |-  ( k = N -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
54 50 53 eqeq12d 
 |-  ( k = N -> ( ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
55 5 12 syl 
 |-  ( ph -> F ( Walks ` G ) P )
56 2 upgrwlkedg 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
57 3 55 56 syl2anc 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
58 54 57 16 rspcdva 
 |-  ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
59 1 2 4 16 10 18 25 28 33 37 39 49 11 58 eupth2lem3lem7 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )