This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ 𝐹 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wlkonprop ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
3 fveqeq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ↔ ( 𝑃 ‘ 0 ) = 𝐵 ) )
4 3 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) ) )
5 eqtr2 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → 𝐴 = 𝐵 )
6 nne ⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 )
7 5 6 sylibr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → ¬ 𝐴 ≠ 𝐵 )
8 4 7 biimtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ¬ 𝐴 ≠ 𝐵 ) )
9 8 com12 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) )
10 9 3adant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) )
11 10 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) )
12 2 11 syl ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) )
13 12 necon2ad ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 ≠ 𝐵 → ( ♯ ‘ 𝐹 ) ≠ 0 ) )
14 13 imp ⊢ ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ 𝐹 ) ≠ 0 )