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 \land A \neq B) \to \|F\| \neq 0$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	wlkonprop	$⊢ F (A WalksOn (G) B) P \to ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
3		fveqeq2	$⊢ \|F\| = 0 \to (P (\|F\|) = B \leftrightarrow P (0) = B)$
4	3	anbi2d	$⊢ \|F\| = 0 \to ((P (0) = A \land P (\|F\|) = B) \leftrightarrow (P (0) = A \land P (0) = B))$
5		eqtr2	$⊢ (P (0) = A \land P (0) = B) \to A = B$
6		nne	$⊢ \neg A \neq B \leftrightarrow A = B$
7	5 6	sylibr	$⊢ (P (0) = A \land P (0) = B) \to \neg A \neq B$
8	4 7	biimtrdi	$⊢ \|F\| = 0 \to ((P (0) = A \land P (\|F\|) = B) \to \neg A \neq B)$
9	8	com12	$⊢ (P (0) = A \land P (\|F\|) = B) \to (\|F\| = 0 \to \neg A \neq B)$
10	9	3adant1	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (\|F\| = 0 \to \neg A \neq B)$
11	10	3ad2ant3	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B)) \to (\|F\| = 0 \to \neg A \neq B)$
12	2 11	syl	$⊢ F (A WalksOn (G) B) P \to (\|F\| = 0 \to \neg A \neq B)$
13	12	necon2ad	$⊢ F (A WalksOn (G) B) P \to (A \neq B \to \|F\| \neq 0)$
14	13	imp	$⊢ (F (A WalksOn (G) B) P \land A \neq B) \to \|F\| \neq 0$

Metamath Proof Explorer