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 
|- V = ( Vtx ` G )
Assertion fusgreghash2wsp 
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fusgreghash2wsp.v 
 |-  V = ( Vtx ` G )
2 fveq1 
 |-  ( s = t -> ( s ` 1 ) = ( t ` 1 ) )
3 2 eqeq1d 
 |-  ( s = t -> ( ( s ` 1 ) = a <-> ( t ` 1 ) = a ) )
4 3 cbvrabv 
 |-  { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } = { t e. ( 2 WSPathsN G ) | ( t ` 1 ) = a }
5 4 mpteq2i 
 |-  ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) = ( a e. V |-> { t e. ( 2 WSPathsN G ) | ( t ` 1 ) = a } )
6 1 5 fusgreg2wsp 
 |-  ( G e. FinUSGraph -> ( 2 WSPathsN G ) = U_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) )
7 6 ad2antrr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( 2 WSPathsN G ) = U_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) )
8 7 fveq2d 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` ( 2 WSPathsN G ) ) = ( # ` U_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) )
9 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
10 eqeq2 
 |-  ( a = y -> ( ( s ` 1 ) = a <-> ( s ` 1 ) = y ) )
11 10 rabbidv 
 |-  ( a = y -> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } = { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } )
12 eqid 
 |-  ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) = ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } )
13 ovex 
 |-  ( 2 WSPathsN G ) e. _V
14 13 rabex 
 |-  { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } e. _V
15 11 12 14 fvmpt 
 |-  ( y e. V -> ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) = { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } )
16 15 adantl 
 |-  ( ( G e. FinUSGraph /\ y e. V ) -> ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) = { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } )
17 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
18 17 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin )
19 wspthnfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( 2 WSPathsN G ) e. Fin )
20 rabfi 
 |-  ( ( 2 WSPathsN G ) e. Fin -> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } e. Fin )
21 18 19 20 3syl 
 |-  ( G e. FinUSGraph -> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } e. Fin )
22 21 adantr 
 |-  ( ( G e. FinUSGraph /\ y e. V ) -> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = y } e. Fin )
23 16 22 eqeltrd 
 |-  ( ( G e. FinUSGraph /\ y e. V ) -> ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) e. Fin )
24 1 5 2wspmdisj 
 |-  Disj_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y )
25 24 a1i 
 |-  ( G e. FinUSGraph -> Disj_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) )
26 9 23 25 hashiun 
 |-  ( G e. FinUSGraph -> ( # ` U_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = sum_ y e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) )
27 26 ad2antrr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` U_ y e. V ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = sum_ y e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) )
28 1 5 fusgreghash2wspv 
 |-  ( G e. FinUSGraph -> A. v e. V ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) ) )
29 ralim 
 |-  ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> A. v e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) ) )
30 28 29 syl 
 |-  ( G e. FinUSGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> A. v e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) ) )
31 30 adantr 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> A. v e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) ) )
32 31 imp 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> A. v e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) )
33 2fveq3 
 |-  ( v = y -> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) )
34 33 eqeq1d 
 |-  ( v = y -> ( ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) <-> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = ( K x. ( K - 1 ) ) ) )
35 34 rspccva 
 |-  ( ( A. v e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` v ) ) = ( K x. ( K - 1 ) ) /\ y e. V ) -> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = ( K x. ( K - 1 ) ) )
36 32 35 sylan 
 |-  ( ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) /\ y e. V ) -> ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = ( K x. ( K - 1 ) ) )
37 36 sumeq2dv 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> sum_ y e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = sum_ y e. V ( K x. ( K - 1 ) ) )
38 9 adantr 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> V e. Fin )
39 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
40 1 39 fusgrregdegfi 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> K e. NN0 ) )
41 40 imp 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> K e. NN0 )
42 41 nn0cnd 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> K e. CC )
43 kcnktkm1cn 
 |-  ( K e. CC -> ( K x. ( K - 1 ) ) e. CC )
44 42 43 syl 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( K x. ( K - 1 ) ) e. CC )
45 fsumconst 
 |-  ( ( V e. Fin /\ ( K x. ( K - 1 ) ) e. CC ) -> sum_ y e. V ( K x. ( K - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) )
46 38 44 45 syl2an2r 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> sum_ y e. V ( K x. ( K - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) )
47 37 46 eqtrd 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> sum_ y e. V ( # ` ( ( a e. V |-> { s e. ( 2 WSPathsN G ) | ( s ` 1 ) = a } ) ` y ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) )
48 8 27 47 3eqtrd 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) )
49 48 ex 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )