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	biimpi	$$⊢F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\to F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
28	27	adantl	$$⊢\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$$
29	8 22 28	3syl	$$⊢\phi \to F:\left(0..^N\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
30	9	fvexi	$$⊢N\in \mathrm{V}$$
31		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\}$$
32	30 5 31	sylancr	$$⊢\phi \to \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
33		dmsnopg	$$⊢E\in \mathrm{Edg}\left(G\right)\to \mathrm{dom}\left\{⟨B,E⟩\right\}=\left\{B\right\}$$
34	10 33	syl	$$⊢\phi \to \mathrm{dom}\left\{⟨B,E⟩\right\}=\left\{B\right\}$$
35	34	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)$$
36	32 35	mpbird	$$⊢\phi \to \left\{⟨N,B⟩\right\}:\left\{N\right\}\underset{1-1\; onto}{⟶}\mathrm{dom}\left\{⟨B,E⟩\right\}$$
37		fzodisjsn	$$⊢\left(0..^N\right)\cap \left\{N\right\}=\varnothing$$
38	37	a1i	$$⊢\phi \to \left(0..^N\right)\cap \left\{N\right\}=\varnothing$$
39	34	ineq2d	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}\left\{⟨B,E⟩\right\}=\mathrm{dom}I\cap \left\{B\right\}$$
40		disjsn	$$⊢\mathrm{dom}I\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in \mathrm{dom}I$$
41	7 40	sylibr	$$⊢\phi \to \mathrm{dom}I\cap \left\{B\right\}=\varnothing$$
42	39 41	eqtrd	$$⊢\phi \to \mathrm{dom}I\cap \mathrm{dom}\left\{⟨B,E⟩\right\}=\varnothing$$
43		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\}$$
44	29 36 38 42 43	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\}$$
45	13	a1i	$$⊢\phi \to H=F\cup \left\{⟨N,B⟩\right\}$$
46	1 2 3 4 5 6 7 18 9 10 11 19 13	wlkp1lem2	$$⊢\phi \to \left|H\right|=N+1$$
47	46	oveq2d	$$⊢\phi \to \left(0..^\left|H\right|\right)=\left(0..^N+1\right)$$
48		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
49	9	eleq1i	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left|F\right|\in {\mathbb{N}}_0$$
50		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
51	49 50	sylbb1	$$⊢\left|F\right|\in {\mathbb{N}}_0\to N\in {\mathbb{Z}}_{\ge 0}$$
52	48 51	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to N\in {\mathbb{Z}}_{\ge 0}$$
53	8 17 52	3syl	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 0}$$
54		fzosplitsn	$$⊢N\in {\mathbb{Z}}_{\ge 0}\to \left(0..^N+1\right)=\left(0..^N\right)\cup \left\{N\right\}$$
55	53 54	syl	$$⊢\phi \to \left(0..^N+1\right)=\left(0..^N\right)\cup \left\{N\right\}$$
56	47 55	eqtrd	$$⊢\phi \to \left(0..^\left|H\right|\right)=\left(0..^N\right)\cup \left\{N\right\}$$
57		dmun	$$⊢\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)=\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
58	57	a1i	$$⊢\phi \to \mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)=\mathrm{dom}I\cup \mathrm{dom}\left\{⟨B,E⟩\right\}$$
59	45 56 58	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)$$
60	44 59	mpbird	$$⊢\phi \to H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left(I\cup \left\{⟨B,E⟩\right\}\right)$$
61	12	eqcomi	$$⊢I\cup \left\{⟨B,E⟩\right\}=\mathrm{iEdg}\left(S\right)$$
62	61	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)$$
63	21 60 62	sylanbrc	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$