This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) 𝑃 )