Metamath Proof Explorer


Theorem 2trlond

Description: A trail of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 30-Jan-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 2wlkd.p P = ⟨“ ABC ”⟩
2wlkd.f F = ⟨“ JK ”⟩
2wlkd.s φ A V B V C V
2wlkd.n φ A B B C
2wlkd.e φ A B I J B C I K
2wlkd.v V = Vtx G
2wlkd.i I = iEdg G
2trld.n φ J K
Assertion 2trlond φ F A TrailsOn G C P

Proof

Step Hyp Ref Expression
1 2wlkd.p P = ⟨“ ABC ”⟩
2 2wlkd.f F = ⟨“ JK ”⟩
3 2wlkd.s φ A V B V C V
4 2wlkd.n φ A B B C
5 2wlkd.e φ A B I J B C I K
6 2wlkd.v V = Vtx G
7 2wlkd.i I = iEdg G
8 2trld.n φ J K
9 1 2 3 4 5 6 7 2wlkond φ F A WalksOn G C P
10 1 2 3 4 5 6 7 8 2trld φ F Trails G P
11 3 simp1d φ A V
12 3 simp3d φ C V
13 s2cli ⟨“ JK ”⟩ Word V
14 2 13 eqeltri F Word V
15 14 a1i φ F Word V
16 s3cli ⟨“ ABC ”⟩ Word V
17 1 16 eqeltri P Word V
18 17 a1i φ P Word V
19 6 istrlson A V C V F Word V P Word V F A TrailsOn G C P F A WalksOn G C P F Trails G P
20 11 12 15 18 19 syl22anc φ F A TrailsOn G C P F A WalksOn G C P F Trails G P
21 9 10 20 mpbir2and φ F A TrailsOn G C P