isupwlk

Description: Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 28-Dec-2020)

	Ref	Expression
Hypotheses	upwlksfval.v	$⊢ V = Vtx (G)$
	upwlksfval.i	$⊢ I = iEdg (G)$
Assertion	isupwlk	$⊢ (G \in W \land F \in U \land P \in Z) \to (F UPWalks (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)\}))$

Proof

Step	Hyp	Ref	Expression
1		upwlksfval.v	$⊢ V = Vtx (G)$
2		upwlksfval.i	$⊢ I = iEdg (G)$
3		df-br	$⊢ F UPWalks (G) P \leftrightarrow ⟨F, P⟩ \in UPWalks (G)$
4	1 2	upwlksfval	$⊢ G \in W \to UPWalks (G) = \{⟨f, p⟩ \| (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	3ad2ant1	$⊢ (G \in W \land F \in U \land P \in Z) \to UPWalks (G) = \{⟨f, p⟩ \| (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)\})\}$
6	5	eleq2d	$⊢ (G \in W \land F \in U \land P \in Z) \to (⟨F, P⟩ \in UPWalks (G) \leftrightarrow ⟨F, P⟩ \in \{⟨f, p⟩ \| (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)\})\})$
7	3 6	syl5bb	$⊢ (G \in W \land F \in U \land P \in Z) \to (F UPWalks (G) P \leftrightarrow ⟨F, P⟩ \in \{⟨f, p⟩ \| (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		eleq1	$⊢ f = F \to (f \in Word dom I \leftrightarrow F \in Word dom I)$
9	8	adantr	$⊢ (f = F \land p = P) \to (f \in Word dom I \leftrightarrow F \in Word dom I)$
10		simpr	$⊢ (f = F \land p = P) \to p = P$
11		fveq2	$⊢ f = F \to \|f\| = \|F\|$
12	11	oveq2d	$⊢ f = F \to (0 \dots \|f\|) = (0 \dots \|F\|)$
13	12	adantr	$⊢ (f = F \land p = P) \to (0 \dots \|f\|) = (0 \dots \|F\|)$
14	10 13	feq12d	$⊢ (f = F \land p = P) \to (p : (0 \dots \|f\|) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
15	11	oveq2d	$⊢ f = F \to (0 ..^\|f\|) = (0 ..^\|F\|)$
16	15	adantr	$⊢ (f = F \land p = P) \to (0 ..^\|f\|) = (0 ..^\|F\|)$
17		fveq1	$⊢ f = F \to f (k) = F (k)$
18	17	fveq2d	$⊢ f = F \to I (f (k)) = I (F (k))$
19		fveq1	$⊢ p = P \to p (k) = P (k)$
20		fveq1	$⊢ p = P \to p (k + 1) = P (k + 1)$
21	19 20	preq12d	$⊢ p = P \to \{p (k), p (k + 1)\} = \{P (k), P (k + 1)\}$
22	18 21	eqeqan12d	$⊢ (f = F \land p = P) \to (I (f (k)) = \{p (k), p (k + 1)\} \leftrightarrow I (F (k)) = \{P (k), P (k + 1)\})$
23	16 22	raleqbidv	$⊢ (f = F \land p = P) \to (\forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\} \leftrightarrow \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
24	9 14 23	3anbi123d	$⊢ (f = F \land p = P) \to ((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)\}))$
25	24	opelopabga	$⊢ (F \in U \land P \in Z) \to (⟨F, P⟩ \in \{⟨f, p⟩ \| (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)\}))$
26	25	3adant1	$⊢ (G \in W \land F \in U \land P \in Z) \to (⟨F, P⟩ \in \{⟨f, p⟩ \| (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)\}))$
27	7 26	bitrd	$⊢ (G \in W \land F \in U \land P \in Z) \to (F UPWalks (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)\}))$

Metamath Proof Explorer

Theorem isupwlk

Proof