upgriswlk

Description: Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021) (Revised by AV, 28-Oct-2021)

	Ref	Expression
Hypotheses	upgriswlk.v	$⊢ V = Vtx (G)$
	upgriswlk.i	$⊢ I = iEdg (G)$
Assertion	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)\}))$

Proof

Step	Hyp	Ref	Expression
1		upgriswlk.v	$⊢ V = Vtx (G)$
2		upgriswlk.i	$⊢ I = iEdg (G)$
3	1 2	iswlkg	$⊢ 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\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
4		df-ifp	$⊢ if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow ((P (k) = P (k + 1) \land I (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))))$
5		dfsn2	$⊢ \{P (k)\} = \{P (k), P (k)\}$
6		preq2	$⊢ P (k) = P (k + 1) \to \{P (k), P (k)\} = \{P (k), P (k + 1)\}$
7	5 6	eqtrid	$⊢ P (k) = P (k + 1) \to \{P (k)\} = \{P (k), P (k + 1)\}$
8	7	eqeq2d	$⊢ P (k) = P (k + 1) \to (I (F (k)) = \{P (k)\} \leftrightarrow I (F (k)) = \{P (k), P (k + 1)\})$
9	8	biimpa	$⊢ (P (k) = P (k + 1) \land I (F (k)) = \{P (k)\}) \to I (F (k)) = \{P (k), P (k + 1)\}$
10	9	a1d	$⊢ (P (k) = P (k + 1) \land I (F (k)) = \{P (k)\}) \to (((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to I (F (k)) = \{P (k), P (k + 1)\})$
11		eqid	$⊢ Edg (G) = Edg (G)$
12	2 11	upgredginwlk	$⊢ (G \in UPGraph \land F \in Word dom I) \to (k \in (0 ..^\|F\|) \to I (F (k)) \in Edg (G))$
13	12	adantrr	$⊢ (G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \to (k \in (0 ..^\|F\|) \to I (F (k)) \in Edg (G))$
14	13	imp	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to I (F (k)) \in Edg (G)$
15		simp-4l	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to G \in UPGraph$
16		simpr	$⊢ (((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \to I (F (k)) \in Edg (G)$
17	16	adantr	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to I (F (k)) \in Edg (G)$
18		simpr	$⊢ (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \to \{P (k), P (k + 1)\} \subseteq I (F (k))$
19	18	adantl	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to \{P (k), P (k + 1)\} \subseteq I (F (k))$
20		fvexd	$⊢ \neg P (k) = P (k + 1) \to P (k) \in V$
21		fvexd	$⊢ \neg P (k) = P (k + 1) \to P (k + 1) \in V$
22		neqne	$⊢ \neg P (k) = P (k + 1) \to P (k) \neq P (k + 1)$
23	20 21 22	3jca	$⊢ \neg P (k) = P (k + 1) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
24	23	adantr	$⊢ (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
25	24	adantl	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
26	1 11	upgredgpr	$⊢ ((G \in UPGraph \land I (F (k)) \in Edg (G) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \land (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))) \to \{P (k), P (k + 1)\} = I (F (k))$
27	15 17 19 25 26	syl31anc	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to \{P (k), P (k + 1)\} = I (F (k))$
28	27	eqcomd	$⊢ ((((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \land I (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to I (F (k)) = \{P (k), P (k + 1)\}$
29	28	exp31	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to (I (F (k)) \in Edg (G) \to ((\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \to I (F (k)) = \{P (k), P (k + 1)\}))$
30	14 29	mpd	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to ((\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \to I (F (k)) = \{P (k), P (k + 1)\})$
31	30	com12	$⊢ (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k))) \to (((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to I (F (k)) = \{P (k), P (k + 1)\})$
32	10 31	jaoi	$⊢ ((P (k) = P (k + 1) \land I (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to (((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to I (F (k)) = \{P (k), P (k + 1)\})$
33	32	com12	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to (((P (k) = P (k + 1) \land I (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to I (F (k)) = \{P (k), P (k + 1)\})$
34	4 33	syl5bi	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to I (F (k)) = \{P (k), P (k + 1)\})$
35		ifpprsnss	$⊢ I (F (k)) = \{P (k), P (k + 1)\} \to if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
36	34 35	impbid1	$⊢ ((G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow I (F (k)) = \{P (k), P (k + 1)\})$
37	36	ralbidva	$⊢ (G \in UPGraph \land (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)) \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\|) I (F (k)) = \{P (k), P (k + 1)\})$
38	37	pm5.32da	$⊢ G \in UPGraph \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\|) I (F (k)) = \{P (k), P (k + 1)\}))$
39		df-3an	$⊢ (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))))$
40		df-3an	$⊢ (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)\})$
41	38 39 40	3bitr4g	$⊢ G \in UPGraph \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\|) I (F (k)) = \{P (k), P (k + 1)\}))$
42	3 41	bitrd	$⊢ 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)\}))$

Metamath Proof Explorer

Theorem upgriswlk

Proof