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∈NWWalksNG↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡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∈NWWalksNG↔W∈WWalks⁡G∧W=N+1
4 1 2 iswwlks ⊢W∈WWalks⁡G↔W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
5 df-3an ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E↔W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡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∈WordV→W=0↔W=∅
13 12 necon3bid ⊢W∈WordV→W≠0↔W≠∅
14 11 13 syl5ibcom ⊢N∈ℕ0∧W=N+1→W∈WordV→W≠∅
15 14 pm4.71rd ⊢N∈ℕ0∧W=N+1→W∈WordV↔W≠∅∧W∈WordV
16 15 bicomd ⊢N∈ℕ0∧W=N+1→W≠∅∧W∈WordV↔W∈WordV
17 16 anbi1d ⊢N∈ℕ0∧W=N+1→W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
18 5 17 bitrid ⊢N∈ℕ0∧W=N+1→W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
19 4 18 bitrid ⊢N∈ℕ0∧W=N+1→W∈WWalks⁡G↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
20 19 ex ⊢N∈ℕ0→W=N+1→W∈WWalks⁡G↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
21 20 pm5.32rd ⊢N∈ℕ0→W∈WWalks⁡G∧W=N+1↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1
22 df-3an ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1
23 21 22 bitr4di ⊢N∈ℕ0→W∈WWalks⁡G∧W=N+1↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1
24 3 23 bitrd ⊢N∈ℕ0→W∈NWWalksNG↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1