Metamath Proof Explorer


Theorem fusgreghash2wsp

Description: In a finite k-regular graph with N vertices there are N times "k choose 2" paths with length 2, according to statement 8 in Huneke p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by length 3 strings, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 19-May-2021) (Proof shortened by AV, 12-Jan-2022)

Ref Expression
Hypothesis fusgreghash2wsp.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion fusgreghash2wsp ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fusgreghash2wsp.v 𝑉 = ( Vtx ‘ 𝐺 )
2 fveq1 ( 𝑠 = 𝑡 → ( 𝑠 ‘ 1 ) = ( 𝑡 ‘ 1 ) )
3 2 eqeq1d ( 𝑠 = 𝑡 → ( ( 𝑠 ‘ 1 ) = 𝑎 ↔ ( 𝑡 ‘ 1 ) = 𝑎 ) )
4 3 cbvrabv { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } = { 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑡 ‘ 1 ) = 𝑎 }
5 4 mpteq2i ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) = ( 𝑎𝑉 ↦ { 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑡 ‘ 1 ) = 𝑎 } )
6 1 5 fusgreg2wsp ( 𝐺 ∈ FinUSGraph → ( 2 WSPathsN 𝐺 ) = 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) )
7 6 ad2antrr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 2 WSPathsN 𝐺 ) = 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) )
8 7 fveq2d ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ♯ ‘ 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) )
9 1 fusgrvtxfi ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
10 eqeq2 ( 𝑎 = 𝑦 → ( ( 𝑠 ‘ 1 ) = 𝑎 ↔ ( 𝑠 ‘ 1 ) = 𝑦 ) )
11 10 rabbidv ( 𝑎 = 𝑦 → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } )
12 eqid ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) = ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } )
13 ovex ( 2 WSPathsN 𝐺 ) ∈ V
14 13 rabex { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ V
15 11 12 14 fvmpt ( 𝑦𝑉 → ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } )
16 15 adantl ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦𝑉 ) → ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } )
17 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
18 17 fusgrvtxfi ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin )
19 wspthnfi ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 2 WSPathsN 𝐺 ) ∈ Fin )
20 rabfi ( ( 2 WSPathsN 𝐺 ) ∈ Fin → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin )
21 18 19 20 3syl ( 𝐺 ∈ FinUSGraph → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin )
22 21 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦𝑉 ) → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin )
23 16 22 eqeltrd ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦𝑉 ) → ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ∈ Fin )
24 1 5 2wspmdisj Disj 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 )
25 24 a1i ( 𝐺 ∈ FinUSGraph → Disj 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) )
26 9 23 25 hashiun ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) )
27 26 ad2antrr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ 𝑦𝑉 ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) )
28 1 5 fusgreghash2wspv ( 𝐺 ∈ FinUSGraph → ∀ 𝑣𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
29 ralim ( ∀ 𝑣𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
30 28 29 syl ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
31 30 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
32 31 imp ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ∀ 𝑣𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
33 2fveq3 ( 𝑣 = 𝑦 → ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) )
34 33 eqeq1d ( 𝑣 = 𝑦 → ( ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ↔ ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) )
35 34 rspccva ( ( ∀ 𝑣𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ∧ 𝑦𝑉 ) → ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
36 32 35 sylan ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑦𝑉 ) → ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) )
37 36 sumeq2dv ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) )
38 9 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin )
39 eqid ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
40 1 39 fusgrregdegfi ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾𝐾 ∈ ℕ0 ) )
41 40 imp ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0 )
42 41 nn0cnd ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℂ )
43 kcnktkm1cn ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ )
44 42 43 syl ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ )
45 fsumconst ( ( 𝑉 ∈ Fin ∧ ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) → Σ 𝑦𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) )
46 38 44 45 syl2an2r ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) )
47 37 46 eqtrd ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦𝑉 ( ♯ ‘ ( ( 𝑎𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) )
48 8 27 47 3eqtrd ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) )
49 48 ex ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) )