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

Metamath Proof Explorer

Theorem umgrwlknloop

Description: In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017) (Revised by AV, 3-Jan-2021)

Ref Expression
Assertion umgrwlknloop ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 umgrupgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 2 upgrwlkvtxedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
4 1 3 sylan ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
5 2 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
6 5 ex ⊢ ( 𝐺 ∈ UMGraph → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
7 6 adantr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
8 7 ralimdv ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
9 4 8 mpd ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )