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

Proof

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