This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) )

Proof

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