umgrclwwlkge2

Description: A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018) (Revised by AV, 24-Apr-2021)

		Ref	Expression
	Assertion	umgrclwwlkge2	$⊢ G \in UMGraph \to (P \in ClWWalks (G) \to 2 \leq \|P\|)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	clwwlkbp	$⊢ P \in ClWWalks (G) \to (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)$
3	2	adantl	$⊢ (G \in UMGraph \land P \in ClWWalks (G)) \to (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)$
4		lencl	$⊢ P \in Word Vtx (G) \to \|P\| \in ℕ_{0}$
5	4	3ad2ant2	$⊢ (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \in ℕ_{0}$
6	5	adantl	$⊢ ((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to \|P\| \in ℕ_{0}$
7		hasheq0	$⊢ P \in Word Vtx (G) \to (\|P\| = 0 \leftrightarrow P = \emptyset)$
8	7	bicomd	$⊢ P \in Word Vtx (G) \to (P = \emptyset \leftrightarrow \|P\| = 0)$
9	8	necon3bid	$⊢ P \in Word Vtx (G) \to (P \neq \emptyset \leftrightarrow \|P\| \neq 0)$
10	9	biimpd	$⊢ P \in Word Vtx (G) \to (P \neq \emptyset \to \|P\| \neq 0)$
11	10	a1i	$⊢ G \in V \to (P \in Word Vtx (G) \to (P \neq \emptyset \to \|P\| \neq 0))$
12	11	3imp	$⊢ (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 0$
13	12	adantl	$⊢ ((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to \|P\| \neq 0$
14		clwwlk1loop	$⊢ (P \in ClWWalks (G) \land \|P\| = 1) \to \{P (0), P (0)\} \in Edg (G)$
15	14	expcom	$⊢ \|P\| = 1 \to (P \in ClWWalks (G) \to \{P (0), P (0)\} \in Edg (G))$
16		eqid	$⊢ P (0) = P (0)$
17		eqid	$⊢ Edg (G) = Edg (G)$
18	17	umgredgne	$⊢ (G \in UMGraph \land \{P (0), P (0)\} \in Edg (G)) \to P (0) \neq P (0)$
19		eqneqall	$⊢ P (0) = P (0) \to (P (0) \neq P (0) \to ((G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 1))$
20	16 18 19	mpsyl	$⊢ (G \in UMGraph \land \{P (0), P (0)\} \in Edg (G)) \to ((G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 1)$
21	20	expcom	$⊢ \{P (0), P (0)\} \in Edg (G) \to (G \in UMGraph \to ((G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 1))$
22	15 21	syl6	$⊢ \|P\| = 1 \to (P \in ClWWalks (G) \to (G \in UMGraph \to ((G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 1)))$
23	22	com23	$⊢ \|P\| = 1 \to (G \in UMGraph \to (P \in ClWWalks (G) \to ((G \in V \land P \in Word Vtx (G) \land P \neq \emptyset) \to \|P\| \neq 1)))$
24	23	imp4c	$⊢ \|P\| = 1 \to (((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to \|P\| \neq 1)$
25		neqne	$⊢ \neg \|P\| = 1 \to \|P\| \neq 1$
26	25	a1d	$⊢ \neg \|P\| = 1 \to (((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to \|P\| \neq 1)$
27	24 26	pm2.61i	$⊢ ((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to \|P\| \neq 1$
28	6 13 27	3jca	$⊢ ((G \in UMGraph \land P \in ClWWalks (G)) \land (G \in V \land P \in Word Vtx (G) \land P \neq \emptyset)) \to (\|P\| \in ℕ_{0} \land \|P\| \neq 0 \land \|P\| \neq 1)$
29	3 28	mpdan	$⊢ (G \in UMGraph \land P \in ClWWalks (G)) \to (\|P\| \in ℕ_{0} \land \|P\| \neq 0 \land \|P\| \neq 1)$
30		nn0n0n1ge2	$⊢ (\|P\| \in ℕ_{0} \land \|P\| \neq 0 \land \|P\| \neq 1) \to 2 \leq \|P\|$
31	29 30	syl	$⊢ (G \in UMGraph \land P \in ClWWalks (G)) \to 2 \leq \|P\|$
32	31	ex	$⊢ G \in UMGraph \to (P \in ClWWalks (G) \to 2 \leq \|P\|)$

Metamath Proof Explorer

Theorem umgrclwwlkge2

Proof