Theorem wlk1ewlk

Description: A walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021)

	Ref	Expression
Assertion	wlk1ewlk	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ ( 𝐺 EdgWalks 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2	1	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
3	1	wlk1walk	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
4		wlkv	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
5	4	simp1d	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐺 ∈ V )
6		1nn0	⊢ 1 ∈ ℕ0
7		nn0xnn0	⊢ ( 1 ∈ ℕ0 → 1 ∈ ℕ0* )
8	6 7	mp1i	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 1 ∈ ℕ0* )
9	1	isewlk	⊢ ( ( 𝐺 ∈ V ∧ 1 ∈ ℕ0* ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 1 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
10	5 8 2 9	syl3anc	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ ( 𝐺 EdgWalks 1 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
11	2 3 10	mpbir2and	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ ( 𝐺 EdgWalks 1 ) )