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 
|- ( ph -> Fun I )
wlkp1.a 
|- ( ph -> I e. Fin )
wlkp1.b 
|- ( ph -> B e. W )
wlkp1.c 
|- ( ph -> C e. V )
wlkp1.d 
|- ( ph -> -. B e. dom I )
wlkp1.w 
|- ( ph -> F ( Walks ` G ) P )
wlkp1.n 
|- N = ( # ` F )
wlkp1.e 
|- ( ph -> E e. ( Edg ` G ) )
wlkp1.x 
|- ( ph -> { ( P ` N ) , C } C_ E )
wlkp1.u 
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
wlkp1.h 
|- H = ( F u. { <. N , B >. } )
wlkp1.q 
|- Q = ( P u. { <. ( N + 1 ) , C >. } )
wlkp1.s 
|- ( ph -> ( Vtx ` S ) = V )
wlkp1.l 
|- ( ( ph /\ C = ( P ` N ) ) -> E = { C } )
Assertion wlkp1 
|- ( ph -> H ( Walks ` S ) Q )

Proof

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