Metamath Proof Explorer

Theorem upgristrl

Description: Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 29-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		upgrtrls.v	$⊢ V = Vtx (G)$
2		upgrtrls.i	$⊢ I = iEdg (G)$
3		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
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 Fun F^{-1}) \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 Fun F^{-1}))$
6		an32	$⊢ ((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 Fun F^{-1}) \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land (P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
7		3anass	$⊢ (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)\}) \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)\}))$
8	7	anbi1i	$⊢ ((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 Fun F^{-1}) \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 Fun F^{-1})$
9		3anass	$⊢ ((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land (P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
10	6 8 9	3bitr4i	$⊢ ((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 Fun F^{-1}) \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
11	5 10	bitrdi	$⊢ G \in UPGraph \to ((F Walks (G) P \land Fun F^{-1}) \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
12	3 11	syl5bb	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$