umgr2cwwk2dif

Description: If a word represents a closed walk of length at least 2 in a multigraph, 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	umgr2cwwk2dif	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to W (1) \neq W (0)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	clwwlknp	$⊢ W \in (N ClWWalksN G) \to ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G))$
4		simpr	$⊢ ((((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land N \in ℤ_{\geq 2}) \land G \in UMGraph) \to G \in UMGraph$
5		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
6		lbfzo0	$⊢ 0 \in (0 ..^N - 1) \leftrightarrow N - 1 \in ℕ$
7	5 6	sylibr	$⊢ N \in ℤ_{\geq 2} \to 0 \in (0 ..^N - 1)$
8		fveq2	$⊢ i = 0 \to W (i) = W (0)$
9	8	adantl	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to W (i) = W (0)$
10		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
11	10	adantl	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to i + 1 = 0 + 1$
12		0p1e1	$⊢ 0 + 1 = 1$
13	11 12	eqtrdi	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to i + 1 = 1$
14	13	fveq2d	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to W (i + 1) = W (1)$
15	9 14	preq12d	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to \{W (i), W (i + 1)\} = \{W (0), W (1)\}$
16	15	eleq1d	$⊢ (N \in ℤ_{\geq 2} \land i = 0) \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (0), W (1)\} \in Edg (G))$
17	7 16	rspcdv	$⊢ N \in ℤ_{\geq 2} \to (\forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \to \{W (0), W (1)\} \in Edg (G))$
18	17	com12	$⊢ \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \to (N \in ℤ_{\geq 2} \to \{W (0), W (1)\} \in Edg (G))$
19	18	3ad2ant2	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \to (N \in ℤ_{\geq 2} \to \{W (0), W (1)\} \in Edg (G))$
20	19	imp	$⊢ (((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land N \in ℤ_{\geq 2}) \to \{W (0), W (1)\} \in Edg (G)$
21	20	adantr	$⊢ ((((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land N \in ℤ_{\geq 2}) \land G \in UMGraph) \to \{W (0), W (1)\} \in Edg (G)$
22	2	umgredgne	$⊢ (G \in UMGraph \land \{W (0), W (1)\} \in Edg (G)) \to W (0) \neq W (1)$
23	22	necomd	$⊢ (G \in UMGraph \land \{W (0), W (1)\} \in Edg (G)) \to W (1) \neq W (0)$
24	4 21 23	syl2anc	$⊢ ((((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land N \in ℤ_{\geq 2}) \land G \in UMGraph) \to W (1) \neq W (0)$
25	24	exp31	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \to (N \in ℤ_{\geq 2} \to (G \in UMGraph \to W (1) \neq W (0)))$
26	3 25	syl	$⊢ W \in (N ClWWalksN G) \to (N \in ℤ_{\geq 2} \to (G \in UMGraph \to W (1) \neq W (0)))$
27	26	3imp31	$⊢ (G \in UMGraph \land N \in ℤ_{\geq 2} \land W \in (N ClWWalksN G)) \to W (1) \neq W (0)$

Metamath Proof Explorer

Theorem umgr2cwwk2dif

Proof