Metamath Proof Explorer

Theorem wlkelwrd

Description: The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 2-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	wlkelwrd	$⊢ W \in Walks (G) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)$

Proof

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	1 2 3 4	wlkcompim	$⊢ W \in Walks (G) \to (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))))$
6		3simpa	$⊢ (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)))) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)$
7	5 6	syl	$⊢ W \in Walks (G) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)$