# Metamath Proof Explorer

## Theorem 3wlkond

Description: A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
3wlkd.n ${⊢}{\phi }\to \left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge \left({B}\ne {C}\wedge {B}\ne {D}\right)\wedge {C}\ne {D}\right)$
3wlkd.e ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\subseteq {I}\left({J}\right)\wedge \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)\wedge \left\{{C},{D}\right\}\subseteq {I}\left({L}\right)\right)$
3wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
3wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion 3wlkond ${⊢}{\phi }\to {F}\left({A}\mathrm{WalksOn}\left({G}\right){D}\right){P}$

### Proof

Step Hyp Ref Expression
1 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
2 3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3 3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
4 3wlkd.n ${⊢}{\phi }\to \left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge \left({B}\ne {C}\wedge {B}\ne {D}\right)\wedge {C}\ne {D}\right)$
5 3wlkd.e ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\subseteq {I}\left({J}\right)\wedge \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)\wedge \left\{{C},{D}\right\}\subseteq {I}\left({L}\right)\right)$
6 3wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
7 3wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
8 1 2 3 4 5 6 7 3wlkd ${⊢}{\phi }\to {F}\mathrm{Walks}\left({G}\right){P}$
9 8 wlkonwlk1l ${⊢}{\phi }\to {F}\left({P}\left(0\right)\mathrm{WalksOn}\left({G}\right)\mathrm{lastS}\left({P}\right)\right){P}$
10 1 2 3 3wlkdlem3 ${⊢}{\phi }\to \left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)$
11 simpll ${⊢}\left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)\to {P}\left(0\right)={A}$
12 11 eqcomd ${⊢}\left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)\to {A}={P}\left(0\right)$
13 10 12 syl ${⊢}{\phi }\to {A}={P}\left(0\right)$
14 1 fveq2i ${⊢}\mathrm{lastS}\left({P}\right)=\mathrm{lastS}\left(⟨“{A}{B}{C}{D}”⟩\right)$
15 fvex ${⊢}{P}\left(3\right)\in \mathrm{V}$
16 eleq1 ${⊢}{P}\left(3\right)={D}\to \left({P}\left(3\right)\in \mathrm{V}↔{D}\in \mathrm{V}\right)$
17 15 16 mpbii ${⊢}{P}\left(3\right)={D}\to {D}\in \mathrm{V}$
18 lsws4 ${⊢}{D}\in \mathrm{V}\to \mathrm{lastS}\left(⟨“{A}{B}{C}{D}”⟩\right)={D}$
19 17 18 syl ${⊢}{P}\left(3\right)={D}\to \mathrm{lastS}\left(⟨“{A}{B}{C}{D}”⟩\right)={D}$
20 14 19 syl5req ${⊢}{P}\left(3\right)={D}\to {D}=\mathrm{lastS}\left({P}\right)$
21 20 ad2antll ${⊢}\left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)\to {D}=\mathrm{lastS}\left({P}\right)$
22 10 21 syl ${⊢}{\phi }\to {D}=\mathrm{lastS}\left({P}\right)$
23 13 22 oveq12d ${⊢}{\phi }\to {A}\mathrm{WalksOn}\left({G}\right){D}={P}\left(0\right)\mathrm{WalksOn}\left({G}\right)\mathrm{lastS}\left({P}\right)$
24 23 breqd ${⊢}{\phi }\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){D}\right){P}↔{F}\left({P}\left(0\right)\mathrm{WalksOn}\left({G}\right)\mathrm{lastS}\left({P}\right)\right){P}\right)$
25 9 24 mpbird ${⊢}{\phi }\to {F}\left({A}\mathrm{WalksOn}\left({G}\right){D}\right){P}$