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 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
2wlkd.v ⊢ V = Vtx ⁡ G
2wlkd.i ⊢ I = iEdg ⁡ G
Assertion 2wlkond ⊢ φ → F A WalksOn ⁡ 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 1 2 3 4 5 6 7 2wlkd ⊢ φ → F Walks ⁡ G P
9 3 simp1d ⊢ φ → A ∈ V
10 1 fveq1i ⊢ P ⁡ 0 = ⟨“ ABC ”⟩ ⁡ 0
11 s3fv0 ⊢ A ∈ V → ⟨“ ABC ”⟩ ⁡ 0 = A
12 10 11 syl5eq ⊢ 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 syl5eq ⊢ φ → 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 ”⟩ ∈ Word V
25 2 24 eqeltri ⊢ F ∈ Word V
26 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
27 1 26 eqeltri ⊢ P ∈ Word V
28 25 27 pm3.2i ⊢ F ∈ Word V ∧ P ∈ Word V
29 6 iswlkon ⊢ A ∈ V ∧ C ∈ V ∧ F ∈ Word V ∧ P ∈ Word V → F A WalksOn ⁡ G C P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
30 23 28 29 sylancl ⊢ φ → F A WalksOn ⁡ G C P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
31 8 13 21 30 mpbir3and ⊢ φ → F A WalksOn ⁡ G C P