Metamath Proof Explorer

Theorem spthcycl

Description: A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023)

Ref Expression
Assertion spthcycl ⊢ F Paths ⁡ G P ∧ F = ∅ ↔ F SPaths ⁡ G P ∧ F Cycles ⁡ G P

Proof

Step Hyp Ref Expression
1 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
2 pthiswlk ⊢ F Paths ⁡ G P → F Walks ⁡ G P
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ Vtx ⁡ G
5 4 ffund ⊢ F Walks ⁡ G P → Fun ⁡ P
6 wlklenvp1 ⊢ F Walks ⁡ G P → P = F + 1
7 6 adantr ⊢ F Walks ⁡ G P ∧ F = ∅ → P = F + 1
8 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
9 8 simp2d ⊢ F Walks ⁡ G P → F ∈ V
10 hasheq0 ⊢ F ∈ V → F = 0 ↔ F = ∅
11 10 biimpar ⊢ F ∈ V ∧ F = ∅ → F = 0
12 9 11 sylan ⊢ F Walks ⁡ G P ∧ F = ∅ → F = 0
13 oveq1 ⊢ F = 0 → F + 1 = 0 + 1
14 0p1e1 ⊢ 0 + 1 = 1
15 13 14 eqtrdi ⊢ F = 0 → F + 1 = 1
16 12 15 syl ⊢ F Walks ⁡ G P ∧ F = ∅ → F + 1 = 1
17 7 16 eqtrd ⊢ F Walks ⁡ G P ∧ F = ∅ → P = 1
18 8 simp3d ⊢ F Walks ⁡ G P → P ∈ V
19 hashen1 ⊢ P ∈ V → P = 1 ↔ P ≈ 1 𝑜
20 18 19 syl ⊢ F Walks ⁡ G P → P = 1 ↔ P ≈ 1 𝑜
21 20 biimpa ⊢ F Walks ⁡ G P ∧ P = 1 → P ≈ 1 𝑜
22 17 21 syldan ⊢ F Walks ⁡ G P ∧ F = ∅ → P ≈ 1 𝑜
23 funen1cnv ⊢ Fun ⁡ P ∧ P ≈ 1 𝑜 → Fun ⁡ P -1
24 5 22 23 syl2an2r ⊢ F Walks ⁡ G P ∧ F = ∅ → Fun ⁡ P -1
25 2 24 sylan ⊢ F Paths ⁡ G P ∧ F = ∅ → Fun ⁡ P -1
26 isspth ⊢ F SPaths ⁡ G P ↔ F Trails ⁡ G P ∧ Fun ⁡ P -1
27 26 biimpri ⊢ F Trails ⁡ G P ∧ Fun ⁡ P -1 → F SPaths ⁡ G P
28 1 25 27 syl2an2r ⊢ F Paths ⁡ G P ∧ F = ∅ → F SPaths ⁡ G P
29 fveq2 ⊢ 0 = F → P ⁡ 0 = P ⁡ F
30 29 eqcoms ⊢ F = 0 → P ⁡ 0 = P ⁡ F
31 12 30 syl ⊢ F Walks ⁡ G P ∧ F = ∅ → P ⁡ 0 = P ⁡ F
32 2 31 sylan ⊢ F Paths ⁡ G P ∧ F = ∅ → P ⁡ 0 = P ⁡ F
33 iscycl ⊢ F Cycles ⁡ G P ↔ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
34 33 biimpri ⊢ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F Cycles ⁡ G P
35 32 34 syldan ⊢ F Paths ⁡ G P ∧ F = ∅ → F Cycles ⁡ G P
36 28 35 jca ⊢ F Paths ⁡ G P ∧ F = ∅ → F SPaths ⁡ G P ∧ F Cycles ⁡ G P
37 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
38 37 adantr ⊢ F SPaths ⁡ G P ∧ F Cycles ⁡ G P → F Paths ⁡ G P
39 notnot ⊢ F SPaths ⁡ G P → ¬ ¬ F SPaths ⁡ G P
40 cyclnspth ⊢ F ≠ ∅ → F Cycles ⁡ G P → ¬ F SPaths ⁡ G P
41 40 com12 ⊢ F Cycles ⁡ G P → F ≠ ∅ → ¬ F SPaths ⁡ G P
42 41 con3dimp ⊢ F Cycles ⁡ G P ∧ ¬ ¬ F SPaths ⁡ G P → ¬ F ≠ ∅
43 nne ⊢ ¬ F ≠ ∅ ↔ F = ∅
44 42 43 sylib ⊢ F Cycles ⁡ G P ∧ ¬ ¬ F SPaths ⁡ G P → F = ∅
45 39 44 sylan2 ⊢ F Cycles ⁡ G P ∧ F SPaths ⁡ G P → F = ∅
46 45 ancoms ⊢ F SPaths ⁡ G P ∧ F Cycles ⁡ G P → F = ∅
47 38 46 jca ⊢ F SPaths ⁡ G P ∧ F Cycles ⁡ G P → F Paths ⁡ G P ∧ F = ∅
48 36 47 impbii ⊢ F Paths ⁡ G P ∧ F = ∅ ↔ F SPaths ⁡ G P ∧ F Cycles ⁡ G P