Metamath Proof Explorer

Theorem 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 ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → W ⁡ 1 ≠ W ⁡ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 clwwlknp ⊢ W ∈ N ClWWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
4 simpr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℤ ≥ 2 ∧ G ∈ UMGraph → G ∈ UMGraph
5 uz2m1nn ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ
6 lbfzo0 ⊢ 0 ∈ 0 ..^ N − 1 ↔ N − 1 ∈ ℕ
7 5 6 sylibr ⊢ N ∈ ℤ ≥ 2 → 0 ∈ 0 ..^ N − 1
8 fveq2 ⊢ i = 0 → W ⁡ i = W ⁡ 0
9 8 adantl ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → W ⁡ i = W ⁡ 0
10 oveq1 ⊢ i = 0 → i + 1 = 0 + 1
11 10 adantl ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → i + 1 = 0 + 1
12 0p1e1 ⊢ 0 + 1 = 1
13 11 12 eqtrdi ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → i + 1 = 1
14 13 fveq2d ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → W ⁡ i + 1 = W ⁡ 1
15 9 14 preq12d ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → W ⁡ i W ⁡ i + 1 = W ⁡ 0 W ⁡ 1
16 15 eleq1d ⊢ N ∈ ℤ ≥ 2 ∧ i = 0 → W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
17 7 16 rspcdv ⊢ N ∈ ℤ ≥ 2 → ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
18 17 com12 ⊢ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → N ∈ ℤ ≥ 2 → W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
19 18 3ad2ant2 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → N ∈ ℤ ≥ 2 → W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
20 19 imp ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℤ ≥ 2 → W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
21 20 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℤ ≥ 2 ∧ G ∈ UMGraph → W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
22 2 umgredgne ⊢ G ∈ UMGraph ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G → W ⁡ 0 ≠ W ⁡ 1
23 22 necomd ⊢ G ∈ UMGraph ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G → W ⁡ 1 ≠ W ⁡ 0
24 4 21 23 syl2anc ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℤ ≥ 2 ∧ G ∈ UMGraph → W ⁡ 1 ≠ W ⁡ 0
25 24 exp31 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → N ∈ ℤ ≥ 2 → G ∈ UMGraph → W ⁡ 1 ≠ W ⁡ 0
26 3 25 syl ⊢ W ∈ N ClWWalksN G → N ∈ ℤ ≥ 2 → G ∈ UMGraph → W ⁡ 1 ≠ W ⁡ 0
27 26 3imp31 ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → W ⁡ 1 ≠ W ⁡ 0