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

Proof

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

Metamath Proof Explorer

Theorem eupthp1

Proof