Metamath Proof Explorer

Theorem eupth2lem3lem3

Description: Lemma for eupth2lem3 , formerly part of proof of eupth2lem3 : If a loop { ( PN ) , ( P( N + 1 ) ) } is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 21-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 ) } ) )
eupth2lem3lem3.e 
|- ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
Assertion 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 ) ) } ) ) )

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 eupth2lem3lem3.e 
 |-  ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
15 fveq2 
 |-  ( x = U -> ( ( VtxDeg ` X ) ` x ) = ( ( VtxDeg ` X ) ` U ) )
16 15 breq2d 
 |-  ( x = U -> ( 2 || ( ( VtxDeg ` X ) ` x ) <-> 2 || ( ( VtxDeg ` X ) ` U ) ) )
17 16 notbid 
 |-  ( x = U -> ( -. 2 || ( ( VtxDeg ` X ) ` x ) <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
18 17 elrab3 
 |-  ( U e. V -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
19 5 18 syl 
 |-  ( ph -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
20 13 eleq2d 
 |-  ( ph -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
21 19 20 bitr3d 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
22 21 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
23 2z 
 |-  2 e. ZZ
24 23 a1i 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
25 1 2 3 4 5 6 7 8 9 10 11 12 eupth2lem3lem1 
 |-  ( ph -> ( ( VtxDeg ` X ) ` U ) e. NN0 )
26 25 nn0zd 
 |-  ( ph -> ( ( VtxDeg ` X ) ` U ) e. ZZ )
27 26 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( VtxDeg ` X ) ` U ) e. ZZ )
28 1 2 3 4 5 6 7 8 9 10 11 12 eupth2lem3lem2 
 |-  ( ph -> ( ( VtxDeg ` Y ) ` U ) e. NN0 )
29 28 nn0zd 
 |-  ( ph -> ( ( VtxDeg ` Y ) ` U ) e. ZZ )
30 29 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( VtxDeg ` Y ) ` U ) e. ZZ )
31 z2even 
 |-  2 || 2
32 8 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( Vtx ` Y ) = V )
33 fvexd 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( F ` N ) e. _V )
34 5 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> U e. V )
35 11 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
36 14 adantr 
 |-  ( ( ph /\ ( 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 ) ) ) )
37 ifptru 
 |-  ( ( 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 ) ) ) <-> ( I ` ( F ` N ) ) = { ( P ` N ) } ) )
38 37 adantl 
 |-  ( ( ph /\ ( 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 ) ) ) <-> ( I ` ( F ` N ) ) = { ( P ` N ) } ) )
39 36 38 mpbid 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( I ` ( F ` N ) ) = { ( P ` N ) } )
40 sneq 
 |-  ( ( P ` N ) = U -> { ( P ` N ) } = { U } )
41 40 eqcoms 
 |-  ( U = ( P ` N ) -> { ( P ` N ) } = { U } )
42 39 41 sylan9eq 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( I ` ( F ` N ) ) = { U } )
43 42 opeq2d 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> <. ( F ` N ) , ( I ` ( F ` N ) ) >. = <. ( F ` N ) , { U } >. )
44 43 sneqd 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } = { <. ( F ` N ) , { U } >. } )
45 35 44 eqtrd 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( iEdg ` Y ) = { <. ( F ` N ) , { U } >. } )
46 32 33 34 45 1loopgrvd2 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> ( ( VtxDeg ` Y ) ` U ) = 2 )
47 31 46 breqtrrid 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U = ( P ` N ) ) -> 2 || ( ( VtxDeg ` Y ) ` U ) )
48 z0even 
 |-  2 || 0
49 8 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( Vtx ` Y ) = V )
50 fvexd 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( F ` N ) e. _V )
51 1 2 3 4 5 6 trlsegvdeglem1 
 |-  ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )
52 51 simpld 
 |-  ( ph -> ( P ` N ) e. V )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( P ` N ) e. V )
54 11 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
55 39 opeq2d 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> <. ( F ` N ) , ( I ` ( F ` N ) ) >. = <. ( F ` N ) , { ( P ` N ) } >. )
56 55 sneqd 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } = { <. ( F ` N ) , { ( P ` N ) } >. } )
57 54 56 eqtrd 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( iEdg ` Y ) = { <. ( F ` N ) , { ( P ` N ) } >. } )
58 57 adantr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( iEdg ` Y ) = { <. ( F ` N ) , { ( P ` N ) } >. } )
59 5 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> U e. V )
60 59 anim1i 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( U e. V /\ U =/= ( P ` N ) ) )
61 eldifsn 
 |-  ( U e. ( V \ { ( P ` N ) } ) <-> ( U e. V /\ U =/= ( P ` N ) ) )
62 60 61 sylibr 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> U e. ( V \ { ( P ` N ) } ) )
63 49 50 53 58 62 1loopgrvd0 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> ( ( VtxDeg ` Y ) ` U ) = 0 )
64 48 63 breqtrrid 
 |-  ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ U =/= ( P ` N ) ) -> 2 || ( ( VtxDeg ` Y ) ` U ) )
65 47 64 pm2.61dane 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( VtxDeg ` Y ) ` U ) )
66 dvdsadd2b 
 |-  ( ( 2 e. ZZ /\ ( ( VtxDeg ` X ) ` U ) e. ZZ /\ ( ( ( VtxDeg ` Y ) ` U ) e. ZZ /\ 2 || ( ( VtxDeg ` Y ) ` U ) ) ) -> ( 2 || ( ( VtxDeg ` X ) ` U ) <-> 2 || ( ( ( VtxDeg ` Y ) ` U ) + ( ( VtxDeg ` X ) ` U ) ) ) )
67 24 27 30 65 66 syl112anc 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( 2 || ( ( VtxDeg ` X ) ` U ) <-> 2 || ( ( ( VtxDeg ` Y ) ` U ) + ( ( VtxDeg ` X ) ` U ) ) ) )
68 28 nn0cnd 
 |-  ( ph -> ( ( VtxDeg ` Y ) ` U ) e. CC )
69 25 nn0cnd 
 |-  ( ph -> ( ( VtxDeg ` X ) ` U ) e. CC )
70 68 69 addcomd 
 |-  ( ph -> ( ( ( VtxDeg ` Y ) ` U ) + ( ( VtxDeg ` X ) ` U ) ) = ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) )
71 70 breq2d 
 |-  ( ph -> ( 2 || ( ( ( VtxDeg ` Y ) ` U ) + ( ( VtxDeg ` X ) ` U ) ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
72 71 adantr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( 2 || ( ( ( VtxDeg ` Y ) ` U ) + ( ( VtxDeg ` X ) ` U ) ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
73 67 72 bitrd 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( 2 || ( ( VtxDeg ` X ) ` U ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
74 73 notbid 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) <-> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) ) )
75 simpr 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
76 75 eqeq2d 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
77 75 preq2d 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
78 76 77 ifbieq2d 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) = if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) )
79 78 eleq2d 
 |-  ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
80 22 74 79 3bitr3d 
 |-  ( ( 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 ) ) } ) ) )