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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	frgr2wsp1	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
3		wpthswwlks2on	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
4	2 3	sylan	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
5	4	3adant2	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
6	5	fveq2d	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
7	1	frgr2wwlk1	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 1 )
8	6 7	eqtrd	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) ) = 1 )