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 ⊢ V = Vtx ⁡ G
iswwlksnx.e ⊢ E = Edg ⁡ G
Assertion iswwlksnx ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1

Proof

Step Hyp Ref Expression
1 iswwlksnx.v ⊢ V = Vtx ⁡ G
2 iswwlksnx.e ⊢ E = Edg ⁡ G
3 iswwlksn ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
4 1 2 iswwlks ⊢ W ∈ WWalks ⁡ G ↔ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
5 df-3an ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
6 nn0p1gt0 ⊢ N ∈ ℕ 0 → 0 < N + 1
7 6 gt0ne0d ⊢ N ∈ ℕ 0 → N + 1 ≠ 0
8 7 adantr ⊢ N ∈ ℕ 0 ∧ W = N + 1 → N + 1 ≠ 0
9 neeq1 ⊢ W = N + 1 → W ≠ 0 ↔ N + 1 ≠ 0
10 9 adantl ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ≠ 0 ↔ N + 1 ≠ 0
11 8 10 mpbird ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ≠ 0
12 hasheq0 ⊢ W ∈ Word V → W = 0 ↔ W = ∅
13 12 necon3bid ⊢ W ∈ Word V → W ≠ 0 ↔ W ≠ ∅
14 11 13 syl5ibcom ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ∈ Word V → W ≠ ∅
15 14 pm4.71rd ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ∈ Word V ↔ W ≠ ∅ ∧ W ∈ Word V
16 15 bicomd ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ≠ ∅ ∧ W ∈ Word V ↔ W ∈ Word V
17 16 anbi1d ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
18 5 17 bitrid ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
19 4 18 bitrid ⊢ N ∈ ℕ 0 ∧ W = N + 1 → W ∈ WWalks ⁡ G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
20 19 ex ⊢ N ∈ ℕ 0 → W = N + 1 → W ∈ WWalks ⁡ G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
21 20 pm5.32rd ⊢ N ∈ ℕ 0 → W ∈ WWalks ⁡ G ∧ W = N + 1 ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1
22 df-3an ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1 ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1
23 21 22 bitr4di ⊢ N ∈ ℕ 0 → W ∈ WWalks ⁡ G ∧ W = N + 1 ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1
24 3 23 bitrd ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W = N + 1