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 e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WSPathsNOn G ) B ) ) = 1 )

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v 
 |-  V = ( Vtx ` G )
2 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
3 wpthswwlks2on 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( A ( 2 WSPathsNOn G ) B ) = ( A ( 2 WWalksNOn G ) B ) )
4 2 3 sylan 
 |-  ( ( G e. FriendGraph /\ A =/= B ) -> ( A ( 2 WSPathsNOn G ) B ) = ( A ( 2 WWalksNOn G ) B ) )
5 4 3adant2 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A ( 2 WSPathsNOn G ) B ) = ( A ( 2 WWalksNOn G ) B ) )
6 5 fveq2d 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WSPathsNOn G ) B ) ) = ( # ` ( A ( 2 WWalksNOn G ) B ) ) )
7 1 frgr2wwlk1 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WWalksNOn G ) B ) ) = 1 )
8 6 7 eqtrd 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` ( A ( 2 WSPathsNOn G ) B ) ) = 1 )