wlkp1

Description: Append one path segment (edge) E from vertex ( PN ) to a vertex C to a walk <. F , P >. to become a walk <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 . (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 6-Mar-2021) (Proof shortened by AV, 18-Apr-2021) (Revised by AV, 8-Apr-2024)

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

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	$⊢ V = Vtx (G)$
2		wlkp1.i	$⊢ I = iEdg (G)$
3		wlkp1.f	$⊢ φ \to Fun I$
4		wlkp1.a	$⊢ φ \to I \in Fin$
5		wlkp1.b	$⊢ φ \to B \in W$
6		wlkp1.c	$⊢ φ \to C \in V$
7		wlkp1.d	$⊢ φ \to \neg B \in dom I$
8		wlkp1.w	$⊢ φ \to F Walks (G) P$
9		wlkp1.n	$⊢ N = \|F\|$
10		wlkp1.e	$⊢ φ \to E \in Edg (G)$
11		wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
12		wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
13		wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
14		wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
15		wlkp1.s	$⊢ φ \to Vtx (S) = V$
16		wlkp1.l	$⊢ (φ \land C = P (N)) \to E = \{C\}$
17	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
18		wrdf	$⊢ F \in Word dom I \to F : (0 ..^\|F\|) ⟶ dom I$
19	9	eqcomi	$⊢ \|F\| = N$
20	19	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^N)$
21	20	feq2i	$⊢ F : (0 ..^\|F\|) ⟶ dom I \leftrightarrow F : (0 ..^N) ⟶ dom I$
22	18 21	sylib	$⊢ F \in Word dom I \to F : (0 ..^N) ⟶ dom I$
23	8 17 22	3syl	$⊢ φ \to F : (0 ..^N) ⟶ dom I$
24	9	fvexi	$⊢ N \in V$
25	24	a1i	$⊢ φ \to N \in V$
26		snidg	$⊢ B \in W \to B \in \{B\}$
27	5 26	syl	$⊢ φ \to B \in \{B\}$
28		dmsnopg	$⊢ E \in Edg (G) \to dom \{⟨B, E⟩\} = \{B\}$
29	10 28	syl	$⊢ φ \to dom \{⟨B, E⟩\} = \{B\}$
30	27 29	eleqtrrd	$⊢ φ \to B \in dom \{⟨B, E⟩\}$
31	25 30	fsnd	$⊢ φ \to \{⟨N, B⟩\} : \{N\} ⟶ dom \{⟨B, E⟩\}$
32		fzodisjsn	$⊢ (0 ..^N) \cap \{N\} = \emptyset$
33	32	a1i	$⊢ φ \to (0 ..^N) \cap \{N\} = \emptyset$
34		fun	$⊢ ((F : (0 ..^N) ⟶ dom I \land \{⟨N, B⟩\} : \{N\} ⟶ dom \{⟨B, E⟩\}) \land (0 ..^N) \cap \{N\} = \emptyset) \to (F \cup \{⟨N, B⟩\}) : (0 ..^N) \cup \{N\} ⟶ dom I \cup dom \{⟨B, E⟩\}$
35	23 31 33 34	syl21anc	$⊢ φ \to (F \cup \{⟨N, B⟩\}) : (0 ..^N) \cup \{N\} ⟶ dom I \cup dom \{⟨B, E⟩\}$
36	13	a1i	$⊢ φ \to H = F \cup \{⟨N, B⟩\}$
37	1 2 3 4 5 6 7 8 9 10 11 12 13	wlkp1lem2	$⊢ φ \to \|H\| = N + 1$
38	37	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N + 1)$
39		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
40		eleq1	$⊢ \|F\| = N \to (\|F\| \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
41	40	eqcoms	$⊢ N = \|F\| \to (\|F\| \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
42		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
43	42	biimpi	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq 0}$
44	41 43	biimtrdi	$⊢ N = \|F\| \to (\|F\| \in ℕ_{0} \to N \in ℤ_{\geq 0})$
45	9 44	ax-mp	$⊢ \|F\| \in ℕ_{0} \to N \in ℤ_{\geq 0}$
46	8 39 45	3syl	$⊢ φ \to N \in ℤ_{\geq 0}$
47		fzosplitsn	$⊢ N \in ℤ_{\geq 0} \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
48	46 47	syl	$⊢ φ \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
49	38 48	eqtrd	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N) \cup \{N\}$
50	12	dmeqd	$⊢ φ \to dom iEdg (S) = dom (I \cup \{⟨B, E⟩\})$
51		dmun	$⊢ dom (I \cup \{⟨B, E⟩\}) = dom I \cup dom \{⟨B, E⟩\}$
52	50 51	eqtrdi	$⊢ φ \to dom iEdg (S) = dom I \cup dom \{⟨B, E⟩\}$
53	36 49 52	feq123d	$⊢ φ \to (H : (0 ..^\|H\|) ⟶ dom iEdg (S) \leftrightarrow (F \cup \{⟨N, B⟩\}) : (0 ..^N) \cup \{N\} ⟶ dom I \cup dom \{⟨B, E⟩\})$
54	35 53	mpbird	$⊢ φ \to H : (0 ..^\|H\|) ⟶ dom iEdg (S)$
55		iswrdb	$⊢ H \in Word dom iEdg (S) \leftrightarrow H : (0 ..^\|H\|) ⟶ dom iEdg (S)$
56	54 55	sylibr	$⊢ φ \to H \in Word dom iEdg (S)$
57	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
58	8 57	syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$
59	9	oveq2i	$⊢ (0 \dots N) = (0 \dots \|F\|)$
60	59	feq2i	$⊢ P : (0 \dots N) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V$
61	58 60	sylibr	$⊢ φ \to P : (0 \dots N) ⟶ V$
62		ovexd	$⊢ φ \to N + 1 \in V$
63	62 6	fsnd	$⊢ φ \to \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ V$
64		fzp1disj	$⊢ (0 \dots N) \cap \{N + 1\} = \emptyset$
65	64	a1i	$⊢ φ \to (0 \dots N) \cap \{N + 1\} = \emptyset$
66		fun	$⊢ ((P : (0 \dots N) ⟶ V \land \{⟨N + 1, C⟩\} : \{N + 1\} ⟶ V) \land (0 \dots N) \cap \{N + 1\} = \emptyset) \to (P \cup \{⟨N + 1, C⟩\}) : (0 \dots N) \cup \{N + 1\} ⟶ V \cup V$
67	61 63 65 66	syl21anc	$⊢ φ \to (P \cup \{⟨N + 1, C⟩\}) : (0 \dots N) \cup \{N + 1\} ⟶ V \cup V$
68		fzsuc	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N + 1) = (0 \dots N) \cup \{N + 1\}$
69	46 68	syl	$⊢ φ \to (0 \dots N + 1) = (0 \dots N) \cup \{N + 1\}$
70		unidm	$⊢ V \cup V = V$
71	70	eqcomi	$⊢ V = V \cup V$
72	71	a1i	$⊢ φ \to V = V \cup V$
73	69 72	feq23d	$⊢ φ \to ((P \cup \{⟨N + 1, C⟩\}) : (0 \dots N + 1) ⟶ V \leftrightarrow (P \cup \{⟨N + 1, C⟩\}) : (0 \dots N) \cup \{N + 1\} ⟶ V \cup V)$
74	67 73	mpbird	$⊢ φ \to (P \cup \{⟨N + 1, C⟩\}) : (0 \dots N + 1) ⟶ V$
75	14	a1i	$⊢ φ \to Q = P \cup \{⟨N + 1, C⟩\}$
76	37	oveq2d	$⊢ φ \to (0 \dots \|H\|) = (0 \dots N + 1)$
77	75 76 15	feq123d	$⊢ φ \to (Q : (0 \dots \|H\|) ⟶ Vtx (S) \leftrightarrow (P \cup \{⟨N + 1, C⟩\}) : (0 \dots N + 1) ⟶ V)$
78	74 77	mpbird	$⊢ φ \to Q : (0 \dots \|H\|) ⟶ Vtx (S)$
79	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	wlkp1lem8	$⊢ φ \to \forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))$
80	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem4	$⊢ φ \to (S \in V \land H \in V \land Q \in V)$
81		eqid	$⊢ Vtx (S) = Vtx (S)$
82		eqid	$⊢ iEdg (S) = iEdg (S)$
83	81 82	iswlk	$⊢ (S \in V \land H \in V \land Q \in V) \to (H Walks (S) Q \leftrightarrow (H \in Word dom iEdg (S) \land Q : (0 \dots \|H\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))))$
84	80 83	syl	$⊢ φ \to (H Walks (S) Q \leftrightarrow (H \in Word dom iEdg (S) \land Q : (0 \dots \|H\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))))$
85	56 78 79 84	mpbir3and	$⊢ φ \to H Walks (S) Q$

Metamath Proof Explorer

Theorem wlkp1

Proof