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 ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 = ∅ ) ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )

Proof

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