Metamath Proof Explorer


Theorem eupth2

Description: The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (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 φ G UPGraph
eupth2.f φ Fun I
eupth2.p φ F EulerPaths G P
Assertion eupth2 φ x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F

Proof

Step Hyp Ref Expression
1 eupth2.v V = Vtx G
2 eupth2.i I = iEdg G
3 eupth2.g φ G UPGraph
4 eupth2.f φ Fun I
5 eupth2.p φ F EulerPaths G P
6 eqid V I F 0 ..^ F = V I F 0 ..^ F
7 1 2 3 4 5 6 eupthvdres φ VtxDeg V I F 0 ..^ F = VtxDeg G
8 7 fveq1d φ VtxDeg V I F 0 ..^ F x = VtxDeg G x
9 8 breq2d φ 2 VtxDeg V I F 0 ..^ F x 2 VtxDeg G x
10 9 notbid φ ¬ 2 VtxDeg V I F 0 ..^ F x ¬ 2 VtxDeg G x
11 10 rabbidv φ x V | ¬ 2 VtxDeg V I F 0 ..^ F x = x V | ¬ 2 VtxDeg G x
12 eupthiswlk F EulerPaths G P F Walks G P
13 wlkcl F Walks G P F 0
14 5 12 13 3syl φ F 0
15 nn0re F 0 F
16 15 leidd F 0 F F
17 breq1 m = 0 m F 0 F
18 oveq2 m = 0 0 ..^ m = 0 ..^ 0
19 18 imaeq2d m = 0 F 0 ..^ m = F 0 ..^ 0
20 19 reseq2d m = 0 I F 0 ..^ m = I F 0 ..^ 0
21 20 opeq2d m = 0 V I F 0 ..^ m = V I F 0 ..^ 0
22 21 fveq2d m = 0 VtxDeg V I F 0 ..^ m = VtxDeg V I F 0 ..^ 0
23 22 fveq1d m = 0 VtxDeg V I F 0 ..^ m x = VtxDeg V I F 0 ..^ 0 x
24 23 breq2d m = 0 2 VtxDeg V I F 0 ..^ m x 2 VtxDeg V I F 0 ..^ 0 x
25 24 notbid m = 0 ¬ 2 VtxDeg V I F 0 ..^ m x ¬ 2 VtxDeg V I F 0 ..^ 0 x
26 25 rabbidv m = 0 x V | ¬ 2 VtxDeg V I F 0 ..^ m x = x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x
27 fveq2 m = 0 P m = P 0
28 27 eqeq2d m = 0 P 0 = P m P 0 = P 0
29 27 preq2d m = 0 P 0 P m = P 0 P 0
30 28 29 ifbieq2d m = 0 if P 0 = P m P 0 P m = if P 0 = P 0 P 0 P 0
31 26 30 eqeq12d m = 0 x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x = if P 0 = P 0 P 0 P 0
32 17 31 imbi12d m = 0 m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m 0 F x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x = if P 0 = P 0 P 0 P 0
33 32 imbi2d m = 0 φ m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m φ 0 F x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x = if P 0 = P 0 P 0 P 0
34 breq1 m = n m F n F
35 oveq2 m = n 0 ..^ m = 0 ..^ n
36 35 imaeq2d m = n F 0 ..^ m = F 0 ..^ n
37 36 reseq2d m = n I F 0 ..^ m = I F 0 ..^ n
38 37 opeq2d m = n V I F 0 ..^ m = V I F 0 ..^ n
39 38 fveq2d m = n VtxDeg V I F 0 ..^ m = VtxDeg V I F 0 ..^ n
40 39 fveq1d m = n VtxDeg V I F 0 ..^ m x = VtxDeg V I F 0 ..^ n x
41 40 breq2d m = n 2 VtxDeg V I F 0 ..^ m x 2 VtxDeg V I F 0 ..^ n x
42 41 notbid m = n ¬ 2 VtxDeg V I F 0 ..^ m x ¬ 2 VtxDeg V I F 0 ..^ n x
43 42 rabbidv m = n x V | ¬ 2 VtxDeg V I F 0 ..^ m x = x V | ¬ 2 VtxDeg V I F 0 ..^ n x
44 fveq2 m = n P m = P n
45 44 eqeq2d m = n P 0 = P m P 0 = P n
46 44 preq2d m = n P 0 P m = P 0 P n
47 45 46 ifbieq2d m = n if P 0 = P m P 0 P m = if P 0 = P n P 0 P n
48 43 47 eqeq12d m = n x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n
49 34 48 imbi12d m = n m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m n F x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n
50 49 imbi2d m = n φ m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m φ n F x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n
51 breq1 m = n + 1 m F n + 1 F
52 oveq2 m = n + 1 0 ..^ m = 0 ..^ n + 1
53 52 imaeq2d m = n + 1 F 0 ..^ m = F 0 ..^ n + 1
54 53 reseq2d m = n + 1 I F 0 ..^ m = I F 0 ..^ n + 1
55 54 opeq2d m = n + 1 V I F 0 ..^ m = V I F 0 ..^ n + 1
56 55 fveq2d m = n + 1 VtxDeg V I F 0 ..^ m = VtxDeg V I F 0 ..^ n + 1
57 56 fveq1d m = n + 1 VtxDeg V I F 0 ..^ m x = VtxDeg V I F 0 ..^ n + 1 x
58 57 breq2d m = n + 1 2 VtxDeg V I F 0 ..^ m x 2 VtxDeg V I F 0 ..^ n + 1 x
59 58 notbid m = n + 1 ¬ 2 VtxDeg V I F 0 ..^ m x ¬ 2 VtxDeg V I F 0 ..^ n + 1 x
60 59 rabbidv m = n + 1 x V | ¬ 2 VtxDeg V I F 0 ..^ m x = x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x
61 fveq2 m = n + 1 P m = P n + 1
62 61 eqeq2d m = n + 1 P 0 = P m P 0 = P n + 1
63 61 preq2d m = n + 1 P 0 P m = P 0 P n + 1
64 62 63 ifbieq2d m = n + 1 if P 0 = P m P 0 P m = if P 0 = P n + 1 P 0 P n + 1
65 60 64 eqeq12d m = n + 1 x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
66 51 65 imbi12d m = n + 1 m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m n + 1 F x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
67 66 imbi2d m = n + 1 φ m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m φ n + 1 F x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
68 breq1 m = F m F F F
69 oveq2 m = F 0 ..^ m = 0 ..^ F
70 69 imaeq2d m = F F 0 ..^ m = F 0 ..^ F
71 70 reseq2d m = F I F 0 ..^ m = I F 0 ..^ F
72 71 opeq2d m = F V I F 0 ..^ m = V I F 0 ..^ F
73 72 fveq2d m = F VtxDeg V I F 0 ..^ m = VtxDeg V I F 0 ..^ F
74 73 fveq1d m = F VtxDeg V I F 0 ..^ m x = VtxDeg V I F 0 ..^ F x
75 74 breq2d m = F 2 VtxDeg V I F 0 ..^ m x 2 VtxDeg V I F 0 ..^ F x
76 75 notbid m = F ¬ 2 VtxDeg V I F 0 ..^ m x ¬ 2 VtxDeg V I F 0 ..^ F x
77 76 rabbidv m = F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = x V | ¬ 2 VtxDeg V I F 0 ..^ F x
78 fveq2 m = F P m = P F
79 78 eqeq2d m = F P 0 = P m P 0 = P F
80 78 preq2d m = F P 0 P m = P 0 P F
81 79 80 ifbieq2d m = F if P 0 = P m P 0 P m = if P 0 = P F P 0 P F
82 77 81 eqeq12d m = F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
83 68 82 imbi12d m = F m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m F F x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
84 83 imbi2d m = F φ m F x V | ¬ 2 VtxDeg V I F 0 ..^ m x = if P 0 = P m P 0 P m φ F F x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
85 1 2 3 4 5 eupth2lemb φ x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x =
86 eqid P 0 = P 0
87 86 iftruei if P 0 = P 0 P 0 P 0 =
88 85 87 eqtr4di φ x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x = if P 0 = P 0 P 0 P 0
89 88 a1d φ 0 F x V | ¬ 2 VtxDeg V I F 0 ..^ 0 x = if P 0 = P 0 P 0 P 0
90 1 2 3 4 5 eupth2lems φ n 0 n F x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n n + 1 F x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
91 90 expcom n 0 φ n F x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n n + 1 F x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
92 91 a2d n 0 φ n F x V | ¬ 2 VtxDeg V I F 0 ..^ n x = if P 0 = P n P 0 P n φ n + 1 F x V | ¬ 2 VtxDeg V I F 0 ..^ n + 1 x = if P 0 = P n + 1 P 0 P n + 1
93 33 50 67 84 89 92 nn0ind F 0 φ F F x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
94 16 93 mpid F 0 φ x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
95 14 94 mpcom φ x V | ¬ 2 VtxDeg V I F 0 ..^ F x = if P 0 = P F P 0 P F
96 11 95 eqtr3d φ x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F