2pthnloop

Description: A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon . (Contributed by AV, 6-Feb-2021)

		Ref	Expression
	Hypothesis	2pthnloop.i	$⊢ I = iEdg (G)$
	Assertion	2pthnloop	$⊢ (F Paths (G) P \land 1 < \|F\|) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|$

Proof

Step	Hyp	Ref	Expression
1		2pthnloop.i	$⊢ I = iEdg (G)$
2		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
3		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
4	2 3	syl	$⊢ F Paths (G) P \to (G \in V \land F \in V \land P \in V)$
5		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
6		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
7		eqid	$⊢ Vtx (G) = Vtx (G)$
8	7 1	iswlkg	$⊢ G \in V \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))))$
9	8	anbi1d	$⊢ G \in V \to ((F Walks (G) P \land Fun F^{-1}) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \land Fun F^{-1}))$
10	6 9	bitrid	$⊢ G \in V \to (F Trails (G) P \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \land Fun F^{-1}))$
11		pthdadjvtx	$⊢ (F Paths (G) P \land 1 < \|F\| \land i \in (0 ..^\|F\|)) \to P (i) \neq P (i + 1)$
12	11	ad5ant245	$⊢ (((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \to P (i) \neq P (i + 1)$
13	12	neneqd	$⊢ (((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \to \neg P (i) = P (i + 1)$
14		ifpfal	$⊢ \neg P (i) = P (i + 1) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow \{P (i), P (i + 1)\} \subseteq I (F (i)))$
15	14	adantl	$⊢ ((((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \land \neg P (i) = P (i + 1)) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow \{P (i), P (i + 1)\} \subseteq I (F (i)))$
16		fvexd	$⊢ \neg P (i) = P (i + 1) \to P (i) \in V$
17		fvexd	$⊢ \neg P (i) = P (i + 1) \to P (i + 1) \in V$
18		neqne	$⊢ \neg P (i) = P (i + 1) \to P (i) \neq P (i + 1)$
19		fvexd	$⊢ \neg P (i) = P (i + 1) \to I (F (i)) \in V$
20		prsshashgt1	$⊢ ((P (i) \in V \land P (i + 1) \in V \land P (i) \neq P (i + 1)) \land I (F (i)) \in V) \to (\{P (i), P (i + 1)\} \subseteq I (F (i)) \to 2 \leq \|I (F (i))\|)$
21	16 17 18 19 20	syl31anc	$⊢ \neg P (i) = P (i + 1) \to (\{P (i), P (i + 1)\} \subseteq I (F (i)) \to 2 \leq \|I (F (i))\|)$
22	21	adantl	$⊢ ((((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \land \neg P (i) = P (i + 1)) \to (\{P (i), P (i + 1)\} \subseteq I (F (i)) \to 2 \leq \|I (F (i))\|)$
23	15 22	sylbid	$⊢ ((((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \land \neg P (i) = P (i + 1)) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to 2 \leq \|I (F (i))\|)$
24	13 23	mpdan	$⊢ (((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to 2 \leq \|I (F (i))\|)$
25	24	ralimdva	$⊢ ((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \land 1 < \|F\|) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)$
26	25	ex	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \to (1 < \|F\| \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))$
27	26	com23	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land F Paths (G) P) \land ((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))$
28	27	exp31	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (F Paths (G) P \to (((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))))$
29	28	com24	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to (((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))))$
30	29	3impia	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \to (((Fun F^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))$
31	30	exp4c	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \to (Fun F^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))))$
32	31	imp	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \land Fun F^{-1}) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))))$
33	10 32	syl6bi	$⊢ G \in V \to (F Trails (G) P \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))))$
34	33	com24	$⊢ G \in V \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to (F Trails (G) P \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))))$
35	34	com14	$⊢ F Trails (G) P \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to (G \in V \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))))$
36	35	3imp	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to (G \in V \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))$
37	36	com12	$⊢ G \in V \to ((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))$
38	5 37	biimtrid	$⊢ G \in V \to (F Paths (G) P \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))$
39	38	3ad2ant1	$⊢ (G \in V \land F \in V \land P \in V) \to (F Paths (G) P \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)))$
40	4 39	mpcom	$⊢ F Paths (G) P \to (F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|))$
41	40	pm2.43i	$⊢ F Paths (G) P \to (1 < \|F\| \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|)$
42	41	imp	$⊢ (F Paths (G) P \land 1 < \|F\|) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|$

Metamath Proof Explorer

Theorem 2pthnloop

Proof