Metamath Proof Explorer

Theorem isspthonpth

Description: A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-Jan-2021)

Ref Expression
Hypothesis isspthonpth.v ⊢ V = Vtx ⁡ G
Assertion isspthonpth ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A SPathsOn ⁡ G B P ↔ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B

Proof

Step Hyp Ref Expression
1 isspthonpth.v ⊢ V = Vtx ⁡ G
2 1 isspthson ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A SPathsOn ⁡ G B P ↔ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
3 1 istrlson ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A TrailsOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
4 3 adantr ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F A TrailsOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
5 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
6 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
7 5 6 syl ⊢ F SPaths ⁡ G P → F Trails ⁡ G P
8 7 adantl ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F Trails ⁡ G P
9 8 biantrud ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F A WalksOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
10 spthiswlk ⊢ F SPaths ⁡ G P → F Walks ⁡ G P
11 10 adantl ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F Walks ⁡ G P
12 1 iswlkon ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
13 3anass ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
14 12 13 syl6bb ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
15 14 adantr ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
16 11 15 mpbirand ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F A WalksOn ⁡ G B P ↔ P ⁡ 0 = A ∧ P ⁡ F = B
17 4 9 16 3bitr2d ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z ∧ F SPaths ⁡ G P → F A TrailsOn ⁡ G B P ↔ P ⁡ 0 = A ∧ P ⁡ F = B
18 17 ex ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F SPaths ⁡ G P → F A TrailsOn ⁡ G B P ↔ P ⁡ 0 = A ∧ P ⁡ F = B
19 18 pm5.32rd ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P ↔ P ⁡ 0 = A ∧ P ⁡ F = B ∧ F SPaths ⁡ G P
20 3anass ⊢ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B ↔ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
21 ancom ⊢ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B ↔ P ⁡ 0 = A ∧ P ⁡ F = B ∧ F SPaths ⁡ G P
22 20 21 bitr2i ⊢ P ⁡ 0 = A ∧ P ⁡ F = B ∧ F SPaths ⁡ G P ↔ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
23 19 22 syl6bb ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P ↔ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
24 2 23 bitrd ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ W ∧ P ∈ Z → F A SPathsOn ⁡ G B P ↔ F SPaths ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B