Metamath Proof Explorer

Theorem umgr2cwwkdifex

Description: If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 30-Apr-2021)

		Ref	Expression
	Assertion	umgr2cwwkdifex	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to \exists i \in (0 ..^N) W (i) \neq W (0)$

Proof

Step	Hyp	Ref	Expression
1		eluz2b2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3	2	a1i	$⊢ (N \in ℕ \land 1 < N) \to 1 \in ℕ_{0}$
4		simpl	$⊢ (N \in ℕ \land 1 < N) \to N \in ℕ$
5		simpr	$⊢ (N \in ℕ \land 1 < N) \to 1 < N$
6		elfzo0	$⊢ 1 \in (0 ..^N) \leftrightarrow (1 \in ℕ_{0} \land N \in ℕ \land 1 < N)$
7	3 4 5 6	syl3anbrc	$⊢ (N \in ℕ \land 1 < N) \to 1 \in (0 ..^N)$
8	1 7	sylbi	$⊢ N \in ℤ_{\geq 2} \to 1 \in (0 ..^N)$
9	8	3ad2ant2	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to 1 \in (0 ..^N)$
10		fveq2	$⊢ i = 1 \to W (i) = W (1)$
11	10	adantl	$⊢ ((G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \land i = 1) \to W (i) = W (1)$
12	11	neeq1d	$⊢ ((G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \land i = 1) \to (W (i) \neq W (0) \leftrightarrow W (1) \neq W (0))$
13		umgr2cwwk2dif	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to W (1) \neq W (0)$
14	9 12 13	rspcedvd	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to \exists i \in (0 ..^N) W (i) \neq W (0)$