spthdep

Description: A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	spthdep	$⊢ (F SPaths (G) P \land \|F\| \neq 0) \to P (0) \neq P (\|F\|)$

Proof

Step	Hyp	Ref	Expression
1		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
2		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4	3	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
5	2 4	syl	$⊢ F Trails (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
6	5	anim1i	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun P^{-1})$
7		df-f1	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \leftrightarrow (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun P^{-1})$
8	6 7	sylibr	$⊢ (F Trails (G) P \land Fun P^{-1}) \to P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)$
9		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
10		nn0fz0	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in (0 \dots \|F\|)$
11	10	biimpi	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in (0 \dots \|F\|)$
12		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
13	11 12	jca	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
14	2 9 13	3syl	$⊢ F Trails (G) P \to (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
15	14	adantr	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
16	8 15	jca	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|)))$
17		eqcom	$⊢ P (0) = P (\|F\|) \leftrightarrow P (\|F\|) = P (0)$
18		f1veqaeq	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))) \to (P (\|F\|) = P (0) \to \|F\| = 0)$
19	17 18	syl5bi	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))) \to (P (0) = P (\|F\|) \to \|F\| = 0)$
20	16 19	syl	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (P (0) = P (\|F\|) \to \|F\| = 0)$
21	20	necon3d	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (\|F\| \neq 0 \to P (0) \neq P (\|F\|))$
22	1 21	sylbi	$⊢ F SPaths (G) P \to (\|F\| \neq 0 \to P (0) \neq P (\|F\|))$
23	22	imp	$⊢ (F SPaths (G) P \land \|F\| \neq 0) \to P (0) \neq P (\|F\|)$

Metamath Proof Explorer

Theorem spthdep

Proof