spthonepeq

Description: The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 18-Jan-2021) (Proof shortened by AV, 31-Oct-2021)

		Ref	Expression
	Assertion	spthonepeq	$⊢ F (A SPathsOn (G) B) P \to (A = B \leftrightarrow \|F\| = 0)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	spthonprop	$⊢ F (A SPathsOn (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 (A TrailsOn (G) B) P \land F SPaths (G) P))$
3	1	istrlson	$⊢ ((A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to (F (A TrailsOn (G) B) P \leftrightarrow (F (A WalksOn (G) B) P \land F Trails (G) P))$
4	3	3adantl1	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to (F (A TrailsOn (G) B) P \leftrightarrow (F (A WalksOn (G) B) P \land F Trails (G) P))$
5		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
6	5	a1i	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to (F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1}))$
7	4 6	anbi12d	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to ((F (A TrailsOn (G) B) P \land F SPaths (G) P) \leftrightarrow ((F (A WalksOn (G) B) P \land F Trails (G) P) \land (F Trails (G) P \land Fun P^{-1})))$
8	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))$
9		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
10	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
11		df-f1	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \leftrightarrow (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun P^{-1})$
12		eqeq2	$⊢ A = B \to (P (0) = A \leftrightarrow P (0) = B)$
13		eqtr3	$⊢ (P (\|F\|) = B \land P (0) = B) \to P (\|F\|) = P (0)$
14		elnn0uz	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in ℤ_{\geq 0}$
15		eluzfz2	$⊢ \|F\| \in ℤ_{\geq 0} \to \|F\| \in (0 \dots \|F\|)$
16	14 15	sylbi	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in (0 \dots \|F\|)$
17		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
18	16 17	jca	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \in (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
19		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)$
20	18 19	sylan2	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land \|F\| \in ℕ_{0}) \to (P (\|F\|) = P (0) \to \|F\| = 0)$
21	20	ex	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to (\|F\| \in ℕ_{0} \to (P (\|F\|) = P (0) \to \|F\| = 0))$
22	21	com13	$⊢ P (\|F\|) = P (0) \to (\|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to \|F\| = 0))$
23	13 22	syl	$⊢ (P (\|F\|) = B \land P (0) = B) \to (\|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to \|F\| = 0))$
24	23	expcom	$⊢ P (0) = B \to (P (\|F\|) = B \to (\|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to \|F\| = 0)))$
25	12 24	biimtrdi	$⊢ A = B \to (P (0) = A \to (P (\|F\|) = B \to (\|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to \|F\| = 0))))$
26	25	com15	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \to (P (0) = A \to (P (\|F\|) = B \to (\|F\| \in ℕ_{0} \to (A = B \to \|F\| = 0))))$
27	11 26	sylbir	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun P^{-1}) \to (P (0) = A \to (P (\|F\|) = B \to (\|F\| \in ℕ_{0} \to (A = B \to \|F\| = 0))))$
28	27	expcom	$⊢ Fun P^{-1} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to (P (0) = A \to (P (\|F\|) = B \to (\|F\| \in ℕ_{0} \to (A = B \to \|F\| = 0)))))$
29	28	com15	$⊢ \|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to (P (0) = A \to (P (\|F\|) = B \to (Fun P^{-1} \to (A = B \to \|F\| = 0)))))$
30	9 10 29	sylc	$⊢ F Walks (G) P \to (P (0) = A \to (P (\|F\|) = B \to (Fun P^{-1} \to (A = B \to \|F\| = 0))))$
31	30	3imp1	$⊢ ((F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \land Fun P^{-1}) \to (A = B \to \|F\| = 0)$
32		fveqeq2	$⊢ \|F\| = 0 \to (P (\|F\|) = B \leftrightarrow P (0) = B)$
33	32	anbi2d	$⊢ \|F\| = 0 \to ((P (0) = A \land P (\|F\|) = B) \leftrightarrow (P (0) = A \land P (0) = B))$
34		eqtr2	$⊢ (P (0) = A \land P (0) = B) \to A = B$
35	33 34	biimtrdi	$⊢ \|F\| = 0 \to ((P (0) = A \land P (\|F\|) = B) \to A = B)$
36	35	com12	$⊢ (P (0) = A \land P (\|F\|) = B) \to (\|F\| = 0 \to A = B)$
37	36	3adant1	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (\|F\| = 0 \to A = B)$
38	37	adantr	$⊢ ((F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \land Fun P^{-1}) \to (\|F\| = 0 \to A = B)$
39	31 38	impbid	$⊢ ((F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \land Fun P^{-1}) \to (A = B \leftrightarrow \|F\| = 0)$
40	39	ex	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (Fun P^{-1} \to (A = B \leftrightarrow \|F\| = 0))$
41	40	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 (Fun P^{-1} \to (A = B \leftrightarrow \|F\| = 0))$
42	8 41	syl	$⊢ F (A WalksOn (G) B) P \to (Fun P^{-1} \to (A = B \leftrightarrow \|F\| = 0))$
43	42	adantld	$⊢ F (A WalksOn (G) B) P \to ((F Trails (G) P \land Fun P^{-1}) \to (A = B \leftrightarrow \|F\| = 0))$
44	43	adantr	$⊢ (F (A WalksOn (G) B) P \land F Trails (G) P) \to ((F Trails (G) P \land Fun P^{-1}) \to (A = B \leftrightarrow \|F\| = 0))$
45	44	imp	$⊢ ((F (A WalksOn (G) B) P \land F Trails (G) P) \land (F Trails (G) P \land Fun P^{-1})) \to (A = B \leftrightarrow \|F\| = 0)$
46	7 45	biimtrdi	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to ((F (A TrailsOn (G) B) P \land F SPaths (G) P) \to (A = B \leftrightarrow \|F\| = 0))$
47	46	3impia	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V) \land (F (A TrailsOn (G) B) P \land F SPaths (G) P)) \to (A = B \leftrightarrow \|F\| = 0)$
48	2 47	syl	$⊢ F (A SPathsOn (G) B) P \to (A = B \leftrightarrow \|F\| = 0)$

Metamath Proof Explorer

Theorem spthonepeq

Proof