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 ) ) )