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 ) )