Metamath Proof Explorer

Theorem iswwlksnx

Description: Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021)

Ref Expression
Hypotheses iswwlksnx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
iswwlksnx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion iswwlksnx ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iswwlksnx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 iswwlksnx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )
4 1 2 iswwlks ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
5 df-3an ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
6 nn0p1gt0 ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
7 6 gt0ne0d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≠ 0 )
8 7 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ≠ 0 )
9 neeq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ ( 𝑁 + 1 ) ≠ 0 ) )
10 9 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ ( 𝑁 + 1 ) ≠ 0 ) )
11 8 10 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ 𝑊 ) ≠ 0 )
12 hasheq0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
13 12 necon3bid ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ 𝑊 ≠ ∅ ) )
14 11 13 syl5ibcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ∈ Word 𝑉 → 𝑊 ≠ ∅ ) )
15 14 pm4.71rd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ∈ Word 𝑉 ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) ) )
16 15 bicomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) ↔ 𝑊 ∈ Word 𝑉 ) )
17 16 anbi1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
18 5 17 syl5bb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
19 4 18 syl5bb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
20 19 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
21 20 pm5.32rd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )
22 df-3an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
23 21 22 bitr4di ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )
24 3 23 bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )