2wlkd

Description: Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018) (Revised by AV, 23-Jan-2021) (Proof shortened by AV, 14-Feb-2021) (Revised by AV, 24-Mar-2021)

	Ref	Expression
Hypotheses	2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
	2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
	2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
	2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
	2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
	2wlkd.v	$⊢ V = Vtx (G)$
	2wlkd.i	$⊢ I = iEdg (G)$
Assertion	2wlkd	$⊢ φ \to F Walks (G) P$

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
2		2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
3		2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
4		2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
5		2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
6		2wlkd.v	$⊢ V = Vtx (G)$
7		2wlkd.i	$⊢ I = iEdg (G)$
8		s3cli	$⊢ ⟨“ A B C ”⟩ \in Word V$
9	1 8	eqeltri	$⊢ P \in Word V$
10	9	a1i	$⊢ φ \to P \in Word V$
11		s2cli	$⊢ ⟨“ J K ”⟩ \in Word V$
12	2 11	eqeltri	$⊢ F \in Word V$
13	12	a1i	$⊢ φ \to F \in Word V$
14	1 2	2wlkdlem1	$⊢ \|P\| = \|F\| + 1$
15	14	a1i	$⊢ φ \to \|P\| = \|F\| + 1$
16	1 2 3 4 5	2wlkdlem10	$⊢ φ \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
17	1 2 3 4	2wlkdlem5	$⊢ φ \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$
18	6	1vgrex	$⊢ A \in V \to G \in V$
19	18	3ad2ant1	$⊢ (A \in V \land B \in V \land C \in V) \to G \in V$
20	3 19	syl	$⊢ φ \to G \in V$
21	1 2 3	2wlkdlem4	$⊢ φ \to \forall k \in (0 \dots \|F\|) P (k) \in V$
22	10 13 15 16 17 20 6 7 21	wlkd	$⊢ φ \to F Walks (G) P$

Metamath Proof Explorer

Theorem 2wlkd

Proof