Metamath Proof Explorer


Theorem uhgrwkspth

Description: Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021) (Proof shortened by AV, 31-Oct-2021) (Revised by AV, 7-Jul-2022)

Ref Expression
Assertion uhgrwkspth
|- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) )

Proof

Step Hyp Ref Expression
1 simpl31
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Walks ` G ) P )
2 uhgrwkspthlem1
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F )
3 2 expcom
 |-  ( ( # ` F ) = 1 -> ( F ( Walks ` G ) P -> Fun `' F ) )
4 3 3ad2ant2
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( Walks ` G ) P -> Fun `' F ) )
5 4 com12
 |-  ( F ( Walks ` G ) P -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
6 5 3ad2ant1
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
7 6 3ad2ant3
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
8 7 imp
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' F )
9 istrl
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
10 1 8 9 sylanbrc
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Trails ` G ) P )
11 3simpc
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( ( # ` F ) = 1 /\ A =/= B ) )
12 11 adantl
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( # ` F ) = 1 /\ A =/= B ) )
13 3simpc
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
14 13 3ad2ant3
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
15 14 adantr
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
16 uhgrwkspthlem2
 |-  ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )
17 1 12 15 16 syl3anc
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' P )
18 isspth
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
19 10 17 18 sylanbrc
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= 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 19 15 20 sylanbrc
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
22 3simpa
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
23 22 adantr
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
24 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
25 24 isspthonpth
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
26 23 25 syl
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
27 21 26 mpbird
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( A ( SPathsOn ` G ) B ) P )
28 27 ex
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> F ( A ( SPathsOn ` G ) B ) P ) )
29 24 wlkonprop
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
30 3simpc
 |-  ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
31 30 3anim1i
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
32 29 31 syl
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
33 28 32 syl11
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P -> F ( A ( SPathsOn ` G ) B ) P ) )
34 spthonpthon
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( PathsOn ` G ) B ) P )
35 pthontrlon
 |-  ( F ( A ( PathsOn ` G ) B ) P -> F ( A ( TrailsOn ` G ) B ) P )
36 trlsonwlkon
 |-  ( F ( A ( TrailsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
37 34 35 36 3syl
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
38 33 37 impbid1
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) )