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	syl6bi	⊢ ( ( ♯ ‘ 𝐹 ) = 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 )