iswlk

Description: Properties of a pair of functions to be/represent a walk. (Contributed by AV, 30-Dec-2020)

	Ref	Expression
Hypotheses	wksfval.v	$⊢ V = Vtx (G)$
	wksfval.i	$⊢ I = iEdg (G)$
Assertion	iswlk	$⊢ (G \in W \land F \in U \land P \in Z) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$

Proof

Step	Hyp	Ref	Expression
1		wksfval.v	$⊢ V = Vtx (G)$
2		wksfval.i	$⊢ I = iEdg (G)$
3		df-br	$⊢ F Walks (G) P \leftrightarrow ⟨F, P⟩ \in Walks (G)$
4	1 2	wksfval	$⊢ G \in W \to Walks (G) = \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\}$
5	4	3ad2ant1	$⊢ (G \in W \land F \in U \land P \in Z) \to Walks (G) = \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\}$
6	5	eleq2d	$⊢ (G \in W \land F \in U \land P \in Z) \to (⟨F, P⟩ \in Walks (G) \leftrightarrow ⟨F, P⟩ \in \{⟨f, p⟩ \| (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\})$
7	3 6	bitrid	$⊢ (G \in W \land F \in U \land P \in Z) \to (F Walks (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\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\})$
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	$⊢ p = P \to p (k) = P (k)$
18		fveq1	$⊢ p = P \to p (k + 1) = P (k + 1)$
19	17 18	eqeq12d	$⊢ p = P \to (p (k) = p (k + 1) \leftrightarrow P (k) = P (k + 1))$
20	19	adantl	$⊢ (f = F \land p = P) \to (p (k) = p (k + 1) \leftrightarrow P (k) = P (k + 1))$
21		fveq1	$⊢ f = F \to f (k) = F (k)$
22	21	fveq2d	$⊢ f = F \to I (f (k)) = I (F (k))$
23	17	sneqd	$⊢ p = P \to \{p (k)\} = \{P (k)\}$
24	22 23	eqeqan12d	$⊢ (f = F \land p = P) \to (I (f (k)) = \{p (k)\} \leftrightarrow I (F (k)) = \{P (k)\})$
25	17 18	preq12d	$⊢ p = P \to \{p (k), p (k + 1)\} = \{P (k), P (k + 1)\}$
26	25	adantl	$⊢ (f = F \land p = P) \to \{p (k), p (k + 1)\} = \{P (k), P (k + 1)\}$
27	22	adantr	$⊢ (f = F \land p = P) \to I (f (k)) = I (F (k))$
28	26 27	sseq12d	$⊢ (f = F \land p = P) \to (\{p (k), p (k + 1)\} \subseteq I (f (k)) \leftrightarrow \{P (k), P (k + 1)\} \subseteq I (F (k)))$
29	20 24 28	ifpbi123d	$⊢ (f = F \land p = P) \to (if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))) \leftrightarrow if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
30	16 29	raleqbidv	$⊢ (f = F \land p = P) \to (\forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))) \leftrightarrow \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
31	9 14 30	3anbi123d	$⊢ (f = F \land p = P) \to ((f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k)))) \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
32	31	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\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\} \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
33	32	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\|) if- (p (k) = p (k + 1), I (f (k)) = \{p (k)\}, \{p (k), p (k + 1)\} \subseteq I (f (k))))\} \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
34	7 33	bitrd	$⊢ (G \in W \land F \in U \land P \in Z) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$

Metamath Proof Explorer

Theorem iswlk

Proof