Metamath Proof Explorer

Theorem fusgreghash2wspv

Description: According to statement 7 in Huneke p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For directed simple paths of length 2 represented by length 3 strings, we have again k*(k-1) such paths, see also comment of frgrhash2wsp . (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 12-Feb-2022)

Ref Expression
Hypotheses frgrhash2wsp.v 
|- V = ( Vtx ` G )
fusgreg2wsp.m 
|- M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
Assertion fusgreghash2wspv 
|- ( G e. FinUSGraph -> A. v e. V ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( M ` v ) ) = ( K x. ( K - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v 
 |-  V = ( Vtx ` G )
2 fusgreg2wsp.m 
 |-  M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
3 1 2 fusgr2wsp2nb 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( M ` v ) = U_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } )
4 3 fveq2d 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( # ` ( M ` v ) ) = ( # ` U_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } ) )
5 4 adantr 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` ( M ` v ) ) = ( # ` U_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } ) )
6 1 eleq2i 
 |-  ( v e. V <-> v e. ( Vtx ` G ) )
7 nbfiusgrfi 
 |-  ( ( G e. FinUSGraph /\ v e. ( Vtx ` G ) ) -> ( G NeighbVtx v ) e. Fin )
8 6 7 sylan2b 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( G NeighbVtx v ) e. Fin )
9 8 adantr 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( G NeighbVtx v ) e. Fin )
10 eqid 
 |-  ( ( G NeighbVtx v ) \ { c } ) = ( ( G NeighbVtx v ) \ { c } )
11 snfi 
 |-  { <" c v d "> } e. Fin
12 11 a1i 
 |-  ( ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) /\ c e. ( G NeighbVtx v ) /\ d e. ( ( G NeighbVtx v ) \ { c } ) ) -> { <" c v d "> } e. Fin )
13 1 nbgrssvtx 
 |-  ( G NeighbVtx v ) C_ V
14 13 a1i 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ c e. ( G NeighbVtx v ) ) -> ( G NeighbVtx v ) C_ V )
15 14 ssdifd 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ c e. ( G NeighbVtx v ) ) -> ( ( G NeighbVtx v ) \ { c } ) C_ ( V \ { c } ) )
16 iunss1 
 |-  ( ( ( G NeighbVtx v ) \ { c } ) C_ ( V \ { c } ) -> U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } C_ U_ d e. ( V \ { c } ) { <" c v d "> } )
17 15 16 syl 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ c e. ( G NeighbVtx v ) ) -> U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } C_ U_ d e. ( V \ { c } ) { <" c v d "> } )
18 17 ralrimiva 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> A. c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } C_ U_ d e. ( V \ { c } ) { <" c v d "> } )
19 simpr 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> v e. V )
20 s3iunsndisj 
 |-  ( v e. V -> Disj_ c e. ( G NeighbVtx v ) U_ d e. ( V \ { c } ) { <" c v d "> } )
21 19 20 syl 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> Disj_ c e. ( G NeighbVtx v ) U_ d e. ( V \ { c } ) { <" c v d "> } )
22 disjss2 
 |-  ( A. c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } C_ U_ d e. ( V \ { c } ) { <" c v d "> } -> ( Disj_ c e. ( G NeighbVtx v ) U_ d e. ( V \ { c } ) { <" c v d "> } -> Disj_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } ) )
23 18 21 22 sylc 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> Disj_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } )
24 23 adantr 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> Disj_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } )
25 19 adantr 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> v e. V )
26 25 anim1ci 
 |-  ( ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) /\ c e. ( G NeighbVtx v ) ) -> ( c e. ( G NeighbVtx v ) /\ v e. V ) )
27 s3sndisj 
 |-  ( ( c e. ( G NeighbVtx v ) /\ v e. V ) -> Disj_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } )
28 26 27 syl 
 |-  ( ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) /\ c e. ( G NeighbVtx v ) ) -> Disj_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } )
29 s3cli 
 |-  <" c v d "> e. Word _V
30 hashsng 
 |-  ( <" c v d "> e. Word _V -> ( # ` { <" c v d "> } ) = 1 )
31 29 30 mp1i 
 |-  ( ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) /\ c e. ( G NeighbVtx v ) /\ d e. ( ( G NeighbVtx v ) \ { c } ) ) -> ( # ` { <" c v d "> } ) = 1 )
32 9 10 12 24 28 31 hash2iun1dif1 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` U_ c e. ( G NeighbVtx v ) U_ d e. ( ( G NeighbVtx v ) \ { c } ) { <" c v d "> } ) = ( ( # ` ( G NeighbVtx v ) ) x. ( ( # ` ( G NeighbVtx v ) ) - 1 ) ) )
33 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
34 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
35 33 34 sylan 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
36 id 
 |-  ( ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
37 oveq1 
 |-  ( ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) -> ( ( # ` ( G NeighbVtx v ) ) - 1 ) = ( ( ( VtxDeg ` G ) ` v ) - 1 ) )
38 36 37 oveq12d 
 |-  ( ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) -> ( ( # ` ( G NeighbVtx v ) ) x. ( ( # ` ( G NeighbVtx v ) ) - 1 ) ) = ( ( ( VtxDeg ` G ) ` v ) x. ( ( ( VtxDeg ` G ) ` v ) - 1 ) ) )
39 35 38 syl 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( ( # ` ( G NeighbVtx v ) ) x. ( ( # ` ( G NeighbVtx v ) ) - 1 ) ) = ( ( ( VtxDeg ` G ) ` v ) x. ( ( ( VtxDeg ` G ) ` v ) - 1 ) ) )
40 id 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( VtxDeg ` G ) ` v ) = K )
41 oveq1 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) - 1 ) = ( K - 1 ) )
42 40 41 oveq12d 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) x. ( ( ( VtxDeg ` G ) ` v ) - 1 ) ) = ( K x. ( K - 1 ) ) )
43 39 42 sylan9eq 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( ( # ` ( G NeighbVtx v ) ) x. ( ( # ` ( G NeighbVtx v ) ) - 1 ) ) = ( K x. ( K - 1 ) ) )
44 5 32 43 3eqtrd 
 |-  ( ( ( G e. FinUSGraph /\ v e. V ) /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` ( M ` v ) ) = ( K x. ( K - 1 ) ) )
45 44 ex 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( M ` v ) ) = ( K x. ( K - 1 ) ) ) )
46 45 ralrimiva 
 |-  ( G e. FinUSGraph -> A. v e. V ( ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( M ` v ) ) = ( K x. ( K - 1 ) ) ) )