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 \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WSPathsNOn G) B\| = 1$

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	$⊢ V = Vtx (G)$
2		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
3		wpthswwlks2on	$⊢ (G \in USGraph \land A \neq B) \to A (2 WSPathsNOn G) B = A (2 WWalksNOn G) B$
4	2 3	sylan	$⊢ (G \in FriendGraph \land A \neq B) \to A (2 WSPathsNOn G) B = A (2 WWalksNOn G) B$
5	4	3adant2	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to A (2 WSPathsNOn G) B = A (2 WWalksNOn G) B$
6	5	fveq2d	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WSPathsNOn G) B\| = \|A (2 WWalksNOn G) B\|$
7	1	frgr2wwlk1	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WWalksNOn G) B\| = 1$
8	6 7	eqtrd	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WSPathsNOn G) B\| = 1$