2clwwlklem

		Ref	Expression
	Assertion	2clwwlklem	$⊢ (W \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) (0) = W (0)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	clwwlknwrd	$⊢ W \in (N ClWWalksN G) \to W \in Word Vtx (G)$
3		ige3m2fz	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in (1 \dots N)$
4	3	adantl	$⊢ (W \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to N - 2 \in (1 \dots N)$
5		clwwlknlen	$⊢ W \in (N ClWWalksN G) \to \|W\| = N$
6	5	oveq2d	$⊢ W \in (N ClWWalksN G) \to (1 \dots \|W\|) = (1 \dots N)$
7	6	eleq2d	$⊢ W \in (N ClWWalksN G) \to (N - 2 \in (1 \dots \|W\|) \leftrightarrow N - 2 \in (1 \dots N))$
8	7	adantr	$⊢ (W \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to (N - 2 \in (1 \dots \|W\|) \leftrightarrow N - 2 \in (1 \dots N))$
9	4 8	mpbird	$⊢ (W \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to N - 2 \in (1 \dots \|W\|)$
10		pfxfv0	$⊢ (W \in Word Vtx (G) \land N - 2 \in (1 \dots \|W\|)) \to (W prefix (N - 2)) (0) = W (0)$
11	2 9 10	syl2an2r	$⊢ (W \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) (0) = W (0)$

Metamath Proof Explorer