wlkcomp

Description: A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-Jan-2021)

	Ref	Expression
Hypotheses	wlkcomp.v	$⊢ V = Vtx (G)$
	wlkcomp.i	$⊢ I = iEdg (G)$
	wlkcomp.1	$⊢ F = 1^{st} (W)$
	wlkcomp.2	$⊢ P = 2^{nd} (W)$
Assertion	wlkcomp	$⊢ (G \in U \land W \in (S \times T)) \to (W \in Walks (G) \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)))))$

Step	Hyp	Ref	Expression
1		wlkcomp.v	$⊢ V = Vtx (G)$
2		wlkcomp.i	$⊢ I = iEdg (G)$
3		wlkcomp.1	$⊢ F = 1^{st} (W)$
4		wlkcomp.2	$⊢ P = 2^{nd} (W)$
5	3	eqcomi	$⊢ 1^{st} (W) = F$
6	4	eqcomi	$⊢ 2^{nd} (W) = P$
7	5 6	pm3.2i	$⊢ (1^{st} (W) = F \land 2^{nd} (W) = P)$
8		eqop	$⊢ W \in (S \times T) \to (W = ⟨F, P⟩ \leftrightarrow (1^{st} (W) = F \land 2^{nd} (W) = P))$
9	7 8	mpbiri	$⊢ W \in (S \times T) \to W = ⟨F, P⟩$
10	9	eleq1d	$⊢ W \in (S \times T) \to (W \in Walks (G) \leftrightarrow ⟨F, P⟩ \in Walks (G))$
11		df-br	$⊢ F Walks (G) P \leftrightarrow ⟨F, P⟩ \in Walks (G)$
12	10 11	bitr4di	$⊢ W \in (S \times T) \to (W \in Walks (G) \leftrightarrow F Walks (G) P)$
13	1 2	iswlkg	$⊢ G \in U \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	12 13	sylan9bbr	$⊢ (G \in U \land W \in (S \times T)) \to (W \in Walks (G) \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)))))$

Metamath Proof Explorer