Theorem rusgrnumwwlkb1

Description: Induction base 1 for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 28-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	rusgrnumwwlkb1	|- ( ( G RegUSGraph K /\ P e. V ) -> ( P L 1 ) = K )

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		simpr	|- ( ( G RegUSGraph K /\ P e. V ) -> P e. V )
4		1nn0	|- 1 e. NN0
5	1 2	rusgrnumwwlklem	|- ( ( P e. V /\ 1 e. NN0 ) -> ( P L 1 ) = ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) )
6	3 4 5	sylancl	|- ( ( G RegUSGraph K /\ P e. V ) -> ( P L 1 ) = ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) )
7	1	rusgrnumwwlkl1	|- ( ( G RegUSGraph K /\ P e. V ) -> ( # ` { w e. ( 1 WWalksN G ) | ( w ` 0 ) = P } ) = K )
8	6 7	eqtrd	|- ( ( G RegUSGraph K /\ P e. V ) -> ( P L 1 ) = K )