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