Theorem wlkd

Description: Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
	wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
	wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
	wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
	wlkd.n	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
	wlkd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	wlkd.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wlkd.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	wlkd.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
Assertion	wlkd	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
2		wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
3		wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
4		wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
5		wlkd.n	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
6		wlkd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
7		wlkd.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
8		wlkd.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
9		wlkd.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
10	1 2 3 4	wlkdlem3	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
11	1 2 3 9	wlkdlem1	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
12	1 2 3 4 5	wlkdlem4	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
13	7 8	iswlk	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
14	6 2 1 13	syl3anc	⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
15	10 11 12 14	mpbir3and	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )