ewlkinedg

Description: The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021)

		Ref	Expression
	Hypothesis	ewlksfval.i	$⊢ I = iEdg (G)$
	Assertion	ewlkinedg	$⊢ (F \in (G EdgWalks S) \land K \in (1 ..^\|F\|)) \to S \leq \|I (F (K - 1)) \cap I (F (K))\|$

Step	Hyp	Ref	Expression
1		ewlksfval.i	$⊢ I = iEdg (G)$
2	1	ewlkprop	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|)$
3		fvoveq1	$⊢ k = K \to F (k - 1) = F (K - 1)$
4	3	fveq2d	$⊢ k = K \to I (F (k - 1)) = I (F (K - 1))$
5		2fveq3	$⊢ k = K \to I (F (k)) = I (F (K))$
6	4 5	ineq12d	$⊢ k = K \to I (F (k - 1)) \cap I (F (k)) = I (F (K - 1)) \cap I (F (K))$
7	6	fveq2d	$⊢ k = K \to \|I (F (k - 1)) \cap I (F (k))\| = \|I (F (K - 1)) \cap I (F (K))\|$
8	7	breq2d	$⊢ k = K \to (S \leq \|I (F (k - 1)) \cap I (F (k))\| \leftrightarrow S \leq \|I (F (K - 1)) \cap I (F (K))\|)$
9	8	rspccv	$⊢ \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\| \to (K \in (1 ..^\|F\|) \to S \leq \|I (F (K - 1)) \cap I (F (K))\|)$
10	9	3ad2ant3	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom I \land \forall k \in (1 ..^\|F\|) S \leq \|I (F (k - 1)) \cap I (F (k))\|) \to (K \in (1 ..^\|F\|) \to S \leq \|I (F (K - 1)) \cap I (F (K))\|)$
11	2 10	syl	$⊢ F \in (G EdgWalks S) \to (K \in (1 ..^\|F\|) \to S \leq \|I (F (K - 1)) \cap I (F (K))\|)$
12	11	imp	$⊢ (F \in (G EdgWalks S) \land K \in (1 ..^\|F\|)) \to S \leq \|I (F (K - 1)) \cap I (F (K))\|$

Metamath Proof Explorer