Metamath Proof Explorer


Theorem eupth2lem3lem6

Description: Formerly part of proof of eupth2lem3 : If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than ( P0 ) and ( PN ) : if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 25-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v V = Vtx G
trlsegvdeg.i I = iEdg G
trlsegvdeg.f φ Fun I
trlsegvdeg.n φ N 0 ..^ F
trlsegvdeg.u φ U V
trlsegvdeg.w φ F Trails G P
trlsegvdeg.vx φ Vtx X = V
trlsegvdeg.vy φ Vtx Y = V
trlsegvdeg.vz φ Vtx Z = V
trlsegvdeg.ix φ iEdg X = I F 0 ..^ N
trlsegvdeg.iy φ iEdg Y = F N I F N
trlsegvdeg.iz φ iEdg Z = I F 0 N
eupth2lem3.o φ x V | ¬ 2 VtxDeg X x = if P 0 = P N P 0 P N
eupth2lem3.e φ I F N = P N P N + 1
Assertion eupth2lem3lem6 φ P N P N + 1 U P N U P N + 1 ¬ 2 VtxDeg X U + VtxDeg Y U U 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 φ Fun I
4 trlsegvdeg.n φ N 0 ..^ F
5 trlsegvdeg.u φ U V
6 trlsegvdeg.w φ F Trails G P
7 trlsegvdeg.vx φ Vtx X = V
8 trlsegvdeg.vy φ Vtx Y = V
9 trlsegvdeg.vz φ Vtx Z = V
10 trlsegvdeg.ix φ iEdg X = I F 0 ..^ N
11 trlsegvdeg.iy φ iEdg Y = F N I F N
12 trlsegvdeg.iz φ iEdg Z = I F 0 N
13 eupth2lem3.o φ x V | ¬ 2 VtxDeg X x = if P 0 = P N P 0 P N
14 eupth2lem3.e φ I F N = P N P N + 1
15 11 3ad2ant1 φ P N P N + 1 U P N U P N + 1 iEdg Y = F N I F N
16 8 3ad2ant1 φ P N P N + 1 U P N U P N + 1 Vtx Y = V
17 fvexd φ P N P N + 1 U P N U P N + 1 F N V
18 5 3ad2ant1 φ P N P N + 1 U P N U P N + 1 U V
19 fvexd φ P N P N + 1 U P N U P N + 1 I F N V
20 simpl U P N U P N + 1 U P N
21 20 adantl P N P N + 1 U P N U P N + 1 U P N
22 simpr U P N U P N + 1 U P N + 1
23 22 adantl P N P N + 1 U P N U P N + 1 U P N + 1
24 21 23 nelprd P N P N + 1 U P N U P N + 1 ¬ U P N P N + 1
25 df-nel U P N P N + 1 ¬ U P N P N + 1
26 24 25 sylibr P N P N + 1 U P N U P N + 1 U P N P N + 1
27 neleq2 I F N = P N P N + 1 U I F N U P N P N + 1
28 26 27 syl5ibr I F N = P N P N + 1 P N P N + 1 U P N U P N + 1 U I F N
29 28 expd I F N = P N P N + 1 P N P N + 1 U P N U P N + 1 U I F N
30 14 29 syl φ P N P N + 1 U P N U P N + 1 U I F N
31 30 3imp φ P N P N + 1 U P N U P N + 1 U I F N
32 15 16 17 18 19 31 1hevtxdg0 φ P N P N + 1 U P N U P N + 1 VtxDeg Y U = 0
33 32 oveq2d φ P N P N + 1 U P N U P N + 1 VtxDeg X U + VtxDeg Y U = VtxDeg X U + 0
34 1 2 3 4 5 6 7 8 9 10 11 12 eupth2lem3lem1 φ VtxDeg X U 0
35 34 nn0cnd φ VtxDeg X U
36 35 addid1d φ VtxDeg X U + 0 = VtxDeg X U
37 36 3ad2ant1 φ P N P N + 1 U P N U P N + 1 VtxDeg X U + 0 = VtxDeg X U
38 33 37 eqtrd φ P N P N + 1 U P N U P N + 1 VtxDeg X U + VtxDeg Y U = VtxDeg X U
39 38 breq2d φ P N P N + 1 U P N U P N + 1 2 VtxDeg X U + VtxDeg Y U 2 VtxDeg X U
40 39 notbid φ P N P N + 1 U P N U P N + 1 ¬ 2 VtxDeg X U + VtxDeg Y U ¬ 2 VtxDeg X U
41 fveq2 x = U VtxDeg X x = VtxDeg X U
42 41 breq2d x = U 2 VtxDeg X x 2 VtxDeg X U
43 42 notbid x = U ¬ 2 VtxDeg X x ¬ 2 VtxDeg X U
44 43 elrab3 U V U x V | ¬ 2 VtxDeg X x ¬ 2 VtxDeg X U
45 5 44 syl φ U x V | ¬ 2 VtxDeg X x ¬ 2 VtxDeg X U
46 13 eleq2d φ U x V | ¬ 2 VtxDeg X x U if P 0 = P N P 0 P N
47 45 46 bitr3d φ ¬ 2 VtxDeg X U U if P 0 = P N P 0 P N
48 47 3ad2ant1 φ P N P N + 1 U P N U P N + 1 ¬ 2 VtxDeg X U U if P 0 = P N P 0 P N
49 20 3ad2ant3 φ P N P N + 1 U P N U P N + 1 U P N
50 22 3ad2ant3 φ P N P N + 1 U P N U P N + 1 U P N + 1
51 49 50 2thd φ P N P N + 1 U P N U P N + 1 U P N U P N + 1
52 neeq1 U = P 0 U P N P 0 P N
53 neeq1 U = P 0 U P N + 1 P 0 P N + 1
54 52 53 bibi12d U = P 0 U P N U P N + 1 P 0 P N P 0 P N + 1
55 51 54 syl5ibcom φ P N P N + 1 U P N U P N + 1 U = P 0 P 0 P N P 0 P N + 1
56 55 pm5.32rd φ P N P N + 1 U P N U P N + 1 P 0 P N U = P 0 P 0 P N + 1 U = P 0
57 49 neneqd φ P N P N + 1 U P N U P N + 1 ¬ U = P N
58 biorf ¬ U = P N U = P 0 U = P N U = P 0
59 57 58 syl φ P N P N + 1 U P N U P N + 1 U = P 0 U = P N U = P 0
60 orcom U = P N U = P 0 U = P 0 U = P N
61 59 60 bitrdi φ P N P N + 1 U P N U P N + 1 U = P 0 U = P 0 U = P N
62 61 anbi2d φ P N P N + 1 U P N U P N + 1 P 0 P N U = P 0 P 0 P N U = P 0 U = P N
63 50 neneqd φ P N P N + 1 U P N U P N + 1 ¬ U = P N + 1
64 biorf ¬ U = P N + 1 U = P 0 U = P N + 1 U = P 0
65 63 64 syl φ P N P N + 1 U P N U P N + 1 U = P 0 U = P N + 1 U = P 0
66 orcom U = P N + 1 U = P 0 U = P 0 U = P N + 1
67 65 66 bitrdi φ P N P N + 1 U P N U P N + 1 U = P 0 U = P 0 U = P N + 1
68 67 anbi2d φ P N P N + 1 U P N U P N + 1 P 0 P N + 1 U = P 0 P 0 P N + 1 U = P 0 U = P N + 1
69 56 62 68 3bitr3d φ P N P N + 1 U P N U P N + 1 P 0 P N U = P 0 U = P N P 0 P N + 1 U = P 0 U = P N + 1
70 eupth2lem1 U V U if P 0 = P N P 0 P N P 0 P N U = P 0 U = P N
71 18 70 syl φ P N P N + 1 U P N U P N + 1 U if P 0 = P N P 0 P N P 0 P N U = P 0 U = P N
72 eupth2lem1 U V U if P 0 = P N + 1 P 0 P N + 1 P 0 P N + 1 U = P 0 U = P N + 1
73 18 72 syl φ P N P N + 1 U P N U P N + 1 U if P 0 = P N + 1 P 0 P N + 1 P 0 P N + 1 U = P 0 U = P N + 1
74 69 71 73 3bitr4d φ P N P N + 1 U P N U P N + 1 U if P 0 = P N P 0 P N U if P 0 = P N + 1 P 0 P N + 1
75 40 48 74 3bitrd φ P N P N + 1 U P N U P N + 1 ¬ 2 VtxDeg X U + VtxDeg Y U U if P 0 = P N + 1 P 0 P N + 1