Metamath Proof Explorer

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 \land P \in V) \to \|\{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\}\| = K$

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwrdl2.v	$⊢ V = Vtx (G)$
2	1	fvexi	$⊢ V \in V$
3	2	wrdexi	$⊢ Word V \in V$
4	3	rabex	$⊢ \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\} \in V$
5	2	a1i	$⊢ G RegUSGraph K \to V \in V$
6		wrd2f1tovbij	$⊢ (V \in V \land P \in V) \to \exists f f : \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\} \underset{1-1 onto}{⟶} \{s \in V \| \{P, s\} \in Edg (G)\}$
7	5 6	sylan	$⊢ (G RegUSGraph K \land P \in V) \to \exists f f : \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\} \underset{1-1 onto}{⟶} \{s \in V \| \{P, s\} \in Edg (G)\}$
8		hasheqf1oi	$⊢ \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\} \in V \to (\exists f f : \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\} \underset{1-1 onto}{⟶} \{s \in V \| \{P, s\} \in Edg (G)\} \to \|\{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\}\| = \|\{s \in V \| \{P, s\} \in Edg (G)\}\|)$
9	4 7 8	mpsyl	$⊢ (G RegUSGraph K \land P \in V) \to \|\{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\}\| = \|\{s \in V \| \{P, s\} \in Edg (G)\}\|$
10	1	rusgrpropadjvtx	$⊢ G RegUSGraph K \to (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall p \in V \|\{s \in V \| \{p, s\} \in Edg (G)\}\| = K)$
11		preq1	$⊢ p = P \to \{p, s\} = \{P, s\}$
12	11	eleq1d	$⊢ p = P \to (\{p, s\} \in Edg (G) \leftrightarrow \{P, s\} \in Edg (G))$
13	12	rabbidv	$⊢ p = P \to \{s \in V \| \{p, s\} \in Edg (G)\} = \{s \in V \| \{P, s\} \in Edg (G)\}$
14	13	fveqeq2d	$⊢ p = P \to (\|\{s \in V \| \{p, s\} \in Edg (G)\}\| = K \leftrightarrow \|\{s \in V \| \{P, s\} \in Edg (G)\}\| = K)$
15	14	rspccv	$⊢ \forall p \in V \|\{s \in V \| \{p, s\} \in Edg (G)\}\| = K \to (P \in V \to \|\{s \in V \| \{P, s\} \in Edg (G)\}\| = K)$
16	15	3ad2ant3	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall p \in V \|\{s \in V \| \{p, s\} \in Edg (G)\}\| = K) \to (P \in V \to \|\{s \in V \| \{P, s\} \in Edg (G)\}\| = K)$
17	10 16	syl	$⊢ G RegUSGraph K \to (P \in V \to \|\{s \in V \| \{P, s\} \in Edg (G)\}\| = K)$
18	17	imp	$⊢ (G RegUSGraph K \land P \in V) \to \|\{s \in V \| \{P, s\} \in Edg (G)\}\| = K$
19	9 18	eqtrd	$⊢ (G RegUSGraph K \land P \in V) \to \|\{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in Edg (G))\}\| = K$