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	18	raleqdv	$⊢ (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) \leftrightarrow \forall i \in (0 ..^\|2^{nd} (W)\| - 1) \{2^{nd} (W) (i), 2^{nd} (W) (i + 1)\} \in Edg (G))$
20	15 19	mpbid	$⊢ (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)$
21	1 20	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)$
22	4 13 21	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))$
23	22	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))$
24		simpl	$⊢ (N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to N \in ℕ_{0}$
25		oveq2	$⊢ \|1^{st} (W)\| = N \to (0 \dots \|1^{st} (W)\|) = (0 \dots N)$
26	25	adantl	$⊢ (1^{st} (W) \in Word dom iEdg (G) \land \|1^{st} (W)\| = N) \to (0 \dots \|1^{st} (W)\|) = (0 \dots N)$
27	26	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))$
28	27	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))$
29	28	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))$
30	29	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))$
31	30	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)$
32		ffz0hash	$⊢ (N \in ℕ_{0} \land 2^{nd} (W) : (0 \dots N) ⟶ Vtx (G)) \to \|2^{nd} (W)\| = N + 1$
33	24 31 32	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$
34	33	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)$
35	9 34	syl	$⊢ W \in Walks (G) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to \|2^{nd} (W)\| = N + 1)$
36	35	adantl	$⊢ (G \in UPGraph \land W \in Walks (G)) \to ((N \in ℕ_{0} \land \|1^{st} (W)\| = N) \to \|2^{nd} (W)\| = N + 1)$
37	36	imp	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to \|2^{nd} (W)\| = N + 1$
38	24	adantl	$⊢ ((G \in UPGraph \land W \in Walks (G)) \land (N \in ℕ_{0} \land \|1^{st} (W)\| = N)) \to N \in ℕ_{0}$
39		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))$
40	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))$
41	40	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)))$
42	41	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))$
43	39 42	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))$
44	38 43	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))$
45	23 37 44	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