Theorem eupthp1

Description: Append one path segment to an Eulerian path <. F , P >. to become an Eulerian path <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 7-Mar-2021) (Proof shortened by AV, 30-Oct-2021) (Revised by AV, 8-Apr-2024)

	Ref	Expression
Hypotheses	eupthp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	eupthp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	eupthp1.f	$$⊢\phi \to \mathrm{Fun}I$$
	eupthp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
	eupthp1.b	$$⊢\phi \to B\in W$$
	eupthp1.c	$$⊢\phi \to C\in V$$
	eupthp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
	eupthp1.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
	eupthp1.n	$$⊢N=\left|F\right|$$
	eupthp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
	eupthp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
	eupthp1.u	$$⊢\mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
	eupthp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
	eupthp1.q	$$⊢Q=P\cup \left\{⟨N+1,C⟩\right\}$$
	eupthp1.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
	eupthp1.l	$$⊢\left(\phi \wedge C=P\left(N\right)\right)\to E=\left\{C\right\}$$
Assertion	eupthp1	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$

Proof

Step	Hyp	Ref	Expression
1		eupthp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eupthp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eupthp1.f	$$⊢\phi \to \mathrm{Fun}I$$
4		eupthp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
5		eupthp1.b	$$⊢\phi \to B\in W$$
6		eupthp1.c	$$⊢\phi \to C\in V$$
7		eupthp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
8		eupthp1.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
9		eupthp1.n	$$⊢N=\left|F\right|$$
10		eupthp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
11		eupthp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
12		eupthp1.u	$$⊢\mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
13		eupthp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
14		eupthp1.q	$$⊢Q=P\cup \left\{⟨N+1,C⟩\right\}$$
15		eupthp1.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
16		eupthp1.l	$$⊢\left(\phi \wedge C=P\left(N\right)\right)\to E=\left\{C\right\}$$
17		eupthiswlk	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
18	8 17	syl	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
19	12	a1i	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
20	15	a1i	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
21	1 2 3 4 5 6 7 18 9 10 11 19 13 14 20 16	wlkp1	$$⊢\phi \to H\mathrm{Walks}\left(S\right)Q$$
22	2	eupthi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$
23	9	eqcomi	$$⊢\left|F\right|=N$$
24	23	oveq2i	$$⊢\left(0..^\left|F\right|\right)=\left(0..^N\right)$$
25		f1oeq2	$$⊢\left(0..^\left|F\right|\right)=\left(0..^N\right)\to \left(F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\leftrightarrow F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$
26	24 25	ax-mp	$$⊢F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\leftrightarrow F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
27	26	bilani	$$⊢\left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)\to F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
28	8 22 27	3syl	$$⊢\phi \to F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
29	9	fvexi	$$⊢N\in \mathrm{V}$$
30		f1osng	$$⊢\left(N\in \mathrm{V}\wedge B\in W\right)\to \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
31	29 5 30	sylancr	$$⊢\phi \to \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
32		dmsnopg	$$⊢E\in \mathrm{Edg}\left(G\right)\to \mathrm{dom}\left\{⟨B,E⟩\right\}=\left\{B\right\}$$
33	10 32	syl	$$⊢\phi \to \mathrm{dom}\left\{⟨B,E⟩\right\}=\left\{B\right\}$$
34	33	f1oeq3d	$$⊢\phi \to \left(\left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}\left\{⟨B,E⟩\right\}\leftrightarrow \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
35	31 34	mpbird	$$⊢\phi \to \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}\left\{⟨B,E⟩\right\}$$
36		fzodisjsn	$$⊢\left(0..^N\right)\cap \left\{N\right\}=\varnothing$$
37	36	a1i	$$⊢\phi \to \left(0..^N\right)\cap \left\{N\right\}=\varnothing$$
38	33	ineq2d	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}\left\{⟨B,E⟩\right\}=\mathrm{dom}I\cap \left\{B\right\}$$
39		disjsn	$$⊢\mathrm{dom}I\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in \mathrm{dom}I$$
40	7 39	sylibr	$$⊢\phi \to \mathrm{dom}I\cap \left\{B\right\}=\varnothing$$
41	38 40	eqtrd	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}\left\{⟨B,E⟩\right\}=\varnothing$$
42		f1oun	$$⊢\left(\left(F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\wedge \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}\left\{⟨B,E⟩\right\}\right)\wedge \left(\left(0..^N\right)\cap \left\{N\right\}=\varnothing \wedge \mathrm{dom}I\cap \mathrm{dom}\left\{⟨B,E⟩\right\}=\varnothing \right)\right)\to \left(F\cup \left\{⟨N,B⟩\right\}\right):\left(0..^N\right)\cup \left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
43	28 35 37 41 42	syl22anc	$$⊢\phi \to \left(F\cup \left\{⟨N,B⟩\right\}\right):\left(0..^N\right)\cup \left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
44	13	a1i	$$⊢\phi \to H=F\cup \left\{⟨N,B⟩\right\}$$
45	1 2 3 4 5 6 7 18 9 10 11 19 13	wlkp1lem2	$$⊢\phi \to \left|H\right|=N+1$$
46	45	oveq2d	$$⊢\phi \to \left(0..^\left|H\right|\right)=\left(0..^N+1\right)$$
47		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
48	9	eleq1i	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left|F\right|\in {\mathbb{N}}_0$$
49		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
50	48 49	sylbb1	$$⊢\left|F\right|\in {\mathbb{N}}_0\to N\in {\mathbb{Z}}_{\ge 0}$$
51	47 50	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to N\in {\mathbb{Z}}_{\ge 0}$$
52	8 17 51	3syl	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 0}$$
53		fzosplitsn	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left(0..^N+1\right)=\left(0..^N\right)\cup \left\{N\right\}$$
54	52 53	syl	$$⊢\phi \to \left(0..^N+1\right)=\left(0..^N\right)\cup \left\{N\right\}$$
55	46 54	eqtrd	$$⊢\phi \to \left(0..^\left|H\right|\right)=\left(0..^N\right)\cup \left\{N\right\}$$
56		dmun	$$⊢\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)=\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
57	56	a1i	$$⊢\phi \to \mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)=\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
58	44 55 57	f1oeq123d	$$⊢\phi \to \left(H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)\leftrightarrow \left(F\cup \left\{⟨N,B⟩\right\}\right):\left(0..^N\right)\cup \left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}\right)$$
59	43 58	mpbird	$$⊢\phi \to H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)$$
60	12	eqcomi	$$⊢I\cup \left\{⟨B,E⟩\right\}=\mathrm{iEdg}\left(S\right)$$
61	60	iseupthf1o	$$⊢H\mathrm{EulerPaths}\left(S\right)Q\leftrightarrow \left(H\mathrm{Walks}\left(S\right)Q\wedge H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)\right)$$
62	21 59 61	sylanbrc	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$