usgr2wlkspth

Description: In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 27-Jan-2021) (Proof shortened by AV, 31-Oct-2021)

		Ref	Expression
	Assertion	usgr2wlkspth	$⊢ (G \in USGraph \land \|F\| = 2 \land A \neq B) \to (F (A WalksOn (G) B) P \leftrightarrow F (A SPathsOn (G) B) P)$

Proof

Step	Hyp	Ref	Expression
1		simpl31	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to F Walks (G) P$
2		simp2	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to P (0) = A$
3		simp3	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to P (\|F\|) = B$
4	2 3	neeq12d	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (P (0) \neq P (\|F\|) \leftrightarrow A \neq B)$
5	4	bicomd	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (A \neq B \leftrightarrow P (0) \neq P (\|F\|))$
6	5	3anbi3d	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in USGraph \land \|F\| = 2 \land A \neq B) \leftrightarrow (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)))$
7		usgr2wlkspthlem1	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun F^{-1}$
8	7	ex	$⊢ F Walks (G) P \to ((G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to Fun F^{-1})$
9	8	3ad2ant1	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to Fun F^{-1})$
10	6 9	sylbid	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in USGraph \land \|F\| = 2 \land A \neq B) \to Fun F^{-1})$
11	10	3ad2ant3	$⊢ ((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 ((G \in USGraph \land \|F\| = 2 \land A \neq B) \to Fun F^{-1})$
12	11	imp	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to Fun F^{-1}$
13		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
14	1 12 13	sylanbrc	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to F Trails (G) P$
15		usgr2wlkspthlem2	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun P^{-1}$
16	15	ex	$⊢ F Walks (G) P \to ((G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to Fun P^{-1})$
17	16	3ad2ant1	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to Fun P^{-1})$
18	6 17	sylbid	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in USGraph \land \|F\| = 2 \land A \neq B) \to Fun P^{-1})$
19	18	3ad2ant3	$⊢ ((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 ((G \in USGraph \land \|F\| = 2 \land A \neq B) \to Fun P^{-1})$
20	19	imp	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to Fun P^{-1}$
21		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
22	14 20 21	sylanbrc	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to F SPaths (G) P$
23		3simpc	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (P (0) = A \land P (\|F\|) = B)$
24	23	3ad2ant3	$⊢ ((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 (P (0) = A \land P (\|F\|) = B)$
25	24	adantr	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to (P (0) = A \land P (\|F\|) = B)$
26		3anass	$⊢ (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B) \leftrightarrow (F SPaths (G) P \land (P (0) = A \land P (\|F\|) = B))$
27	22 25 26	sylanbrc	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B)$
28		3simpa	$⊢ ((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 ((A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V))$
29	28	adantr	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to ((A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V))$
30		eqid	$⊢ Vtx (G) = Vtx (G)$
31	30	isspthonpth	$⊢ ((A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V)) \to (F (A SPathsOn (G) B) P \leftrightarrow (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B))$
32	29 31	syl	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to (F (A SPathsOn (G) B) P \leftrightarrow (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B))$
33	27 32	mpbird	$⊢ (((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)) \land (G \in USGraph \land \|F\| = 2 \land A \neq B)) \to F (A SPathsOn (G) B) P$
34	33	ex	$⊢ ((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 ((G \in USGraph \land \|F\| = 2 \land A \neq B) \to F (A SPathsOn (G) B) P)$
35	30	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))$
36		3simpc	$⊢ (G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \to (A \in Vtx (G) \land B \in Vtx (G))$
37	36	3anim1i	$⊢ ((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 ((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))$
38	35 37	syl	$⊢ F (A WalksOn (G) B) P \to ((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))$
39	34 38	syl11	$⊢ (G \in USGraph \land \|F\| = 2 \land A \neq B) \to (F (A WalksOn (G) B) P \to F (A SPathsOn (G) B) P)$
40		spthonpthon	$⊢ F (A SPathsOn (G) B) P \to F (A PathsOn (G) B) P$
41		pthontrlon	$⊢ F (A PathsOn (G) B) P \to F (A TrailsOn (G) B) P$
42		trlsonwlkon	$⊢ F (A TrailsOn (G) B) P \to F (A WalksOn (G) B) P$
43	40 41 42	3syl	$⊢ F (A SPathsOn (G) B) P \to F (A WalksOn (G) B) P$
44	39 43	impbid1	$⊢ (G \in USGraph \land \|F\| = 2 \land A \neq B) \to (F (A WalksOn (G) B) P \leftrightarrow F (A SPathsOn (G) B) P)$

Metamath Proof Explorer

Theorem usgr2wlkspth

Proof