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	18	raleqdv	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
20	15 19	mpbid	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
21	1 20	sylan2b	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
22	4 13 21	3jca	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
23	22	adantr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
24		simpl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → 𝑁 ∈ ℕ₀ )
25		oveq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 → ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ( 0 ... 𝑁 ) )
26	25	adantl	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ( 0 ... 𝑁 ) )
27	26	feq2d	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
28	27	biimpd	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
29	28	impancom	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
30	29	adantld	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
31	30	imp	⊢ ( ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) )
32		ffz0hash	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
33	24 31 32	syl2an2	⊢ ( ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
34	33	ex	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
35	9 34	syl	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
36	35	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) )
37	36	imp	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) )
38	24	adantl	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → 𝑁 ∈ ℕ₀ )
39		iswwlksn	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
40	5 14	iswwlks	⊢ ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
41	40	a1i	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
42	41	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 ) ) ) )
43	39 42	bitrd	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( ( 2^nd ‘ 𝑊 ) ≠ ∅ ∧ ( 2^nd ‘ 𝑊 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) − 1 ) ) { ( ( 2^nd ‘ 𝑊 ) ‘ 𝑖 ) , ( ( 2^nd ‘ 𝑊 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑊 ) ) = ( 𝑁 + 1 ) ) ) )
44	38 43	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 ) ) ) )
45	23 37 44	mpbir2and	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) = 𝑁 ) ) → ( 2^nd ‘ 𝑊 ) ∈ ( 𝑁 WWalksN 𝐺 ) )

Metamath Proof Explorer

Theorem wlknewwlksn

Proof