eupth2eucrct

Description: Append one path segment to an Eulerian path <. F , P >. which may not be an (Eulerian) circuit to become an Eulerian circuit <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by AV, 11-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\}$
	eupth2eucrct.c	$⊢ φ \to C = P (0)$
Assertion	eupth2eucrct	$⊢ φ \to (H EulerPaths (S) Q \land H Circuits (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		eupth2eucrct.c	$⊢ φ \to C = P (0)$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	eupthp1	$⊢ φ \to H EulerPaths (S) Q$
19		simpr	$⊢ (φ \land H EulerPaths (S) Q) \to H EulerPaths (S) Q$
20		eupthistrl	$⊢ H EulerPaths (S) Q \to H Trails (S) Q$
21	20	adantl	$⊢ (φ \land H EulerPaths (S) Q) \to H Trails (S) Q$
22		fveq2	$⊢ k = 0 \to Q (k) = Q (0)$
23		fveq2	$⊢ k = 0 \to P (k) = P (0)$
24	22 23	eqeq12d	$⊢ k = 0 \to (Q (k) = P (k) \leftrightarrow Q (0) = P (0))$
25		eupthiswlk	$⊢ F EulerPaths (G) P \to F Walks (G) P$
26	8 25	syl	$⊢ φ \to F Walks (G) P$
27	12	a1i	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
28	15	a1i	$⊢ φ \to Vtx (S) = V$
29	1 2 3 4 5 6 7 26 9 10 11 27 13 14 28	wlkp1lem5	$⊢ φ \to \forall k \in (0 \dots N) Q (k) = P (k)$
30	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
31	25 30	syl	$⊢ F EulerPaths (G) P \to F \in Word dom I$
32		lencl	$⊢ F \in Word dom I \to \|F\| \in ℕ_{0}$
33	9	eleq1i	$⊢ N \in ℕ_{0} \leftrightarrow \|F\| \in ℕ_{0}$
34		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
35	33 34	sylbir	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots N)$
36	32 35	syl	$⊢ F \in Word dom I \to 0 \in (0 \dots N)$
37	8 31 36	3syl	$⊢ φ \to 0 \in (0 \dots N)$
38	24 29 37	rspcdva	$⊢ φ \to Q (0) = P (0)$
39	38	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to Q (0) = P (0)$
40	17	eqcomd	$⊢ φ \to P (0) = C$
41	40	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to P (0) = C$
42	14	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to Q = P \cup \{⟨N + 1, C⟩\}$
43	13	fveq2i	$⊢ \|H\| = \|F \cup \{⟨N, B⟩\}\|$
44	43	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \|H\| = \|F \cup \{⟨N, B⟩\}\|$
45		wrdfin	$⊢ F \in Word dom I \to F \in Fin$
46	30 45	syl	$⊢ F Walks (G) P \to F \in Fin$
47	8 25 46	3syl	$⊢ φ \to F \in Fin$
48	47	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to F \in Fin$
49		snfi	$⊢ \{⟨N, B⟩\} \in Fin$
50	49	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \{⟨N, B⟩\} \in Fin$
51		wrddm	$⊢ F \in Word dom I \to dom F = (0 ..^\|F\|)$
52	8 31 51	3syl	$⊢ φ \to dom F = (0 ..^\|F\|)$
53		fzonel	$⊢ \neg \|F\| \in (0 ..^\|F\|)$
54	53	a1i	$⊢ φ \to \neg \|F\| \in (0 ..^\|F\|)$
55	9	eleq1i	$⊢ N \in (0 ..^\|F\|) \leftrightarrow \|F\| \in (0 ..^\|F\|)$
56	54 55	sylnibr	$⊢ φ \to \neg N \in (0 ..^\|F\|)$
57		eleq2	$⊢ dom F = (0 ..^\|F\|) \to (N \in dom F \leftrightarrow N \in (0 ..^\|F\|))$
58	57	notbid	$⊢ dom F = (0 ..^\|F\|) \to (\neg N \in dom F \leftrightarrow \neg N \in (0 ..^\|F\|))$
59	56 58	syl5ibrcom	$⊢ φ \to (dom F = (0 ..^\|F\|) \to \neg N \in dom F)$
60	9	fvexi	$⊢ N \in V$
61	60	a1i	$⊢ φ \to N \in V$
62	61 5	opeldmd	$⊢ φ \to (⟨N, B⟩ \in F \to N \in dom F)$
63	59 62	nsyld	$⊢ φ \to (dom F = (0 ..^\|F\|) \to \neg ⟨N, B⟩ \in F)$
64	52 63	mpd	$⊢ φ \to \neg ⟨N, B⟩ \in F$
65	64	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to \neg ⟨N, B⟩ \in F$
66		disjsn	$⊢ F \cap \{⟨N, B⟩\} = \emptyset \leftrightarrow \neg ⟨N, B⟩ \in F$
67	65 66	sylibr	$⊢ (φ \land H EulerPaths (S) Q) \to F \cap \{⟨N, B⟩\} = \emptyset$
68		hashun	$⊢ (F \in Fin \land \{⟨N, B⟩\} \in Fin \land F \cap \{⟨N, B⟩\} = \emptyset) \to \|F \cup \{⟨N, B⟩\}\| = \|F\| + \|\{⟨N, B⟩\}\|$
69	48 50 67 68	syl3anc	$⊢ (φ \land H EulerPaths (S) Q) \to \|F \cup \{⟨N, B⟩\}\| = \|F\| + \|\{⟨N, B⟩\}\|$
70	9	eqcomi	$⊢ \|F\| = N$
71		opex	$⊢ ⟨N, B⟩ \in V$
72		hashsng	$⊢ ⟨N, B⟩ \in V \to \|\{⟨N, B⟩\}\| = 1$
73	71 72	ax-mp	$⊢ \|\{⟨N, B⟩\}\| = 1$
74	70 73	oveq12i	$⊢ \|F\| + \|\{⟨N, B⟩\}\| = N + 1$
75	74	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \|F\| + \|\{⟨N, B⟩\}\| = N + 1$
76	44 69 75	3eqtrd	$⊢ (φ \land H EulerPaths (S) Q) \to \|H\| = N + 1$
77	42 76	fveq12d	$⊢ (φ \land H EulerPaths (S) Q) \to Q (\|H\|) = (P \cup \{⟨N + 1, C⟩\}) (N + 1)$
78		ovexd	$⊢ φ \to N + 1 \in V$
79	1 2 3 4 5 6 7 26 9	wlkp1lem1	$⊢ φ \to \neg N + 1 \in dom P$
80	78 6 79	3jca	$⊢ φ \to (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P)$
81	80	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P)$
82		fsnunfv	$⊢ (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P) \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
83	81 82	syl	$⊢ (φ \land H EulerPaths (S) Q) \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
84	77 83	eqtr2d	$⊢ (φ \land H EulerPaths (S) Q) \to C = Q (\|H\|)$
85	39 41 84	3eqtrd	$⊢ (φ \land H EulerPaths (S) Q) \to Q (0) = Q (\|H\|)$
86		iscrct	$⊢ H Circuits (S) Q \leftrightarrow (H Trails (S) Q \land Q (0) = Q (\|H\|))$
87	21 85 86	sylanbrc	$⊢ (φ \land H EulerPaths (S) Q) \to H Circuits (S) Q$
88	19 87	jca	$⊢ (φ \land H EulerPaths (S) Q) \to (H EulerPaths (S) Q \land H Circuits (S) Q)$
89	18 88	mpdan	$⊢ φ \to (H EulerPaths (S) Q \land H Circuits (S) Q)$

Metamath Proof Explorer

Theorem eupth2eucrct

Proof