spthcycl

Description: A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023)

		Ref	Expression
	Assertion	spthcycl	$⊢ (F Paths (G) P \land F = \emptyset) \leftrightarrow (F SPaths (G) P \land F Cycles (G) P)$

Proof

Step	Hyp	Ref	Expression
1		pthistrl	$⊢ F Paths (G) P \to F Trails (G) P$
2		pthiswlk	$⊢ F Paths (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	4	ffund	$⊢ F Walks (G) P \to Fun P$
6		wlklenvp1	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$
7	6	adantr	$⊢ (F Walks (G) P \land F = \emptyset) \to \|P\| = \|F\| + 1$
8		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
9	8	simp2d	$⊢ F Walks (G) P \to F \in V$
10		hasheq0	$⊢ F \in V \to (\|F\| = 0 \leftrightarrow F = \emptyset)$
11	10	biimpar	$⊢ (F \in V \land F = \emptyset) \to \|F\| = 0$
12	9 11	sylan	$⊢ (F Walks (G) P \land F = \emptyset) \to \|F\| = 0$
13		oveq1	$⊢ \|F\| = 0 \to \|F\| + 1 = 0 + 1$
14		0p1e1	$⊢ 0 + 1 = 1$
15	13 14	eqtrdi	$⊢ \|F\| = 0 \to \|F\| + 1 = 1$
16	12 15	syl	$⊢ (F Walks (G) P \land F = \emptyset) \to \|F\| + 1 = 1$
17	7 16	eqtrd	$⊢ (F Walks (G) P \land F = \emptyset) \to \|P\| = 1$
18	8	simp3d	$⊢ F Walks (G) P \to P \in V$
19		hashen1	$⊢ P \in V \to (\|P\| = 1 \leftrightarrow P \approx 1_{𝑜})$
20	18 19	syl	$⊢ F Walks (G) P \to (\|P\| = 1 \leftrightarrow P \approx 1_{𝑜})$
21	20	biimpa	$⊢ (F Walks (G) P \land \|P\| = 1) \to P \approx 1_{𝑜}$
22	17 21	syldan	$⊢ (F Walks (G) P \land F = \emptyset) \to P \approx 1_{𝑜}$
23		funen1cnv	$⊢ (Fun P \land P \approx 1_{𝑜}) \to Fun P^{-1}$
24	5 22 23	syl2an2r	$⊢ (F Walks (G) P \land F = \emptyset) \to Fun P^{-1}$
25	2 24	sylan	$⊢ (F Paths (G) P \land F = \emptyset) \to Fun P^{-1}$
26		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
27	26	biimpri	$⊢ (F Trails (G) P \land Fun P^{-1}) \to F SPaths (G) P$
28	1 25 27	syl2an2r	$⊢ (F Paths (G) P \land F = \emptyset) \to F SPaths (G) P$
29		fveq2	$⊢ 0 = \|F\| \to P (0) = P (\|F\|)$
30	29	eqcoms	$⊢ \|F\| = 0 \to P (0) = P (\|F\|)$
31	12 30	syl	$⊢ (F Walks (G) P \land F = \emptyset) \to P (0) = P (\|F\|)$
32	2 31	sylan	$⊢ (F Paths (G) P \land F = \emptyset) \to P (0) = P (\|F\|)$
33		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
34	33	biimpri	$⊢ (F Paths (G) P \land P (0) = P (\|F\|)) \to F Cycles (G) P$
35	32 34	syldan	$⊢ (F Paths (G) P \land F = \emptyset) \to F Cycles (G) P$
36	28 35	jca	$⊢ (F Paths (G) P \land F = \emptyset) \to (F SPaths (G) P \land F Cycles (G) P)$
37		spthispth	$⊢ F SPaths (G) P \to F Paths (G) P$
38	37	adantr	$⊢ (F SPaths (G) P \land F Cycles (G) P) \to F Paths (G) P$
39		notnot	$⊢ F SPaths (G) P \to \neg \neg F SPaths (G) P$
40		cyclnspth	$⊢ F \neq \emptyset \to (F Cycles (G) P \to \neg F SPaths (G) P)$
41	40	com12	$⊢ F Cycles (G) P \to (F \neq \emptyset \to \neg F SPaths (G) P)$
42	41	con3dimp	$⊢ (F Cycles (G) P \land \neg \neg F SPaths (G) P) \to \neg F \neq \emptyset$
43		nne	$⊢ \neg F \neq \emptyset \leftrightarrow F = \emptyset$
44	42 43	sylib	$⊢ (F Cycles (G) P \land \neg \neg F SPaths (G) P) \to F = \emptyset$
45	39 44	sylan2	$⊢ (F Cycles (G) P \land F SPaths (G) P) \to F = \emptyset$
46	45	ancoms	$⊢ (F SPaths (G) P \land F Cycles (G) P) \to F = \emptyset$
47	38 46	jca	$⊢ (F SPaths (G) P \land F Cycles (G) P) \to (F Paths (G) P \land F = \emptyset)$
48	36 47	impbii	$⊢ (F Paths (G) P \land F = \emptyset) \leftrightarrow (F SPaths (G) P \land F Cycles (G) P)$

Metamath Proof Explorer

Theorem spthcycl

Proof