Metamath Proof Explorer

Theorem umgr2cwwkdifex

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

Ref Expression
Assertion umgr2cwwkdifex ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → ∃ i ∈ 0 ..^ N W ⁡ i ≠ W ⁡ 0

Proof

Step Hyp Ref Expression
1 eluz2b2 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℕ ∧ 1 < N
2 1nn0 ⊢ 1 ∈ ℕ 0
3 2 a1i ⊢ N ∈ ℕ ∧ 1 < N → 1 ∈ ℕ 0
4 simpl ⊢ N ∈ ℕ ∧ 1 < N → N ∈ ℕ
5 simpr ⊢ N ∈ ℕ ∧ 1 < N → 1 < N
6 elfzo0 ⊢ 1 ∈ 0 ..^ N ↔ 1 ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N
7 3 4 5 6 syl3anbrc ⊢ N ∈ ℕ ∧ 1 < N → 1 ∈ 0 ..^ N
8 1 7 sylbi ⊢ N ∈ ℤ ≥ 2 → 1 ∈ 0 ..^ N
9 8 3ad2ant2 ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → 1 ∈ 0 ..^ N
10 fveq2 ⊢ i = 1 → W ⁡ i = W ⁡ 1
11 10 adantl ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G ∧ i = 1 → W ⁡ i = W ⁡ 1
12 11 neeq1d ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G ∧ i = 1 → W ⁡ i ≠ W ⁡ 0 ↔ W ⁡ 1 ≠ W ⁡ 0
13 umgr2cwwk2dif ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → W ⁡ 1 ≠ W ⁡ 0
14 9 12 13 rspcedvd ⊢ G ∈ UMGraph ∧ N ∈ ℤ ≥ 2 ∧ W ∈ N ClWWalksN G → ∃ i ∈ 0 ..^ N W ⁡ i ≠ W ⁡ 0