Metamath Proof Explorer

Theorem upwlkwlk

Description: A simple walk is a walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 27-Feb-2021)

		Ref	Expression
	Assertion	upwlkwlk	$⊢ F UPWalks (G) P \to F Walks (G) P$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	1 2	upwlkbprop	$⊢ F UPWalks (G) P \to (G \in V \land F \in V \land P \in V)$
4		idd	$⊢ (G \in V \land F \in V \land P \in V) \to (F \in Word dom iEdg (G) \to F \in Word dom iEdg (G))$
5		idd	$⊢ (G \in V \land F \in V \land P \in V) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to P : (0 \dots \|F\|) ⟶ Vtx (G))$
6		ifpprsnss	$⊢ iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))$
7	6	a1i	$⊢ ((G \in V \land F \in V \land P \in V) \land k \in (0 ..^\|F\|)) \to (iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
8	7	ralimdva	$⊢ (G \in V \land F \in V \land P \in V) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \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))))$
9	4 5 8	3anim123d	$⊢ (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)\}) \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)))))$
10	1 2	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)\}))$
11	1 2	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)))))$
12	9 10 11	3imtr4d	$⊢ (G \in V \land F \in V \land P \in V) \to (F UPWalks (G) P \to F Walks (G) P)$
13	3 12	mpcom	$⊢ F UPWalks (G) P \to F Walks (G) P$