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 ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )

Proof

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