Metamath Proof Explorer

Theorem usgr2trlspth

Description: In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021)

Ref Expression
Assertion usgr2trlspth ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P ↔ F SPaths ⁡ G P

Proof

Step Hyp Ref Expression
1 usgr2trlncl ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2
2 1 imp ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2
3 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
4 wlkonwlk ⊢ F Walks ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P
5 simpll ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ 2 → G ∈ USGraph
6 simplr ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ 2 → F = 2
7 fveq2 ⊢ F = 2 → P ⁡ F = P ⁡ 2
8 7 eqcomd ⊢ F = 2 → P ⁡ 2 = P ⁡ F
9 8 neeq2d ⊢ F = 2 → P ⁡ 0 ≠ P ⁡ 2 ↔ P ⁡ 0 ≠ P ⁡ F
10 9 biimpd ⊢ F = 2 → P ⁡ 0 ≠ P ⁡ 2 → P ⁡ 0 ≠ P ⁡ F
11 10 adantl ⊢ G ∈ USGraph ∧ F = 2 → P ⁡ 0 ≠ P ⁡ 2 → P ⁡ 0 ≠ P ⁡ F
12 11 imp ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ 2 → P ⁡ 0 ≠ P ⁡ F
13 usgr2wlkspth ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ F → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 SPathsOn ⁡ G P ⁡ F P
14 5 6 12 13 syl3anc ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ 2 → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 SPathsOn ⁡ G P ⁡ F P
15 spthonisspth ⊢ F P ⁡ 0 SPathsOn ⁡ G P ⁡ F P → F SPaths ⁡ G P
16 14 15 syl6bi ⊢ G ∈ USGraph ∧ F = 2 ∧ P ⁡ 0 ≠ P ⁡ 2 → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P → F SPaths ⁡ G P
17 16 expcom ⊢ P ⁡ 0 ≠ P ⁡ 2 → G ∈ USGraph ∧ F = 2 → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P → F SPaths ⁡ G P
18 17 com13 ⊢ F P ⁡ 0 WalksOn ⁡ G P ⁡ F P → G ∈ USGraph ∧ F = 2 → P ⁡ 0 ≠ P ⁡ 2 → F SPaths ⁡ G P
19 3 4 18 3syl ⊢ F Trails ⁡ G P → G ∈ USGraph ∧ F = 2 → P ⁡ 0 ≠ P ⁡ 2 → F SPaths ⁡ G P
20 19 impcom ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2 → F SPaths ⁡ G P
21 2 20 mpd ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → F SPaths ⁡ G P
22 21 ex ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P → F SPaths ⁡ G P
23 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
24 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
25 23 24 syl ⊢ F SPaths ⁡ G P → F Trails ⁡ G P
26 22 25 impbid1 ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P ↔ F SPaths ⁡ G P