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 ⊢φ→FWalks⁡GP
Assertion wlkonwlk1l ⊢φ→FP⁡0WalksOn⁡GlastS⁡PP

Proof

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