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		lencl	$⊢ F \in Word dom I \to \|F\| \in ℕ_{0}$
32	9	eleq1i	$⊢ N \in ℕ_{0} \leftrightarrow \|F\| \in ℕ_{0}$
33		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
34	32 33	sylbir	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots N)$
35	31 34	syl	$⊢ F \in Word dom I \to 0 \in (0 \dots N)$
36	8 25 30 35	4syl	$⊢ φ \to 0 \in (0 \dots N)$
37	24 29 36	rspcdva	$⊢ φ \to Q (0) = P (0)$
38	37	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to Q (0) = P (0)$
39	17	eqcomd	$⊢ φ \to P (0) = C$
40	39	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to P (0) = C$
41	14	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to Q = P \cup \{⟨N + 1, C⟩\}$
42	13	fveq2i	$⊢ \|H\| = \|F \cup \{⟨N, B⟩\}\|$
43	42	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \|H\| = \|F \cup \{⟨N, B⟩\}\|$
44		wrdfin	$⊢ F \in Word dom I \to F \in Fin$
45	8 25 30 44	4syl	$⊢ φ \to F \in Fin$
46	45	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to F \in Fin$
47		snfi	$⊢ \{⟨N, B⟩\} \in Fin$
48	47	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \{⟨N, B⟩\} \in Fin$
49		wrddm	$⊢ F \in Word dom I \to dom F = (0 ..^\|F\|)$
50	8 25 30 49	4syl	$⊢ φ \to dom F = (0 ..^\|F\|)$
51		fzonel	$⊢ \neg \|F\| \in (0 ..^\|F\|)$
52	51	a1i	$⊢ φ \to \neg \|F\| \in (0 ..^\|F\|)$
53	9	eleq1i	$⊢ N \in (0 ..^\|F\|) \leftrightarrow \|F\| \in (0 ..^\|F\|)$
54	52 53	sylnibr	$⊢ φ \to \neg N \in (0 ..^\|F\|)$
55		eleq2	$⊢ dom F = (0 ..^\|F\|) \to (N \in dom F \leftrightarrow N \in (0 ..^\|F\|))$
56	55	notbid	$⊢ dom F = (0 ..^\|F\|) \to (\neg N \in dom F \leftrightarrow \neg N \in (0 ..^\|F\|))$
57	54 56	syl5ibrcom	$⊢ φ \to (dom F = (0 ..^\|F\|) \to \neg N \in dom F)$
58	9	fvexi	$⊢ N \in V$
59	58	a1i	$⊢ φ \to N \in V$
60	59 5	opeldmd	$⊢ φ \to (⟨N, B⟩ \in F \to N \in dom F)$
61	57 60	nsyld	$⊢ φ \to (dom F = (0 ..^\|F\|) \to \neg ⟨N, B⟩ \in F)$
62	50 61	mpd	$⊢ φ \to \neg ⟨N, B⟩ \in F$
63	62	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to \neg ⟨N, B⟩ \in F$
64		disjsn	$⊢ F \cap \{⟨N, B⟩\} = \emptyset \leftrightarrow \neg ⟨N, B⟩ \in F$
65	63 64	sylibr	$⊢ (φ \land H EulerPaths (S) Q) \to F \cap \{⟨N, B⟩\} = \emptyset$
66		hashun	$⊢ (F \in Fin \land \{⟨N, B⟩\} \in Fin \land F \cap \{⟨N, B⟩\} = \emptyset) \to \|F \cup \{⟨N, B⟩\}\| = \|F\| + \|\{⟨N, B⟩\}\|$
67	46 48 65 66	syl3anc	$⊢ (φ \land H EulerPaths (S) Q) \to \|F \cup \{⟨N, B⟩\}\| = \|F\| + \|\{⟨N, B⟩\}\|$
68	9	eqcomi	$⊢ \|F\| = N$
69		opex	$⊢ ⟨N, B⟩ \in V$
70		hashsng	$⊢ ⟨N, B⟩ \in V \to \|\{⟨N, B⟩\}\| = 1$
71	69 70	ax-mp	$⊢ \|\{⟨N, B⟩\}\| = 1$
72	68 71	oveq12i	$⊢ \|F\| + \|\{⟨N, B⟩\}\| = N + 1$
73	72	a1i	$⊢ (φ \land H EulerPaths (S) Q) \to \|F\| + \|\{⟨N, B⟩\}\| = N + 1$
74	43 67 73	3eqtrd	$⊢ (φ \land H EulerPaths (S) Q) \to \|H\| = N + 1$
75	41 74	fveq12d	$⊢ (φ \land H EulerPaths (S) Q) \to Q (\|H\|) = (P \cup \{⟨N + 1, C⟩\}) (N + 1)$
76		ovexd	$⊢ φ \to N + 1 \in V$
77	1 2 3 4 5 6 7 26 9	wlkp1lem1	$⊢ φ \to \neg N + 1 \in dom P$
78	76 6 77	3jca	$⊢ φ \to (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P)$
79	78	adantr	$⊢ (φ \land H EulerPaths (S) Q) \to (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P)$
80		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$
81	79 80	syl	$⊢ (φ \land H EulerPaths (S) Q) \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
82	75 81	eqtr2d	$⊢ (φ \land H EulerPaths (S) Q) \to C = Q (\|H\|)$
83	38 40 82	3eqtrd	$⊢ (φ \land H EulerPaths (S) Q) \to Q (0) = Q (\|H\|)$
84		iscrct	$⊢ H Circuits (S) Q \leftrightarrow (H Trails (S) Q \land Q (0) = Q (\|H\|))$
85	21 83 84	sylanbrc	$⊢ (φ \land H EulerPaths (S) Q) \to H Circuits (S) Q$
86	19 85	jca	$⊢ (φ \land H EulerPaths (S) Q) \to (H EulerPaths (S) Q \land H Circuits (S) Q)$
87	18 86	mpdan	$⊢ φ \to (H EulerPaths (S) Q \land H Circuits (S) Q)$

Metamath Proof Explorer

Theorem eupth2eucrct

Proof