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 eqtrdi $⊢ φ → 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$