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 ⊢ G ∈ UMGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 umgrupgr ⊢ G ∈ UMGraph → G ∈ UPGraph
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 2 upgrwlkvtxedg ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G
4 1 3 sylan ⊢ G ∈ UMGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G
5 2 umgredgne ⊢ G ∈ UMGraph ∧ P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G → P ⁡ k ≠ P ⁡ k + 1
6 5 ex ⊢ G ∈ UMGraph → P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G → P ⁡ k ≠ P ⁡ k + 1
7 6 adantr ⊢ G ∈ UMGraph ∧ F Walks ⁡ G P → P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G → P ⁡ k ≠ P ⁡ k + 1
8 7 ralimdv ⊢ G ∈ UMGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ Edg ⁡ G → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
9 4 8 mpd ⊢ G ∈ UMGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1