Metamath Proof Explorer


Theorem eupth2eucrct

Description: Append one path segment to an Eulerian path <. F , P >. which may not be an (Eulerian) circuit to become an Eulerian circuit <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by AV, 11-Mar-2021) (Proof shortened by AV, 30-Oct-2021) (Revised by AV, 8-Apr-2024)

Ref Expression
Hypotheses eupthp1.v V = Vtx G
eupthp1.i I = iEdg G
eupthp1.f φ Fun I
eupthp1.a φ I Fin
eupthp1.b φ B W
eupthp1.c φ C V
eupthp1.d φ ¬ B dom I
eupthp1.p φ F EulerPaths G P
eupthp1.n N = F
eupthp1.e φ E Edg G
eupthp1.x φ P N C E
eupthp1.u iEdg S = I B E
eupthp1.h H = F N B
eupthp1.q Q = P N + 1 C
eupthp1.s Vtx S = V
eupthp1.l φ C = P N E = C
eupth2eucrct.c φ C = P 0
Assertion eupth2eucrct φ H EulerPaths S Q H Circuits S Q

Proof

Step Hyp Ref Expression
1 eupthp1.v V = Vtx G
2 eupthp1.i I = iEdg G
3 eupthp1.f φ Fun I
4 eupthp1.a φ I Fin
5 eupthp1.b φ B W
6 eupthp1.c φ C V
7 eupthp1.d φ ¬ B dom I
8 eupthp1.p φ F EulerPaths G P
9 eupthp1.n N = F
10 eupthp1.e φ E Edg G
11 eupthp1.x φ P N C E
12 eupthp1.u iEdg S = I B E
13 eupthp1.h H = F N B
14 eupthp1.q Q = P N + 1 C
15 eupthp1.s Vtx S = V
16 eupthp1.l φ C = P N E = C
17 eupth2eucrct.c φ C = P 0
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 eupthp1 φ H EulerPaths S Q
19 simpr φ H EulerPaths S Q H EulerPaths S Q
20 eupthistrl H EulerPaths S Q H Trails S Q
21 20 adantl φ H EulerPaths S Q H Trails S Q
22 fveq2 k = 0 Q k = Q 0
23 fveq2 k = 0 P k = P 0
24 22 23 eqeq12d k = 0 Q k = P k Q 0 = P 0
25 eupthiswlk F EulerPaths G P F Walks G P
26 8 25 syl φ F Walks G P
27 12 a1i φ iEdg S = I B E
28 15 a1i φ Vtx S = V
29 1 2 3 4 5 6 7 26 9 10 11 27 13 14 28 wlkp1lem5 φ k 0 N Q k = P k
30 2 wlkf F Walks G P F Word dom I
31 lencl F Word dom I F 0
32 9 eleq1i N 0 F 0
33 0elfz N 0 0 0 N
34 32 33 sylbir F 0 0 0 N
35 31 34 syl F Word dom I 0 0 N
36 8 25 30 35 4syl φ 0 0 N
37 24 29 36 rspcdva φ Q 0 = P 0
38 37 adantr φ H EulerPaths S Q Q 0 = P 0
39 17 eqcomd φ P 0 = C
40 39 adantr φ H EulerPaths S Q P 0 = C
41 14 a1i φ H EulerPaths S Q Q = P N + 1 C
42 13 fveq2i H = F N B
43 42 a1i φ H EulerPaths S Q H = F N B
44 wrdfin F Word dom I F Fin
45 8 25 30 44 4syl φ F Fin
46 45 adantr φ H EulerPaths S Q F Fin
47 snfi N B Fin
48 47 a1i φ H EulerPaths S Q N B Fin
49 wrddm F Word dom I dom F = 0 ..^ F
50 8 25 30 49 4syl φ dom F = 0 ..^ F
51 fzonel ¬ F 0 ..^ F
52 51 a1i φ ¬ F 0 ..^ F
53 9 eleq1i N 0 ..^ F F 0 ..^ F
54 52 53 sylnibr φ ¬ N 0 ..^ F
55 eleq2 dom F = 0 ..^ F N dom F N 0 ..^ F
56 55 notbid dom F = 0 ..^ F ¬ N dom F ¬ N 0 ..^ F
57 54 56 syl5ibrcom φ dom F = 0 ..^ F ¬ N dom F
58 9 fvexi N V
59 58 a1i φ N V
60 59 5 opeldmd φ N B F N dom F
61 57 60 nsyld φ dom F = 0 ..^ F ¬ N B F
62 50 61 mpd φ ¬ N B F
63 62 adantr φ H EulerPaths S Q ¬ N B F
64 disjsn F N B = ¬ N B F
65 63 64 sylibr φ H EulerPaths S Q F N B =
66 hashun F Fin N B Fin F N B = F N B = F + N B
67 46 48 65 66 syl3anc φ H EulerPaths S Q F N B = F + N B
68 9 eqcomi F = N
69 opex N B V
70 hashsng N B V N B = 1
71 69 70 ax-mp N B = 1
72 68 71 oveq12i F + N B = N + 1
73 72 a1i φ H EulerPaths S Q F + N B = N + 1
74 43 67 73 3eqtrd φ H EulerPaths S Q H = N + 1
75 41 74 fveq12d φ H EulerPaths S Q Q H = P N + 1 C N + 1
76 ovexd φ N + 1 V
77 1 2 3 4 5 6 7 26 9 wlkp1lem1 φ ¬ N + 1 dom P
78 76 6 77 3jca φ N + 1 V C V ¬ N + 1 dom P
79 78 adantr φ H EulerPaths S Q N + 1 V C V ¬ N + 1 dom P
80 fsnunfv N + 1 V C V ¬ N + 1 dom P P N + 1 C N + 1 = C
81 79 80 syl φ H EulerPaths S Q P N + 1 C N + 1 = C
82 75 81 eqtr2d φ H EulerPaths S Q C = Q H
83 38 40 82 3eqtrd φ H EulerPaths S Q Q 0 = Q H
84 iscrct H Circuits S Q H Trails S Q Q 0 = Q H
85 21 83 84 sylanbrc φ H EulerPaths S Q H Circuits S Q
86 19 85 jca φ H EulerPaths S Q H EulerPaths S Q H Circuits S Q
87 18 86 mpdan φ H EulerPaths S Q H Circuits S Q