Theorem pthd

Description: Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	pthd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
	pthd.r	⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
	pthd.s	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
	pthd.f	⊢ ( ♯ ‘ 𝐹 ) = 𝑅
	pthd.t	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
Assertion	pthd	⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		pthd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
2		pthd.r	⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
3		pthd.s	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
4		pthd.f	⊢ ( ♯ ‘ 𝐹 ) = 𝑅
5		pthd.t	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
6	4 2	eqtri	⊢ ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 )
7	4	oveq2i	⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 𝑅 )
8	7	raleqi	⊢ ( ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
9	8	ralbii	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
10	3 9	sylibr	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
11	1 6 10	pthdlem1	⊢ ( 𝜑 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
12	1 6 10	pthdlem2	⊢ ( 𝜑 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
13		ispth	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
14	5 11 12 13	syl3anbrc	⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )