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	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) )
2		wlkn0	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( 2^nd ‘ 𝑊 ) ≠ ∅ )
3	1 2	sylbi	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( 2^nd ‘ 𝑊 ) ≠ ∅ )
4	3	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( 2^nd ‘ 𝑊 ) ≠ ∅ )
5		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7		eqid	⊢ ( 1^st ‘ 𝑊 ) = ( 1^st ‘ 𝑊 )
8		eqid	⊢ ( 2^nd ‘ 𝑊 ) = ( 2^nd ‘ 𝑊 )
9	5 6 7 8	wlkelwrd	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
10		ffz0iswrd	⊢ ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) )
11	10	adantl	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) )
12	9 11	syl	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) )
13	12	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) )
14		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
15	14	upgrwlkvtxedg	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
16		wlklenvm1	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) )
17	16	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) )
18	17	oveq2d	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) )
19	15 18	raleqtrdv	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
20	1 19	sylan2b	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
21	4 13 20	3jca	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
22	21	adantr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
23		simpl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → 𝑁 ∈ ℕ₀ )
24		oveq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 → ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ( 0 ... 𝑁 ) )
25	24	adantl	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ( 0 ... 𝑁 ) )
26	25	feq2d	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
27	26	biimpd	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
28	27	impancom	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
29	28	adantld	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
30	29	imp	⊢ ( ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) )
31		ffz0hash	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
32	23 30 31	syl2an2	⊢ ( ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
33	32	ex	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
34	9 33	syl	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
35	34	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
36	35	imp	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
37	23	adantl	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → 𝑁 ∈ ℕ₀ )
38		iswwlksn	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
39	5 14	iswwlks	⊢ ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
40	39	a1i	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
41	40	anbi1d	⊢ ( 𝑁 ∈ ℕ₀ → ( ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ↔ ( ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
42	38 41	bitrd	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
43	37 42	syl	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
44	22 36 43	mpbir2and	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) )

Metamath Proof Explorer

Theorem wlknewwlksn

Proof