Metamath Proof Explorer

Theorem frgrhash2wsp

Description: The number of simple paths of length 2 is n*(n-1) in a friendship graph with n vertices. This corresponds to the proof of claim 3 in Huneke p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, Huneke counts undirected paths, so obtains the result ( ( n _C 2 ) = ( ( n x. ( n - 1 ) ) / 2 ) ), whereas we count directed paths, obtaining twice that number. (Contributed by Alexander van der Vekens, 6-Mar-2018) (Revised by AV, 10-Jan-2022)

Ref Expression
Hypothesis frgrhash2wsp.v 
|- V = ( Vtx ` G )
Assertion frgrhash2wsp 
|- ( ( G e. FriendGraph /\ V e. Fin ) -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v 
 |-  V = ( Vtx ` G )
2 2nn 
 |-  2 e. NN
3 1 wspniunwspnon 
 |-  ( ( 2 e. NN /\ G e. FriendGraph ) -> ( 2 WSPathsN G ) = U_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) )
4 2 3 mpan 
 |-  ( G e. FriendGraph -> ( 2 WSPathsN G ) = U_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) )
5 4 fveq2d 
 |-  ( G e. FriendGraph -> ( # ` ( 2 WSPathsN G ) ) = ( # ` U_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) ) )
6 5 adantr 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( # ` ( 2 WSPathsN G ) ) = ( # ` U_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) ) )
7 simpr 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> V e. Fin )
8 eqid 
 |-  ( V \ { a } ) = ( V \ { a } )
9 1 eleq1i 
 |-  ( V e. Fin <-> ( Vtx ` G ) e. Fin )
10 wspthnonfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( a ( 2 WSPathsNOn G ) b ) e. Fin )
11 9 10 sylbi 
 |-  ( V e. Fin -> ( a ( 2 WSPathsNOn G ) b ) e. Fin )
12 11 adantl 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( a ( 2 WSPathsNOn G ) b ) e. Fin )
13 12 3ad2ant1 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V /\ b e. ( V \ { a } ) ) -> ( a ( 2 WSPathsNOn G ) b ) e. Fin )
14 2wspiundisj 
 |-  Disj_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b )
15 14 a1i 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> Disj_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) )
16 2wspdisj 
 |-  Disj_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b )
17 16 a1i 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) -> Disj_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) )
18 simplll 
 |-  ( ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) /\ b e. ( V \ { a } ) ) -> G e. FriendGraph )
19 simpr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) -> a e. V )
20 eldifi 
 |-  ( b e. ( V \ { a } ) -> b e. V )
21 19 20 anim12i 
 |-  ( ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) /\ b e. ( V \ { a } ) ) -> ( a e. V /\ b e. V ) )
22 eldifsni 
 |-  ( b e. ( V \ { a } ) -> b =/= a )
23 22 necomd 
 |-  ( b e. ( V \ { a } ) -> a =/= b )
24 23 adantl 
 |-  ( ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) /\ b e. ( V \ { a } ) ) -> a =/= b )
25 1 frgr2wsp1 
 |-  ( ( G e. FriendGraph /\ ( a e. V /\ b e. V ) /\ a =/= b ) -> ( # ` ( a ( 2 WSPathsNOn G ) b ) ) = 1 )
26 18 21 24 25 syl3anc 
 |-  ( ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V ) /\ b e. ( V \ { a } ) ) -> ( # ` ( a ( 2 WSPathsNOn G ) b ) ) = 1 )
27 26 3impa 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin ) /\ a e. V /\ b e. ( V \ { a } ) ) -> ( # ` ( a ( 2 WSPathsNOn G ) b ) ) = 1 )
28 7 8 13 15 17 27 hash2iun1dif1 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( # ` U_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) ) = ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) )
29 6 28 eqtrd 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) )