Theorem rusgrnumwwlklem

Description: Lemma for rusgrnumwwlk etc. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	|- V = ( Vtx ` G )
	rusgrnumwwlk.l	|- L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
Assertion	rusgrnumwwlklem	|- ( ( P e. V /\ N e. NN0 ) -> ( P L N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	|- V = ( Vtx ` G )
2		rusgrnumwwlk.l	|- L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
3		oveq1	|- ( n = N -> ( n WWalksN G ) = ( N WWalksN G ) )
4	3	adantl	|- ( ( v = P /\ n = N ) -> ( n WWalksN G ) = ( N WWalksN G ) )
5		eqeq2	|- ( v = P -> ( ( w ` 0 ) = v <-> ( w ` 0 ) = P ) )
6	5	adantr	|- ( ( v = P /\ n = N ) -> ( ( w ` 0 ) = v <-> ( w ` 0 ) = P ) )
7	4 6	rabeqbidv	|- ( ( v = P /\ n = N ) -> { w e. ( n WWalksN G ) | ( w ` 0 ) = v } = { w e. ( N WWalksN G ) | ( w ` 0 ) = P } )
8	7	fveq2d	|- ( ( v = P /\ n = N ) -> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
9		fvex	|- ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) e. _V
10	8 2 9	ovmpoa	|- ( ( P e. V /\ N e. NN0 ) -> ( P L N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )