Metamath Proof Explorer

Theorem isclwlkupgr

Description: Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 11-Apr-2021) (Revised by AV, 28-Oct-2021)

		Ref	Expression
	Hypotheses	isclwlke.v	$⊢ V = Vtx (G)$
		isclwlke.i	$⊢ I = iEdg (G)$
	Assertion	isclwlkupgr	$⊢ G \in UPGraph \to (F ClWalks (G) P \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|))))$

Proof

Step	Hyp	Ref	Expression
1		isclwlke.v	$⊢ V = Vtx (G)$
2		isclwlke.i	$⊢ I = iEdg (G)$
3		isclwlk	$⊢ F ClWalks (G) P \leftrightarrow (F Walks (G) P \land P (0) = P (\|F\|))$
4	1 2	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
5	4	anbi1d	$⊢ G \in UPGraph \to ((F Walks (G) P \land P (0) = P (\|F\|)) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land P (0) = P (\|F\|)))$
6		3an4anass	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land P (0) = P (\|F\|)) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|)))$
7	5 6	bitrdi	$⊢ G \in UPGraph \to ((F Walks (G) P \land P (0) = P (\|F\|)) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|))))$
8	3 7	bitrid	$⊢ G \in UPGraph \to (F ClWalks (G) P \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|))))$