Metamath Proof Explorer

Theorem clwwlkgt0

Description: There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021)

		Ref	Expression
	Assertion	clwwlkgt0	$⊢ W \in ClWWalks (G) \to 0 < \|W\|$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	clwwlkbp	$⊢ W \in ClWWalks (G) \to (G \in V \land W \in Word Vtx (G) \land W \neq \emptyset)$
3		hashgt0	$⊢ (W \in Word Vtx (G) \land W \neq \emptyset) \to 0 < \|W\|$
4	3	3adant1	$⊢ (G \in V \land W \in Word Vtx (G) \land W \neq \emptyset) \to 0 < \|W\|$
5	2 4	syl	$⊢ W \in ClWWalks (G) \to 0 < \|W\|$