Theorem rusgrnumwrdl2

Description: In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018) (Revised by AV, 6-May-2021)

	Ref	Expression
Hypothesis	rusgrnumwrdl2.v	|- V = ( Vtx ` G )
Assertion	rusgrnumwrdl2	|- ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = K )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwrdl2.v	|- V = ( Vtx ` G )
2	1	fvexi	|- V e. _V
3	2	wrdexi	|- Word V e. _V
4	3	rabex	|- { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } e. _V
5	2	a1i	|- ( G RegUSGraph K -> V e. _V )
6		wrd2f1tovbij	|- ( ( V e. _V /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } -1-1-onto-> { s e. V | { P , s } e. ( Edg ` G ) } )
7	5 6	sylan	|- ( ( G RegUSGraph K /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } -1-1-onto-> { s e. V | { P , s } e. ( Edg ` G ) } )
8		hasheqf1oi	|- ( { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } e. _V -> ( E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } -1-1-onto-> { s e. V | { P , s } e. ( Edg ` G ) } -> ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) ) )
9	4 7 8	mpsyl	|- ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) )
10	1	rusgrpropadjvtx	|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. p e. V ( # ` { s e. V | { p , s } e. ( Edg ` G ) } ) = K ) )
11		preq1	|- ( p = P -> { p , s } = { P , s } )
12	11	eleq1d	|- ( p = P -> ( { p , s } e. ( Edg ` G ) <-> { P , s } e. ( Edg ` G ) ) )
13	12	rabbidv	|- ( p = P -> { s e. V | { p , s } e. ( Edg ` G ) } = { s e. V | { P , s } e. ( Edg ` G ) } )
14	13	fveqeq2d	|- ( p = P -> ( ( # ` { s e. V | { p , s } e. ( Edg ` G ) } ) = K <-> ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) = K ) )
15	14	rspccv	|- ( A. p e. V ( # ` { s e. V | { p , s } e. ( Edg ` G ) } ) = K -> ( P e. V -> ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) = K ) )
16	15	3ad2ant3	|- ( ( G e. USGraph /\ K e. NN0* /\ A. p e. V ( # ` { s e. V | { p , s } e. ( Edg ` G ) } ) = K ) -> ( P e. V -> ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) = K ) )
17	10 16	syl	|- ( G RegUSGraph K -> ( P e. V -> ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) = K ) )
18	17	imp	|- ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { s e. V | { P , s } e. ( Edg ` G ) } ) = K )
19	9 18	eqtrd	|- ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = K )