uhgrwkspth

Description: Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021) (Proof shortened by AV, 31-Oct-2021) (Revised by AV, 7-Jul-2022)

		Ref	Expression
	Assertion	uhgrwkspth	$⊢ (G \in W \land \|F\| = 1 \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 W \land \|F\| = 1 \land A \neq B)) \to F Walks (G) P$
2		uhgrwkspthlem1	$⊢ (F Walks (G) P \land \|F\| = 1) \to Fun F^{-1}$
3	2	expcom	$⊢ \|F\| = 1 \to (F Walks (G) P \to Fun F^{-1})$
4	3	3ad2ant2	$⊢ (G \in W \land \|F\| = 1 \land A \neq B) \to (F Walks (G) P \to Fun F^{-1})$
5	4	com12	$⊢ F Walks (G) P \to ((G \in W \land \|F\| = 1 \land A \neq B) \to Fun F^{-1})$
6	5	3ad2ant1	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to ((G \in W \land \|F\| = 1 \land A \neq B) \to Fun F^{-1})$
7	6	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 W \land \|F\| = 1 \land A \neq B) \to Fun F^{-1})$
8	7	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 W \land \|F\| = 1 \land A \neq B)) \to Fun F^{-1}$
9		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
10	1 8 9	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 W \land \|F\| = 1 \land A \neq B)) \to F Trails (G) P$
11		3simpc	$⊢ (G \in W \land \|F\| = 1 \land A \neq B) \to (\|F\| = 1 \land A \neq B)$
12	11	adantl	$⊢ (((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 W \land \|F\| = 1 \land A \neq B)) \to (\|F\| = 1 \land A \neq B)$
13		3simpc	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (P (0) = A \land P (\|F\|) = B)$
14	13	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)$
15	14	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 W \land \|F\| = 1 \land A \neq B)) \to (P (0) = A \land P (\|F\|) = B)$
16		uhgrwkspthlem2	$⊢ (F Walks (G) P \land (\|F\| = 1 \land A \neq B) \land (P (0) = A \land P (\|F\|) = B)) \to Fun P^{-1}$
17	1 12 15 16	syl3anc	$⊢ (((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 W \land \|F\| = 1 \land A \neq B)) \to Fun P^{-1}$
18		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
19	10 17 18	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 W \land \|F\| = 1 \land A \neq B)) \to F SPaths (G) P$
20		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))$
21	19 15 20	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 W \land \|F\| = 1 \land A \neq B)) \to (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B)$
22		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))$
23	22	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 W \land \|F\| = 1 \land A \neq B)) \to ((A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V))$
24		eqid	$⊢ Vtx (G) = Vtx (G)$
25	24	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))$
26	23 25	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 W \land \|F\| = 1 \land A \neq B)) \to (F (A SPathsOn (G) B) P \leftrightarrow (F SPaths (G) P \land P (0) = A \land P (\|F\|) = B))$
27	21 26	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 W \land \|F\| = 1 \land A \neq B)) \to F (A SPathsOn (G) B) P$
28	27	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 W \land \|F\| = 1 \land A \neq B) \to F (A SPathsOn (G) B) P)$
29	24	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))$
30		3simpc	$⊢ (G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \to (A \in Vtx (G) \land B \in Vtx (G))$
31	30	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))$
32	29 31	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))$
33	28 32	syl11	$⊢ (G \in W \land \|F\| = 1 \land A \neq B) \to (F (A WalksOn (G) B) P \to F (A SPathsOn (G) B) P)$
34		spthonpthon	$⊢ F (A SPathsOn (G) B) P \to F (A PathsOn (G) B) P$
35		pthontrlon	$⊢ F (A PathsOn (G) B) P \to F (A TrailsOn (G) B) P$
36		trlsonwlkon	$⊢ F (A TrailsOn (G) B) P \to F (A WalksOn (G) B) P$
37	34 35 36	3syl	$⊢ F (A SPathsOn (G) B) P \to F (A WalksOn (G) B) P$
38	33 37	impbid1	$⊢ (G \in W \land \|F\| = 1 \land A \neq B) \to (F (A WalksOn (G) B) P \leftrightarrow F (A SPathsOn (G) B) P)$

Metamath Proof Explorer

Theorem uhgrwkspth

Proof