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 โŠข ๐‘‰ = ( Vtx โ€˜ ๐บ )
Assertion frgrhash2wsp ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ( โ™ฏ โ€˜ ( 2 WSPathsN ๐บ ) ) = ( ( โ™ฏ โ€˜ ๐‘‰ ) ยท ( ( โ™ฏ โ€˜ ๐‘‰ ) โˆ’ 1 ) ) )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v โŠข ๐‘‰ = ( Vtx โ€˜ ๐บ )
2 2nn โŠข 2 โˆˆ โ„•
3 1 wspniunwspnon โŠข ( ( 2 โˆˆ โ„• โˆง ๐บ โˆˆ FriendGraph ) โ†’ ( 2 WSPathsN ๐บ ) = โˆช ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) )
4 2 3 mpan โŠข ( ๐บ โˆˆ FriendGraph โ†’ ( 2 WSPathsN ๐บ ) = โˆช ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) )
5 4 fveq2d โŠข ( ๐บ โˆˆ FriendGraph โ†’ ( โ™ฏ โ€˜ ( 2 WSPathsN ๐บ ) ) = ( โ™ฏ โ€˜ โˆช ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) )
6 5 adantr โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ( โ™ฏ โ€˜ ( 2 WSPathsN ๐บ ) ) = ( โ™ฏ โ€˜ โˆช ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) )
7 simpr โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ๐‘‰ โˆˆ Fin )
8 eqid โŠข ( ๐‘‰ โˆ– { ๐‘Ž } ) = ( ๐‘‰ โˆ– { ๐‘Ž } )
9 1 eleq1i โŠข ( ๐‘‰ โˆˆ Fin โ†” ( Vtx โ€˜ ๐บ ) โˆˆ Fin )
10 wspthnonfi โŠข ( ( Vtx โ€˜ ๐บ ) โˆˆ Fin โ†’ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) โˆˆ Fin )
11 9 10 sylbi โŠข ( ๐‘‰ โˆˆ Fin โ†’ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) โˆˆ Fin )
12 11 adantl โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) โˆˆ Fin )
13 12 3ad2ant1 โŠข ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) โˆˆ Fin )
14 2wspiundisj โŠข Disj ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ )
15 14 a1i โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ Disj ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) )
16 2wspdisj โŠข Disj ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ )
17 16 a1i โŠข ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โ†’ Disj ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) )
18 simplll โŠข ( ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ๐บ โˆˆ FriendGraph )
19 simpr โŠข ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โ†’ ๐‘Ž โˆˆ ๐‘‰ )
20 eldifi โŠข ( ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) โ†’ ๐‘ โˆˆ ๐‘‰ )
21 19 20 anim12i โŠข ( ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ( ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) )
22 eldifsni โŠข ( ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) โ†’ ๐‘ โ‰  ๐‘Ž )
23 22 necomd โŠข ( ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) โ†’ ๐‘Ž โ‰  ๐‘ )
24 23 adantl โŠข ( ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ๐‘Ž โ‰  ๐‘ )
25 1 frgr2wsp1 โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ( ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) โˆง ๐‘Ž โ‰  ๐‘ ) โ†’ ( โ™ฏ โ€˜ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) = 1 )
26 18 21 24 25 syl3anc โŠข ( ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ( โ™ฏ โ€˜ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) = 1 )
27 26 3impa โŠข ( ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ) โ†’ ( โ™ฏ โ€˜ ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) = 1 )
28 7 8 13 15 17 27 hash2iun1dif1 โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ( โ™ฏ โ€˜ โˆช ๐‘Ž โˆˆ ๐‘‰ โˆช ๐‘ โˆˆ ( ๐‘‰ โˆ– { ๐‘Ž } ) ( ๐‘Ž ( 2 WSPathsNOn ๐บ ) ๐‘ ) ) = ( ( โ™ฏ โ€˜ ๐‘‰ ) ยท ( ( โ™ฏ โ€˜ ๐‘‰ ) โˆ’ 1 ) ) )
29 6 28 eqtrd โŠข ( ( ๐บ โˆˆ FriendGraph โˆง ๐‘‰ โˆˆ Fin ) โ†’ ( โ™ฏ โ€˜ ( 2 WSPathsN ๐บ ) ) = ( ( โ™ฏ โ€˜ ๐‘‰ ) ยท ( ( โ™ฏ โ€˜ ๐‘‰ ) โˆ’ 1 ) ) )