Metamath Proof Explorer

Theorem eupth2lem3lem7

Description: Lemma for eupth2lem3 : Combining trlsegvdeg , eupth2lem3lem3 , eupth2lem3lem4 and eupth2lem3lem6 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 27-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 ) ) ) )
eupth2lem3.o 
|- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
eupth2lem3.e 
|- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
Assertion eupth2lem3lem7 
|- ( ph -> ( -. 2 || ( ( VtxDeg ` Z ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Proof

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 eupth2lem3.o 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
14 eupth2lem3.e 
 |-  ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
15 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeg 
 |-  ( ph -> ( ( VtxDeg ` Z ) ` U ) = ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) )
16 15 breq2d 
 |-  ( ph -> ( 2 || ( ( VtxDeg ` Z ) ` U ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
17 16 notbid 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` Z ) ` U ) <-> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
18 ifpprsnss 
 |-  ( ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
19 14 18 syl 
 |-  ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 19 eupth2lem3lem3 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem5 
 |-  ( ph -> ( I ` ( F ` N ) ) e. ~P V )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 19 21 eupth2lem3lem4 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
23 22 3expa 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
24 23 expcom 
 |-  ( ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
25 neanior 
 |-  ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) <-> -. ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem6 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
27 26 3expa 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
28 27 expcom 
 |-  ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
29 25 28 sylbir 
 |-  ( -. ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
30 24 29 pm2.61i 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
31 20 30 pm2.61dane 
 |-  ( ph -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
32 17 31 bitrd 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` Z ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )