Metamath Proof Explorer

Theorem wlkonwlk1l

Description: A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkonwlk1l.w ⊢ φ → F Walks ⁡ G P
Assertion wlkonwlk1l ⊢ φ → F P ⁡ 0 WalksOn ⁡ G lastS ⁡ P P

Proof

Step Hyp Ref Expression
1 wlkonwlk1l.w ⊢ φ → F Walks ⁡ G P
2 eqidd ⊢ φ → P ⁡ 0 = P ⁡ 0
3 wlklenvm1 ⊢ F Walks ⁡ G P → F = P − 1
4 3 fveq2d ⊢ F Walks ⁡ G P → P ⁡ F = P ⁡ P − 1
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 5 wlkpwrd ⊢ F Walks ⁡ G P → P ∈ Word Vtx ⁡ G
7 lsw ⊢ P ∈ Word Vtx ⁡ G → lastS ⁡ P = P ⁡ P − 1
8 6 7 syl ⊢ F Walks ⁡ G P → lastS ⁡ P = P ⁡ P − 1
9 4 8 eqtr4d ⊢ F Walks ⁡ G P → P ⁡ F = lastS ⁡ P
10 1 9 syl ⊢ φ → P ⁡ F = lastS ⁡ P
11 wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0
12 nn0p1nn ⊢ F ∈ ℕ 0 → F + 1 ∈ ℕ
13 11 12 syl ⊢ F Walks ⁡ G P → F + 1 ∈ ℕ
14 wlklenvp1 ⊢ F Walks ⁡ G P → P = F + 1
15 13 6 14 jca32 ⊢ F Walks ⁡ G P → F + 1 ∈ ℕ ∧ P ∈ Word Vtx ⁡ G ∧ P = F + 1
16 fstwrdne0 ⊢ F + 1 ∈ ℕ ∧ P ∈ Word Vtx ⁡ G ∧ P = F + 1 → P ⁡ 0 ∈ Vtx ⁡ G
17 lswlgt0cl ⊢ F + 1 ∈ ℕ ∧ P ∈ Word Vtx ⁡ G ∧ P = F + 1 → lastS ⁡ P ∈ Vtx ⁡ G
18 16 17 jca ⊢ F + 1 ∈ ℕ ∧ P ∈ Word Vtx ⁡ G ∧ P = F + 1 → P ⁡ 0 ∈ Vtx ⁡ G ∧ lastS ⁡ P ∈ Vtx ⁡ G
19 15 18 syl ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ lastS ⁡ P ∈ Vtx ⁡ G
20 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
21 20 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ iEdg ⁡ G
22 wrdv ⊢ F ∈ Word dom ⁡ iEdg ⁡ G → F ∈ Word V
23 21 22 syl ⊢ F Walks ⁡ G P → F ∈ Word V
24 19 23 6 jca32 ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ lastS ⁡ P ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word Vtx ⁡ G
25 1 24 syl ⊢ φ → P ⁡ 0 ∈ Vtx ⁡ G ∧ lastS ⁡ P ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word Vtx ⁡ G
26 5 iswlkon ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ lastS ⁡ P ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word Vtx ⁡ G → F P ⁡ 0 WalksOn ⁡ G lastS ⁡ P P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 0 ∧ P ⁡ F = lastS ⁡ P
27 25 26 syl ⊢ φ → F P ⁡ 0 WalksOn ⁡ G lastS ⁡ P P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 0 ∧ P ⁡ F = lastS ⁡ P
28 1 2 10 27 mpbir3and ⊢ φ → F P ⁡ 0 WalksOn ⁡ G lastS ⁡ P P