3wlkd

Description: Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021) (Revised by AV, 24-Mar-2021)

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

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