Metamath Proof Explorer

Theorem wlkon2n0

Description: The length of a walk between two different vertices is not 0 (i.e. is at least 1). (Contributed by AV, 3-Apr-2021)

Ref Expression
Assertion wlkon2n0 
|- ( ( F ( A ( WalksOn ` G ) B ) P /\ A =/= B ) -> ( # ` F ) =/= 0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 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 ) ) )
3 fveqeq2 
 |-  ( ( # ` F ) = 0 -> ( ( P ` ( # ` F ) ) = B <-> ( P ` 0 ) = B ) )
4 3 anbi2d 
 |-  ( ( # ` F ) = 0 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( ( P ` 0 ) = A /\ ( P ` 0 ) = B ) ) )
5 eqtr2 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 0 ) = B ) -> A = B )
6 nne 
 |-  ( -. A =/= B <-> A = B )
7 5 6 sylibr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 0 ) = B ) -> -. A =/= B )
8 4 7 syl6bi 
 |-  ( ( # ` F ) = 0 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> -. A =/= B ) )
9 8 com12 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` F ) = 0 -> -. A =/= B ) )
10 9 3adant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` F ) = 0 -> -. A =/= B ) )
11 10 3ad2ant3 
 |-  ( ( ( 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 ) ) -> ( ( # ` F ) = 0 -> -. A =/= B ) )
12 2 11 syl 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( # ` F ) = 0 -> -. A =/= B ) )
13 12 necon2ad 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( A =/= B -> ( # ` F ) =/= 0 ) )
14 13 imp 
 |-  ( ( F ( A ( WalksOn ` G ) B ) P /\ A =/= B ) -> ( # ` F ) =/= 0 )