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 ∈ FriendGraph ∧ V ∈ Fin → 2 WSPathsN G = V ⁢ V − 1

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v ⊢ V = Vtx ⁡ G
2 2nn ⊢ 2 ∈ ℕ
3 1 wspniunwspnon ⊢ 2 ∈ ℕ ∧ G ∈ FriendGraph → 2 WSPathsN G = ⋃ a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
4 2 3 mpan ⊢ G ∈ FriendGraph → 2 WSPathsN G = ⋃ a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
5 4 fveq2d ⊢ G ∈ FriendGraph → 2 WSPathsN G = ⋃ a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
6 5 adantr ⊢ G ∈ FriendGraph ∧ V ∈ Fin → 2 WSPathsN G = ⋃ a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
7 simpr ⊢ G ∈ FriendGraph ∧ V ∈ Fin → V ∈ Fin
8 eqid ⊢ V ∖ a = V ∖ a
9 1 eleq1i ⊢ V ∈ Fin ↔ Vtx ⁡ G ∈ Fin
10 wspthnonfi ⊢ Vtx ⁡ G ∈ Fin → a 2 WSPathsNOn G b ∈ Fin
11 9 10 sylbi ⊢ V ∈ Fin → a 2 WSPathsNOn G b ∈ Fin
12 11 adantl ⊢ G ∈ FriendGraph ∧ V ∈ Fin → a 2 WSPathsNOn G b ∈ Fin
13 12 3ad2ant1 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → a 2 WSPathsNOn G b ∈ Fin
14 2wspiundisj ⊢ Disj a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
15 14 a1i ⊢ G ∈ FriendGraph ∧ V ∈ Fin → Disj a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
16 2wspdisj ⊢ Disj b ∈ V ∖ a a 2 WSPathsNOn G b
17 16 a1i ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V → Disj b ∈ V ∖ a a 2 WSPathsNOn G b
18 simplll ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → G ∈ FriendGraph
19 simpr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V → a ∈ V
20 eldifi ⊢ b ∈ V ∖ a → b ∈ V
21 19 20 anim12i ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → a ∈ V ∧ b ∈ V
22 eldifsni ⊢ b ∈ V ∖ a → b ≠ a
23 22 necomd ⊢ b ∈ V ∖ a → a ≠ b
24 23 adantl ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → a ≠ b
25 1 frgr2wsp1 ⊢ G ∈ FriendGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b → a 2 WSPathsNOn G b = 1
26 18 21 24 25 syl3anc ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → a 2 WSPathsNOn G b = 1
27 26 3impa ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ a ∈ V ∧ b ∈ V ∖ a → a 2 WSPathsNOn G b = 1
28 7 8 13 15 17 27 hash2iun1dif1 ⊢ G ∈ FriendGraph ∧ V ∈ Fin → ⋃ a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b = V ⁢ V − 1
29 6 28 eqtrd ⊢ G ∈ FriendGraph ∧ V ∈ Fin → 2 WSPathsN G = V ⁢ V − 1