Theorem wlkonwlk

Description: A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 31-Jan-2021)

	Ref	Expression
Assertion	wlkonwlk	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2		eqidd	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
3		eqidd	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5	4	wlkepvtx	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) )
6		wlkv	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
7		3simpc	⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
8	6 7	syl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
9	4	iswlkon	⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
10	5 8 9	syl2anc	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
11	1 2 3 10	mpbir3and	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )