upgr2pthnlp

Description: A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		2pthnloop.i	$⊢ I = iEdg (G)$
2	1	2pthnloop	$⊢ (F Paths (G) P \land 1 < \|F\|) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|$
3	2	3adant1	$⊢ (G \in UPGraph \land F Paths (G) P \land 1 < \|F\|) \to \forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\|$
4		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
5	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
6		simp2	$⊢ (F \in Word dom I \land G \in UPGraph \land i \in (0 ..^\|F\|)) \to G \in UPGraph$
7		wrdsymbcl	$⊢ (F \in Word dom I \land i \in (0 ..^\|F\|)) \to F (i) \in dom I$
8	1	upgrle2	$⊢ (G \in UPGraph \land F (i) \in dom I) \to \|I (F (i))\| \leq 2$
9	6 7 8	3imp3i2an	$⊢ (F \in Word dom I \land G \in UPGraph \land i \in (0 ..^\|F\|)) \to \|I (F (i))\| \leq 2$
10		fvex	$⊢ I (F (i)) \in V$
11		hashxnn0	$⊢ I (F (i)) \in V \to \|I (F (i))\| \in ℕ_{0}^{*}$
12		xnn0xr	$⊢ \|I (F (i))\| \in ℕ_{0}^{} \to \|I (F (i))\| \in ℝ^{}$
13	10 11 12	mp2b	$⊢ \|I (F (i))\| \in ℝ^{*}$
14		2re	$⊢ 2 \in ℝ$
15	14	rexri	$⊢ 2 \in ℝ^{*}$
16	13 15	pm3.2i	$⊢ (\|I (F (i))\| \in ℝ^{} \land 2 \in ℝ^{})$
17		xrletri3	$⊢ (\|I (F (i))\| \in ℝ^{} \land 2 \in ℝ^{}) \to (\|I (F (i))\| = 2 \leftrightarrow (\|I (F (i))\| \leq 2 \land 2 \leq \|I (F (i))\|))$
18	16 17	mp1i	$⊢ (F \in Word dom I \land G \in UPGraph \land i \in (0 ..^\|F\|)) \to (\|I (F (i))\| = 2 \leftrightarrow (\|I (F (i))\| \leq 2 \land 2 \leq \|I (F (i))\|))$
19	18	biimprd	$⊢ (F \in Word dom I \land G \in UPGraph \land i \in (0 ..^\|F\|)) \to ((\|I (F (i))\| \leq 2 \land 2 \leq \|I (F (i))\|) \to \|I (F (i))\| = 2)$
20	9 19	mpand	$⊢ (F \in Word dom I \land G \in UPGraph \land i \in (0 ..^\|F\|)) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2)$
21	20	3exp	$⊢ F \in Word dom I \to (G \in UPGraph \to (i \in (0 ..^\|F\|) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2)))$
22	4 5 21	3syl	$⊢ F Paths (G) P \to (G \in UPGraph \to (i \in (0 ..^\|F\|) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2)))$
23	22	impcom	$⊢ (G \in UPGraph \land F Paths (G) P) \to (i \in (0 ..^\|F\|) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2))$
24	23	3adant3	$⊢ (G \in UPGraph \land F Paths (G) P \land 1 < \|F\|) \to (i \in (0 ..^\|F\|) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2))$
25	24	imp	$⊢ ((G \in UPGraph \land F Paths (G) P \land 1 < \|F\|) \land i \in (0 ..^\|F\|)) \to (2 \leq \|I (F (i))\| \to \|I (F (i))\| = 2)$
26	25	ralimdva	$⊢ (G \in UPGraph \land F Paths (G) P \land 1 < \|F\|) \to (\forall i \in (0 ..^\|F\|) 2 \leq \|I (F (i))\| \to \forall i \in (0 ..^\|F\|) \|I (F (i))\| = 2)$
27	3 26	mpd	$⊢ (G \in UPGraph \land F Paths (G) P \land 1 < \|F\|) \to \forall i \in (0 ..^\|F\|) \|I (F (i))\| = 2$

Metamath Proof Explorer

Theorem upgr2pthnlp

Proof