Metamath Proof Explorer


Theorem wlkp1

Description: Append one path segment (edge) E from vertex ( PN ) to a vertex C to a walk <. F , P >. to become a walk <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 . (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 6-Mar-2021) (Proof shortened by AV, 18-Apr-2021) (Revised by AV, 8-Apr-2024)

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

Proof

Step Hyp Ref Expression
1 wlkp1.v V = Vtx G
2 wlkp1.i I = iEdg G
3 wlkp1.f φ Fun I
4 wlkp1.a φ I Fin
5 wlkp1.b φ B W
6 wlkp1.c φ C V
7 wlkp1.d φ ¬ B dom I
8 wlkp1.w φ F Walks G P
9 wlkp1.n N = F
10 wlkp1.e φ E Edg G
11 wlkp1.x φ P N C E
12 wlkp1.u φ iEdg S = I B E
13 wlkp1.h H = F N B
14 wlkp1.q Q = P N + 1 C
15 wlkp1.s φ Vtx S = V
16 wlkp1.l φ C = P N E = C
17 2 wlkf F Walks G P F Word dom I
18 wrdf F Word dom I F : 0 ..^ F dom I
19 9 eqcomi F = N
20 19 oveq2i 0 ..^ F = 0 ..^ N
21 20 feq2i F : 0 ..^ F dom I F : 0 ..^ N dom I
22 18 21 sylib F Word dom I F : 0 ..^ N dom I
23 8 17 22 3syl φ F : 0 ..^ N dom I
24 9 fvexi N V
25 24 a1i φ N V
26 snidg B W B B
27 5 26 syl φ B B
28 dmsnopg E Edg G dom B E = B
29 10 28 syl φ dom B E = B
30 27 29 eleqtrrd φ B dom B E
31 25 30 fsnd φ N B : N dom B E
32 fzodisjsn 0 ..^ N N =
33 32 a1i φ 0 ..^ N N =
34 fun F : 0 ..^ N dom I N B : N dom B E 0 ..^ N N = F N B : 0 ..^ N N dom I dom B E
35 23 31 33 34 syl21anc φ F N B : 0 ..^ N N dom I dom B E
36 13 a1i φ H = F N B
37 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem2 φ H = N + 1
38 37 oveq2d φ 0 ..^ H = 0 ..^ N + 1
39 wlkcl F Walks G P F 0
40 eleq1 F = N F 0 N 0
41 40 eqcoms N = F F 0 N 0
42 elnn0uz N 0 N 0
43 42 biimpi N 0 N 0
44 41 43 syl6bi N = F F 0 N 0
45 9 44 ax-mp F 0 N 0
46 8 39 45 3syl φ N 0
47 fzosplitsn N 0 0 ..^ N + 1 = 0 ..^ N N
48 46 47 syl φ 0 ..^ N + 1 = 0 ..^ N N
49 38 48 eqtrd φ 0 ..^ H = 0 ..^ N N
50 12 dmeqd φ dom iEdg S = dom I B E
51 dmun dom I B E = dom I dom B E
52 50 51 syl6eq φ dom iEdg S = dom I dom B E
53 36 49 52 feq123d φ H : 0 ..^ H dom iEdg S F N B : 0 ..^ N N dom I dom B E
54 35 53 mpbird φ H : 0 ..^ H dom iEdg S
55 iswrdb H Word dom iEdg S H : 0 ..^ H dom iEdg S
56 54 55 sylibr φ H Word dom iEdg S
57 1 wlkp F Walks G P P : 0 F V
58 8 57 syl φ P : 0 F V
59 9 oveq2i 0 N = 0 F
60 59 feq2i P : 0 N V P : 0 F V
61 58 60 sylibr φ P : 0 N V
62 ovexd φ N + 1 V
63 62 6 fsnd φ N + 1 C : N + 1 V
64 fzp1disj 0 N N + 1 =
65 64 a1i φ 0 N N + 1 =
66 fun P : 0 N V N + 1 C : N + 1 V 0 N N + 1 = P N + 1 C : 0 N N + 1 V V
67 61 63 65 66 syl21anc φ P N + 1 C : 0 N N + 1 V V
68 fzsuc N 0 0 N + 1 = 0 N N + 1
69 46 68 syl φ 0 N + 1 = 0 N N + 1
70 unidm V V = V
71 70 eqcomi V = V V
72 71 a1i φ V = V V
73 69 72 feq23d φ P N + 1 C : 0 N + 1 V P N + 1 C : 0 N N + 1 V V
74 67 73 mpbird φ P N + 1 C : 0 N + 1 V
75 14 a1i φ Q = P N + 1 C
76 37 oveq2d φ 0 H = 0 N + 1
77 75 76 15 feq123d φ Q : 0 H Vtx S P N + 1 C : 0 N + 1 V
78 74 77 mpbird φ Q : 0 H Vtx S
79 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 wlkp1lem8 φ k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
80 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem4 φ S V H V Q V
81 eqid Vtx S = Vtx S
82 eqid iEdg S = iEdg S
83 81 82 iswlk S V H V Q V H Walks S Q H Word dom iEdg S Q : 0 H Vtx S k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
84 80 83 syl φ H Walks S Q H Word dom iEdg S Q : 0 H Vtx S k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
85 56 78 79 84 mpbir3and φ H Walks S Q