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