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