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=\mathrm{Vtx}\left(G\right)$$
	wlkp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	wlkp1.f	$$⊢\phi \to \mathrm{Fun}I$$
	wlkp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
	wlkp1.b	$$⊢\phi \to B\in W$$
	wlkp1.c	$$⊢\phi \to C\in V$$
	wlkp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
	wlkp1.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
	wlkp1.n	$$⊢N=\left|F\right|$$
	wlkp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
	wlkp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
	wlkp1.u	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
	wlkp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
	wlkp1.q	$$⊢Q=P\cup \left\{⟨N+1,C⟩\right\}$$
	wlkp1.s	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
	wlkp1.l	$$⊢\left(\phi \wedge C=P\left(N\right)\right)\to E=\left\{C\right\}$$
Assertion	wlkp1	$$⊢\phi \to H\mathrm{Walks}\left(S\right)Q$$

Proof

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