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 V A Vtx G B Vtx G F V P 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 V A Vtx G B Vtx G F V P 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