Metamath Proof Explorer

Theorem 2wlkond

Description: A walk 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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
2wlkd.v ⊢V=Vtx⁡G
2wlkd.i ⊢I=iEdg⁡G
Assertion 2wlkond ⊢φ→FAWalksOn⁡GCP

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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
6 2wlkd.v ⊢V=Vtx⁡G
7 2wlkd.i ⊢I=iEdg⁡G
8 1 2 3 4 5 6 7 2wlkd ⊢φ→FWalks⁡GP
9 3 simp1d ⊢φ→A∈V
10 1 fveq1i ⊢P⁡0=⟨“ABC”⟩⁡0
11 s3fv0 ⊢A∈V→⟨“ABC”⟩⁡0=A
12 10 11 eqtrid ⊢A∈V→P⁡0=A
13 9 12 syl ⊢φ→P⁡0=A
14 2 fveq2i ⊢F=⟨“JK”⟩
15 s2len ⊢⟨“JK”⟩=2
16 14 15 eqtri ⊢F=2
17 1 16 fveq12i ⊢P⁡F=⟨“ABC”⟩⁡2
18 3 simp3d ⊢φ→C∈V
19 s3fv2 ⊢C∈V→⟨“ABC”⟩⁡2=C
20 18 19 syl ⊢φ→⟨“ABC”⟩⁡2=C
21 17 20 eqtrid ⊢φ→P⁡F=C
22 3simpb ⊢A∈V∧B∈V∧C∈V→A∈V∧C∈V
23 3 22 syl ⊢φ→A∈V∧C∈V
24 s2cli ⊢⟨“JK”⟩∈WordV
25 2 24 eqeltri ⊢F∈WordV
26 s3cli ⊢⟨“ABC”⟩∈WordV
27 1 26 eqeltri ⊢P∈WordV
28 25 27 pm3.2i ⊢F∈WordV∧P∈WordV
29 6 iswlkon ⊢A∈V∧C∈V∧F∈WordV∧P∈WordV→FAWalksOn⁡GCP↔FWalks⁡GP∧P⁡0=A∧P⁡F=C
30 23 28 29 sylancl ⊢φ→FAWalksOn⁡GCP↔FWalks⁡GP∧P⁡0=A∧P⁡F=C
31 8 13 21 30 mpbir3and ⊢φ→FAWalksOn⁡GCP