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 = ⟨“ ABCD ”⟩
3wlkd.f F = ⟨“ JKL ”⟩
3wlkd.s φ A V B V C V D V
3wlkd.n φ A B A C B C B D C D
3wlkd.e φ A B I J B C I K C D I L
3wlkd.v V = Vtx G
3wlkd.i I = iEdg G
Assertion 3wlkond φ F A WalksOn G D P

Proof

Step Hyp Ref Expression
1 3wlkd.p P = ⟨“ ABCD ”⟩
2 3wlkd.f F = ⟨“ JKL ”⟩
3 3wlkd.s φ A V B V C V D V
4 3wlkd.n φ A B A C B C B D C D
5 3wlkd.e φ A B I J B C I K C D I L
6 3wlkd.v V = Vtx G
7 3wlkd.i I = iEdg G
8 1 2 3 4 5 6 7 3wlkd φ F Walks G P
9 8 wlkonwlk1l φ F P 0 WalksOn G lastS P P
10 1 2 3 3wlkdlem3 φ P 0 = A P 1 = B P 2 = C P 3 = D
11 simpll P 0 = A P 1 = B P 2 = C P 3 = D P 0 = A
12 11 eqcomd P 0 = A P 1 = B P 2 = C P 3 = D A = P 0
13 10 12 syl φ A = P 0
14 1 fveq2i lastS P = lastS ⟨“ ABCD ”⟩
15 fvex P 3 V
16 eleq1 P 3 = D P 3 V D V
17 15 16 mpbii P 3 = D D V
18 lsws4 D V lastS ⟨“ ABCD ”⟩ = D
19 17 18 syl P 3 = D lastS ⟨“ ABCD ”⟩ = D
20 14 19 eqtr2id P 3 = D D = lastS P
21 20 ad2antll P 0 = A P 1 = B P 2 = C P 3 = D D = lastS P
22 10 21 syl φ D = lastS P
23 13 22 oveq12d φ A WalksOn G D = P 0 WalksOn G lastS P
24 23 breqd φ F A WalksOn G D P F P 0 WalksOn G lastS P P
25 9 24 mpbird φ F A WalksOn G D P