Metamath Proof Explorer

Theorem wwlknp

Description: Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Hypotheses wwlkbp.v ⊢V=Vtx⁡G
wwlknp.e ⊢E=Edg⁡G
Assertion wwlknp ⊢W∈NWWalksNG→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E

Proof

Step Hyp Ref Expression
1 wwlkbp.v ⊢V=Vtx⁡G
2 wwlknp.e ⊢E=Edg⁡G
3 1 wwlknbp ⊢W∈NWWalksNG→G∈V∧N∈ℕ0∧W∈WordV
4 iswwlksn ⊢N∈ℕ0→W∈NWWalksNG↔W∈WWalks⁡G∧W=N+1
5 1 2 iswwlks ⊢W∈WWalks⁡G↔W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E
6 simpl2 ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1∧N∈ℕ0→W∈WordV
7 simprl ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1∧N∈ℕ0→W=N+1
8 oveq1 ⊢W=N+1→W−1=N+1-1
9 nn0cn ⊢N∈ℕ0→N∈ℂ
10 pncan1 ⊢N∈ℂ→N+1-1=N
11 9 10 syl ⊢N∈ℕ0→N+1-1=N
12 8 11 sylan9eq ⊢W=N+1∧N∈ℕ0→W−1=N
13 12 oveq2d ⊢W=N+1∧N∈ℕ0→0..^W−1=0..^N
14 13 raleqdv ⊢W=N+1∧N∈ℕ0→∀i∈0..^W−1W⁡iW⁡i+1∈E↔∀i∈0..^NW⁡iW⁡i+1∈E
15 14 biimpcd ⊢∀i∈0..^W−1W⁡iW⁡i+1∈E→W=N+1∧N∈ℕ0→∀i∈0..^NW⁡iW⁡i+1∈E
16 15 3ad2ant3 ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E→W=N+1∧N∈ℕ0→∀i∈0..^NW⁡iW⁡i+1∈E
17 16 imp ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1∧N∈ℕ0→∀i∈0..^NW⁡iW⁡i+1∈E
18 6 7 17 3jca ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W=N+1∧N∈ℕ0→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
19 18 ex ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E→W=N+1∧N∈ℕ0→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
20 5 19 sylbi ⊢W∈WWalks⁡G→W=N+1∧N∈ℕ0→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
21 20 expdimp ⊢W∈WWalks⁡G∧W=N+1→N∈ℕ0→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
22 21 com12 ⊢N∈ℕ0→W∈WWalks⁡G∧W=N+1→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
23 4 22 sylbid ⊢N∈ℕ0→W∈NWWalksNG→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
24 23 3ad2ant2 ⊢G∈V∧N∈ℕ0∧W∈WordV→W∈NWWalksNG→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E
25 3 24 mpcom ⊢W∈NWWalksNG→W∈WordV∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈E