wlkd

Description: Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	$⊢ φ \to P \in Word V$
	wlkd.f	$⊢ φ \to F \in Word V$
	wlkd.l	$⊢ φ \to \|P\| = \|F\| + 1$
	wlkd.e	$⊢ φ \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
	wlkd.n	$⊢ φ \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$
	wlkd.g	$⊢ φ \to G \in W$
	wlkd.v	$⊢ V = Vtx (G)$
	wlkd.i	$⊢ I = iEdg (G)$
	wlkd.a	$⊢ φ \to \forall k \in (0 \dots \|F\|) P (k) \in V$
Assertion	wlkd	$⊢ φ \to F Walks (G) P$

Step	Hyp	Ref	Expression
1		wlkd.p	$⊢ φ \to P \in Word V$
2		wlkd.f	$⊢ φ \to F \in Word V$
3		wlkd.l	$⊢ φ \to \|P\| = \|F\| + 1$
4		wlkd.e	$⊢ φ \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
5		wlkd.n	$⊢ φ \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$
6		wlkd.g	$⊢ φ \to G \in W$
7		wlkd.v	$⊢ V = Vtx (G)$
8		wlkd.i	$⊢ I = iEdg (G)$
9		wlkd.a	$⊢ φ \to \forall k \in (0 \dots \|F\|) P (k) \in V$
10	1 2 3 4	wlkdlem3	$⊢ φ \to F \in Word dom I$
11	1 2 3 9	wlkdlem1	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$
12	1 2 3 4 5	wlkdlem4	$⊢ φ \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
13	7 8	iswlk	$⊢ (G \in W \land F \in Word V \land P \in Word V) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
14	6 2 1 13	syl3anc	$⊢ φ \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
15	10 11 12 14	mpbir3and	$⊢ φ \to F Walks (G) P$

Metamath Proof Explorer