wlknewwlksn

Description: If a walk in a pseudograph has length N , then the sequence of the vertices of the walk is a word representing the walk as word of length N . (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 11-Apr-2021)

		Ref	Expression
	Assertion	wlknewwlksn	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to 2^{nd} (W) \in (N WWalksN G)$

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	$⊢ W \in Walks (G) \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
2		wlkn0	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to 2^{nd} (W) \neq \emptyset$
3	1 2	sylbi	$⊢ W \in Walks (G) \to 2^{nd} (W) \neq \emptyset$
4	3	adantl	$⊢ (G \in UPGraph \land W \in Walks (G)) \to 2^{nd} (W) \neq \emptyset$
5		eqid	$⊢ Vtx (G) = Vtx (G)$
6		eqid	$⊢ iEdg (G) = iEdg (G)$
7		eqid	$⊢ 1^{st} (W) = 1^{st} (W)$
8		eqid	$⊢ 2^{nd} (W) = 2^{nd} (W)$
9	5 6 7 8	wlkelwrd	$⊢ W \in Walks (G) \to (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G))$
10		ffz0iswrd	$⊢ 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \to 2^{nd} (W) \in Word Vtx (G)$
11	10	adantl	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \to 2^{nd} (W) \in Word Vtx (G)$
12	9 11	syl	$⊢ W \in Walks (G) \to 2^{nd} (W) \in Word Vtx (G)$
13	12	adantl	$⊢ (G \in UPGraph \land W \in Walks (G)) \to 2^{nd} (W) \in Word Vtx (G)$
14		eqid	$⊢ Edg (G) = Edg (G)$
15	14	upgrwlkvtxedg	$⊢ (G \in UPGraph \land 1^{st} (W) Walks (G) 2^{nd} (W)) \to \forall i \in (0 ..^\|1^{st} (W)\|) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)$
16		wlklenvm1	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to \|1^{st} (W)\| = \|2^{nd} (W)\| - 1$
17	16	adantl	$⊢ (G \in UPGraph \land 1^{st} (W) Walks (G) 2^{nd} (W)) \to \|1^{st} (W)\| = \|2^{nd} (W)\| - 1$
18	17	oveq2d	$⊢ (G \in UPGraph \land 1^{st} (W) Walks (G) 2^{nd} (W)) \to (0 ..^\|1^{st} (W)\|) = (0 ..^\|2^{nd} (W)\| - 1)$
19	15 18	raleqtrdv	$⊢ (G \in UPGraph \land 1^{st} (W) Walks (G) 2^{nd} (W)) \to \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)$
20	1 19	sylan2b	$⊢ (G \in UPGraph \land W \in Walks (G)) \to \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)$
21	4 13 20	3jca	$⊢ (G \in UPGraph \land W \in Walks (G)) \to (2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G))$
22	21	adantr	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to (2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G))$
23		simpl	$⊢ (N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to N \in ℕ_{0}$
24		oveq2	$⊢ \|1^{st} (W)\| = N \to (0 \dots \|1^{st} (W)\|) = (0 \dots N)$
25	24	adantl	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land \|1^{st} (W)\| = N) \to (0 \dots \|1^{st} (W)\|) = (0 \dots N)$
26	25	feq2d	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land \|1^{st} (W)\| = N) \to (2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \leftrightarrow 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G))$
27	26	biimpd	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land \|1^{st} (W)\| = N) \to (2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \to 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G))$
28	27	impancom	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \to (\|1^{st} (W)\| = N \to 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G))$
29	28	adantld	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G))$
30	29	imp	$⊢ ((1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G)$
31		ffz0hash	$⊢ (N \in ℕ_{0} \land 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G)) \to \|2^{nd} (W)\| = N + 1$
32	23 30 31	syl2an2	$⊢ ((1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to \|2^{nd} (W)\| = N + 1$
33	32	ex	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to \|2^{nd} (W)\| = N + 1)$
34	9 33	syl	$⊢ W \in Walks (G) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to \|2^{nd} (W)\| = N + 1)$
35	34	adantl	$⊢ (G \in UPGraph \land W \in Walks (G)) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to \|2^{nd} (W)\| = N + 1)$
36	35	imp	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to \|2^{nd} (W)\| = N + 1$
37	23	adantl	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to N \in ℕ_{0}$
38		iswwlksn	$⊢ N \in ℕ_{0} \to (2^{nd} (W) \in (N WWalksN G) \leftrightarrow (2^{nd} (W) \in WWalks (G) \land \|2^{nd} (W)\| = N + 1))$
39	5 14	iswwlks	$⊢ 2^{nd} (W) \in WWalks (G) \leftrightarrow (2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G))$
40	39	a1i	$⊢ N \in ℕ_{0} \to (2^{nd} (W) \in WWalks (G) \leftrightarrow (2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)))$
41	40	anbi1d	$⊢ N \in ℕ_{0} \to ((2^{nd} (W) \in WWalks (G) \land \|2^{nd} (W)\| = N + 1) \leftrightarrow ((2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)) \land \|2^{nd} (W)\| = N + 1))$
42	38 41	bitrd	$⊢ N \in ℕ_{0} \to (2^{nd} (W) \in (N WWalksN G) \leftrightarrow ((2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)) \land \|2^{nd} (W)\| = N + 1))$
43	37 42	syl	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to (2^{nd} (W) \in (N WWalksN G) \leftrightarrow ((2^{nd} (W) \neq \emptyset \land 2^{nd} (W) \in Word Vtx (G) \land \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G)) \land \|2^{nd} (W)\| = N + 1))$
44	22 36 43	mpbir2and	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to 2^{nd} (W) \in (N WWalksN G)$

Metamath Proof Explorer

Theorem wlknewwlksn

Proof