Metamath Proof Explorer

Theorem frgr2wsp1

Description: In a friendship graph, there is exactly one simple path of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 13-May-2021)

Ref Expression
Hypothesis frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
Assertion frgr2wsp1 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WSPathsNOn G B = 1

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v ⊢ V = Vtx ⁡ G
2 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
3 wpthswwlks2on ⊢ G ∈ USGraph ∧ A ≠ B → A 2 WSPathsNOn G B = A 2 WWalksNOn G B
4 2 3 sylan ⊢ G ∈ FriendGraph ∧ A ≠ B → A 2 WSPathsNOn G B = A 2 WWalksNOn G B
5 4 3adant2 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WSPathsNOn G B = A 2 WWalksNOn G B
6 5 fveq2d ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WSPathsNOn G B = A 2 WWalksNOn G B
7 1 frgr2wwlk1 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WWalksNOn G B = 1
8 6 7 eqtrd ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A 2 WSPathsNOn G B = 1