rusgrnumwwlkb1

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	$⊢ V = Vtx (G)$
	rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
Assertion	rusgrnumwwlkb1	$⊢ (G RegUSGraph K \land P \in V) \to P L 1 = K$

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	$⊢ V = Vtx (G)$
2		rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
3		simpr	$⊢ (G RegUSGraph K \land P \in V) \to P \in V$
4		1nn0	$⊢ 1 \in ℕ_{0}$
5	1 2	rusgrnumwwlklem	$⊢ (P \in V \land 1 \in ℕ_{0}) \to P L 1 = \|\{w \in (1 WWalksN G) \| w (0) = P\}\|$
6	3 4 5	sylancl	$⊢ (G RegUSGraph K \land P \in V) \to P L 1 = \|\{w \in (1 WWalksN G) \| w (0) = P\}\|$
7	1	rusgrnumwwlkl1	$⊢ (G RegUSGraph K \land P \in V) \to \|\{w \in (1 WWalksN G) \| w (0) = P\}\| = K$
8	6 7	eqtrd	$⊢ (G RegUSGraph K \land P \in V) \to P L 1 = K$

Metamath Proof Explorer