redwlk

Description: A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

		Ref	Expression
	Assertion	redwlk	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \to ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)})$

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		wrdred1	$⊢ F \in Word dom iEdg (G) \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G)$
6	5	a1i	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \to (F \in Word dom iEdg (G) \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G))$
7	3	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
8		redwlklem	$⊢ (F \in Word dom iEdg (G) \land 1 \leq \|F\| \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G)$
9	8	3exp	$⊢ F \in Word dom iEdg (G) \to (1 \leq \|F\| \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G)))$
10	7 9	syl	$⊢ F Walks (G) P \to (1 \leq \|F\| \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G)))$
11	10	imp	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G))$
12		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
13		wrdred1hash	$⊢ (F \in Word dom iEdg (G) \land 1 \leq \|F\|) \to \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1$
14	7 13	sylan	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \to \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1$
15		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
16		fzossrbm1	$⊢ \|F\| \in ℤ \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
17	15 16	syl	$⊢ \|F\| \in ℕ_{0} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
18		ssralv	$⊢ (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|) \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\| - 1) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
19	17 18	syl	$⊢ \|F\| \in ℕ_{0} \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\| - 1) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
20	17	sselda	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to k \in (0 ..^\|F\|)$
21	20	fvresd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to ({P ↾}_{(0 ..^\|F\|)}) (k) = P (k)$
22	21	eqcomd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to P (k) = ({P ↾}_{(0 ..^\|F\|)}) (k)$
23		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
24		simpr	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to k \in (0 ..^\|F\| - 1)$
25	15	adantr	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to \|F\| \in ℤ$
26		1zzd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to 1 \in ℤ$
27		fzoaddel2	$⊢ (k \in (0 ..^\|F\| - 1) \land \|F\| \in ℤ \land 1 \in ℤ) \to k + 1 \in (1 ..^\|F\|)$
28	24 25 26 27	syl3anc	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to k + 1 \in (1 ..^\|F\|)$
29	23 28	sselid	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to k + 1 \in (0 ..^\|F\|)$
30	29	fvresd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to ({P ↾}_{(0 ..^\|F\|)}) (k + 1) = P (k + 1)$
31	30	eqcomd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to P (k + 1) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1)$
32	22 31	eqeq12d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to (P (k) = P (k + 1) \leftrightarrow ({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1))$
33		fvres	$⊢ k \in (0 ..^\|F\| - 1) \to ({F ↾}_{(0 ..^\|F\| - 1)}) (k) = F (k)$
34	33	adantl	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to ({F ↾}_{(0 ..^\|F\| - 1)}) (k) = F (k)$
35	34	eqcomd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to F (k) = ({F ↾}_{(0 ..^\|F\| - 1)}) (k)$
36	35	fveq2d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to iEdg (G) (F (k)) = iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))$
37	22	sneqd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to \{P (k)\} = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}$
38	36 37	eqeq12d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to (iEdg (G) (F (k)) = \{P (k)\} \leftrightarrow iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\})$
39	22 31	preq12d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to \{P (k), P (k + 1)\} = \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\}$
40	39 36	sseq12d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to (\{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)) \leftrightarrow \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)))$
41	32 38 40	ifpbi123d	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to (if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \leftrightarrow if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
42	41	biimpd	$⊢ (\|F\| \in ℕ_{0} \land k \in (0 ..^\|F\| - 1)) \to (if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
43	42	ralimdva	$⊢ \|F\| \in ℕ_{0} \to (\forall k \in (0 ..^\|F\| - 1) 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\| - 1) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
44	19 43	syld	$⊢ \|F\| \in ℕ_{0} \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\| - 1) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
45	44	adantr	$⊢ (\|F\| \in ℕ_{0} \land \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 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))) \to \forall k \in (0 ..^\|F\| - 1) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
46		oveq2	$⊢ \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1 \to (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) = (0 ..^\|F\| - 1)$
47	46	eqcomd	$⊢ \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1 \to (0 ..^\|F\| - 1) = (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|)$
48	47	raleqdv	$⊢ \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1 \to (\forall k \in (0 ..^\|F\| - 1) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))) \leftrightarrow \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
49	48	adantl	$⊢ (\|F\| \in ℕ_{0} \land \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 1) \to (\forall k \in (0 ..^\|F\| - 1) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))) \leftrightarrow \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
50	45 49	sylibd	$⊢ (\|F\| \in ℕ_{0} \land \|{F ↾}_{(0 ..^\|F\| - 1)}\| = \|F\| - 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))) \to \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
51	12 14 50	syl2an2r	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \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 ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
52	6 11 51	3anim123d	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \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 ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G) \land ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)))))$
53	52	imp	$⊢ ((F Walks (G) P \land 1 \leq \|F\|) \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 ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G) \land ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k))))$
54		id	$⊢ G \in V \to G \in V$
55		resexg	$⊢ F \in V \to {F ↾}_{(0 ..^\|F\| - 1)} \in V$
56		resexg	$⊢ P \in V \to {P ↾}_{(0 ..^\|F\|)} \in V$
57	2 3	iswlk	$⊢ (G \in V \land {F ↾}_{(0 ..^\|F\| - 1)} \in V \land {P ↾}_{(0 ..^\|F\|)} \in V) \to (({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)}) \leftrightarrow ({F ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G) \land ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)))))$
58	57	bicomd	$⊢ (G \in V \land {F ↾}_{(0 ..^\|F\| - 1)} \in V \land {P ↾}_{(0 ..^\|F\|)} \in V) \to (({F ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G) \land ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)))) \leftrightarrow ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)}))$
59	54 55 56 58	syl3an	$⊢ (G \in V \land F \in V \land P \in V) \to (({F ↾}_{(0 ..^\|F\| - 1)} \in Word dom iEdg (G) \land ({P ↾}_{(0 ..^\|F\|)}) : (0 \dots \|{F ↾}_{(0 ..^\|F\| - 1)}\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|{F ↾}_{(0 ..^\|F\| - 1)}\|) if- (({P ↾}_{(0 ..^\|F\|)}) (k) = ({P ↾}_{(0 ..^\|F\|)}) (k + 1), iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)) = \{({P ↾}_{(0 ..^\|F\|)}) (k)\}, \{({P ↾}_{(0 ..^\|F\|)}) (k), ({P ↾}_{(0 ..^\|F\|)}) (k + 1)\} \subseteq iEdg (G) (({F ↾}_{(0 ..^\|F\| - 1)}) (k)))) \leftrightarrow ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)}))$
60	53 59	imbitrid	$⊢ (G \in V \land F \in V \land P \in V) \to (((F Walks (G) P \land 1 \leq \|F\|) \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 ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)}))$
61	60	expcomd	$⊢ (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 ((F Walks (G) P \land 1 \leq \|F\|) \to ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)})))$
62	4 61	sylbid	$⊢ (G \in V \land F \in V \land P \in V) \to (F Walks (G) P \to ((F Walks (G) P \land 1 \leq \|F\|) \to ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)})))$
63	1 62	mpcom	$⊢ F Walks (G) P \to ((F Walks (G) P \land 1 \leq \|F\|) \to ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)}))$
64	63	anabsi5	$⊢ (F Walks (G) P \land 1 \leq \|F\|) \to ({F ↾}_{(0 ..^\|F\| - 1)}) Walks (G) ({P ↾}_{(0 ..^\|F\|)})$

Metamath Proof Explorer

Theorem redwlk

Proof