upgrwlkupwlk

Description: In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 2-Jan-2021)

		Ref	Expression
	Assertion	upgrwlkupwlk	$⊢ (G \in UPGraph \land F Walks (G) P) \to F UPWalks (G) P$

Proof

Step	Hyp	Ref	Expression
1		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ iEdg (G) = iEdg (G)$
4	2 3	iswlk	$⊢ (G \in V \land F \in V \land P \in V) \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
5		simpr1	$⊢ (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))) \to F \in Word dom iEdg (G)$
6		simpr2	$⊢ (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
7		df-ifp	$⊢ if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \leftrightarrow ((P (k) = P (k + 1) \land iEdg (G) (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
8		dfsn2	$⊢ \{P (k)\} = \{P (k), P (k)\}$
9		preq2	$⊢ P (k) = P (k + 1) \to \{P (k), P (k)\} = \{P (k), P (k + 1)\}$
10	8 9	syl5eq	$⊢ P (k) = P (k + 1) \to \{P (k)\} = \{P (k), P (k + 1)\}$
11	10	eqeq2d	$⊢ P (k) = P (k + 1) \to (iEdg (G) (F (k)) = \{P (k)\} \leftrightarrow iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
12	11	biimpa	$⊢ (P (k) = P (k + 1) \land iEdg (G) (F (k)) = \{P (k)\}) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\}$
13	12	a1d	$⊢ (P (k) = P (k + 1) \land iEdg (G) (F (k)) = \{P (k)\}) \to ((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
14		simpr	$⊢ ((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \to G \in UPGraph$
15		simpl	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to F \in Word dom iEdg (G)$
16		eqid	$⊢ Edg (G) = Edg (G)$
17	3 16	upgredginwlk	$⊢ (G \in UPGraph \land F \in Word dom iEdg (G)) \to (k \in (0 ..^\|F\|) \to iEdg (G) (F (k)) \in Edg (G))$
18	14 15 17	syl2anr	$⊢ ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \to (k \in (0 ..^\|F\|) \to iEdg (G) (F (k)) \in Edg (G))$
19	18	imp	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to iEdg (G) (F (k)) \in Edg (G)$
20		simprr	$⊢ ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \to G \in UPGraph$
21	20	adantr	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to G \in UPGraph$
22	21	adantr	$⊢ ((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \to G \in UPGraph$
23	22	adantr	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to G \in UPGraph$
24		simplr	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to iEdg (G) (F (k)) \in Edg (G)$
25		simprr	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))$
26		df-ne	$⊢ P (k) \neq P (k + 1) \leftrightarrow \neg P (k) = P (k + 1)$
27		fvexd	$⊢ P (k) \neq P (k + 1) \to P (k) \in V$
28		fvexd	$⊢ P (k) \neq P (k + 1) \to P (k + 1) \in V$
29		id	$⊢ P (k) \neq P (k + 1) \to P (k) \neq P (k + 1)$
30	27 28 29	3jca	$⊢ P (k) \neq P (k + 1) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
31	26 30	sylbir	$⊢ \neg P (k) = P (k + 1) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
32	31	adantr	$⊢ (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
33	32	adantl	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to (P (k) \in V \land P (k + 1) \in V \land P (k) \neq P (k + 1))$
34	2 16	upgredgpr	$⊢ ((G \in UPGraph \land iEdg (G) (F (k)) \in Edg (G) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (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)\} = iEdg (G) (F (k))$
35	23 24 25 33 34	syl31anc	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to \{P (k), P (k + 1)\} = iEdg (G) (F (k))$
36	35	eqcomd	$⊢ (((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \land iEdg (G) (F (k)) \in Edg (G)) \land (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\}$
37	36	exp31	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to (iEdg (G) (F (k)) \in Edg (G) \to ((\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
38	19 37	mpd	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to ((\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
39	38	com12	$⊢ (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to ((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
40	13 39	jaoi	$⊢ ((P (k) = P (k + 1) \land iEdg (G) (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to ((((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
41	40	com12	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to (((P (k) = P (k + 1) \land iEdg (G) (F (k)) = \{P (k)\}) \lor (\neg P (k) = P (k + 1) \land \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
42	7 41	syl5bi	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
43	42	ralimdva	$⊢ ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land ((G \in V \land F \in V \land P \in V) \land G \in UPGraph)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
44	43	ex	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
45	44	com23	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
46	45	3impia	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
47	46	impcom	$⊢ (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}$
48	5 6 47	3jca	$⊢ (((G \in V \land F \in V \land P \in V) \land G \in UPGraph) \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
49	48	exp31	$⊢ (G \in V \land F \in V \land P \in V) \to (G \in UPGraph \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})))$
50	49	com23	$⊢ (G \in V \land F \in V \land P \in V) \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to (G \in UPGraph \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})))$
51	4 50	sylbid	$⊢ (G \in V \land F \in V \land P \in V) \to (F Walks (G) P \to (G \in UPGraph \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})))$
52	51	impd	$⊢ (G \in V \land F \in V \land P \in V) \to ((F Walks (G) P \land G \in UPGraph) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
53	52	impcom	$⊢ ((F Walks (G) P \land G \in UPGraph) \land (G \in V \land F \in V \land P \in V)) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
54	2 3	isupwlk	$⊢ (G \in V \land F \in V \land P \in V) \to (F UPWalks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
55	54	adantl	$⊢ ((F Walks (G) P \land G \in UPGraph) \land (G \in V \land F \in V \land P \in V)) \to (F UPWalks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
56	53 55	mpbird	$⊢ ((F Walks (G) P \land G \in UPGraph) \land (G \in V \land F \in V \land P \in V)) \to F UPWalks (G) P$
57	56	exp31	$⊢ F Walks (G) P \to (G \in UPGraph \to ((G \in V \land F \in V \land P \in V) \to F UPWalks (G) P))$
58	1 57	mpid	$⊢ F Walks (G) P \to (G \in UPGraph \to F UPWalks (G) P)$
59	58	impcom	$⊢ (G \in UPGraph \land F Walks (G) P) \to F UPWalks (G) P$

Metamath Proof Explorer

Theorem upgrwlkupwlk

Proof