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 ⊢ φ → P ∈ Word V
pthd.r ⊢ R = P − 1
pthd.s ⊢ φ → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
pthd.f ⊢ F = R
pthd.t ⊢ φ → F Trails ⁡ G P
Assertion pthd ⊢ φ → F Paths ⁡ G P

Proof

Step Hyp Ref Expression
1 pthd.p ⊢ φ → P ∈ Word V
2 pthd.r ⊢ R = P − 1
3 pthd.s ⊢ φ → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
4 pthd.f ⊢ F = R
5 pthd.t ⊢ φ → F Trails ⁡ G P
6 4 2 eqtri ⊢ F = P − 1
7 4 oveq2i ⊢ 1 ..^ F = 1 ..^ R
8 7 raleqi ⊢ ∀ j ∈ 1 ..^ F i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
9 8 ralbii ⊢ ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ F i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
10 3 9 sylibr ⊢ φ → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ F i ≠ j → P ⁡ i ≠ P ⁡ j
11 1 6 10 pthdlem1 ⊢ φ → Fun ⁡ P ↾ 1 ..^ F -1
12 1 6 10 pthdlem2 ⊢ φ → P 0 F ∩ P 1 ..^ F = ∅
13 ispth ⊢ F Paths ⁡ G P ↔ F Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ F -1 ∧ P 0 F ∩ P 1 ..^ F = ∅
14 5 11 12 13 syl3anbrc ⊢ φ → F Paths ⁡ G P