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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
wlkp1.l ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { 𝐶 } )
Assertion wlkp1 ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
4 wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
7 wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
10 wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13 wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 wlkp1.l ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { 𝐶 } )
17 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
18 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
19 9 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
20 19 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 )
21 20 feq2i ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 𝑁 ) ⟶ dom 𝐼 )
22 18 21 sylib ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ dom 𝐼 )
23 8 17 22 3syl ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ dom 𝐼 )
24 9 fvexi ⊢ 𝑁 ∈ V
25 24 a1i ⊢ ( 𝜑 → 𝑁 ∈ V )
26 snidg ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 } )
27 5 26 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
28 dmsnopg ⊢ ( 𝐸 ∈ ( Edg ‘ 𝐺 ) → dom { ⟨ 𝐵 , 𝐸 ⟩ } = { 𝐵 } )
29 10 28 syl ⊢ ( 𝜑 → dom { ⟨ 𝐵 , 𝐸 ⟩ } = { 𝐵 } )
30 27 29 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ dom { ⟨ 𝐵 , 𝐸 ⟩ } )
31 25 30 fsnd ⊢ ( 𝜑 → { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } ⟶ dom { ⟨ 𝐵 , 𝐸 ⟩ } )
32 fzodisjsn ⊢ ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅
33 32 a1i ⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ )
34 fun ⊢ ( ( ( 𝐹 : ( 0 ..^ 𝑁 ) ⟶ dom 𝐼 ∧ { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } ⟶ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) ∧ ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ ) → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ⟶ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
35 23 31 33 34 syl21anc ⊢ ( 𝜑 → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ⟶ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
36 13 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )
38 37 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
39 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
40 eleq1 ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
41 40 eqcoms ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
42 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
43 42 biimpi ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
44 41 43 syl6bi ⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) )
45 9 44 ax-mp ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
46 8 39 45 3syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
47 fzosplitsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
48 46 47 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
49 38 48 eqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
50 12 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
51 dmun ⊢ dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) = ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } )
52 50 51 eqtrdi ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
53 36 49 52 feq123d ⊢ ( 𝜑 → ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ dom ( iEdg ‘ 𝑆 ) ↔ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ⟶ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) ) )
54 35 53 mpbird ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ dom ( iEdg ‘ 𝑆 ) )
55 iswrdb ⊢ ( 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) ↔ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ dom ( iEdg ‘ 𝑆 ) )
56 54 55 sylibr ⊢ ( 𝜑 → 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) )
57 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
58 8 57 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
59 9 oveq2i ⊢ ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝐹 ) )
60 59 feq2i ⊢ ( 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
61 58 60 sylibr ⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 )
62 ovexd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
63 62 6 fsnd ⊢ ( 𝜑 → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ 𝑉 )
64 fzp1disj ⊢ ( ( 0 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
65 64 a1i ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ )
66 fun ⊢ ( ( ( 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ∧ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ 𝑉 ) ∧ ( ( 0 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ ) → ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝑉 ∪ 𝑉 ) )
67 61 63 65 66 syl21anc ⊢ ( 𝜑 → ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝑉 ∪ 𝑉 ) )
68 fzsuc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
69 46 68 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
70 unidm ⊢ ( 𝑉 ∪ 𝑉 ) = 𝑉
71 70 eqcomi ⊢ 𝑉 = ( 𝑉 ∪ 𝑉 )
72 71 a1i ⊢ ( 𝜑 → 𝑉 = ( 𝑉 ∪ 𝑉 ) )
73 69 72 feq23d ⊢ ( 𝜑 → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 0 ... ( 𝑁 + 1 ) ) ⟶ 𝑉 ↔ ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝑉 ∪ 𝑉 ) ) )
74 67 73 mpbird ⊢ ( 𝜑 → ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 0 ... ( 𝑁 + 1 ) ) ⟶ 𝑉 )
75 14 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) )
76 37 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐻 ) ) = ( 0 ... ( 𝑁 + 1 ) ) )
77 75 76 15 feq123d ⊢ ( 𝜑 → ( 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ↔ ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 0 ... ( 𝑁 + 1 ) ) ⟶ 𝑉 ) )
78 74 77 mpbird ⊢ ( 𝜑 → 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) )
79 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 wlkp1lem8 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
80 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem4 ⊢ ( 𝜑 → ( 𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )
81 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
82 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
83 81 82 iswlk ⊢ ( ( 𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) → ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) ) )
84 80 83 syl ⊢ ( 𝜑 → ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) ) )
85 56 78 79 84 mpbir3and ⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )