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