Metamath Proof Explorer

Theorem usgr2wspthons3

Description: A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypotheses usgr2wspthon0.v ⊢ V = Vtx ⁡ G
usgr2wspthon0.e ⊢ E = Edg ⁡ G
Assertion usgr2wspthons3 ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ A B ∈ E ∧ B C ∈ E

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ⊢ V = Vtx ⁡ G
2 usgr2wspthon0.e ⊢ E = Edg ⁡ G
3 2nn ⊢ 2 ∈ ℕ
4 ne0i ⊢ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A 2 WSPathsNOn G C ≠ ∅
5 wspthsnonn0vne ⊢ 2 ∈ ℕ ∧ A 2 WSPathsNOn G C ≠ ∅ → A ≠ C
6 3 4 5 sylancr ⊢ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C
7 simplr ⊢ G ∈ USGraph ∧ A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C
8 wpthswwlks2on ⊢ G ∈ USGraph ∧ A ≠ C → A 2 WSPathsNOn G C = A 2 WWalksNOn G C
9 8 eleq2d ⊢ G ∈ USGraph ∧ A ≠ C → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C ↔ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
10 9 biimpa ⊢ G ∈ USGraph ∧ A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
11 7 10 jca ⊢ G ∈ USGraph ∧ A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
12 11 exp31 ⊢ G ∈ USGraph → A ≠ C → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
13 12 com13 ⊢ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C → G ∈ USGraph → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
14 6 13 mpd ⊢ ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → G ∈ USGraph → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
15 14 com12 ⊢ G ∈ USGraph → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
16 9 biimprd ⊢ G ∈ USGraph ∧ A ≠ C → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C
17 16 expimpd ⊢ G ∈ USGraph → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C
18 15 17 impbid ⊢ G ∈ USGraph → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
19 18 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C
20 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
21 1 2 umgrwwlks2on ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ E ∧ B C ∈ E
22 20 21 sylan ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ E ∧ B C ∈ E
23 22 anbi2d ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A ≠ C ∧ A B ∈ E ∧ B C ∈ E
24 3anass ⊢ A ≠ C ∧ A B ∈ E ∧ B C ∈ E ↔ A ≠ C ∧ A B ∈ E ∧ B C ∈ E
25 23 24 bitr4di ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ≠ C ∧ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A ≠ C ∧ A B ∈ E ∧ B C ∈ E
26 19 25 bitrd ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ A B ∈ E ∧ B C ∈ E