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 ⊢GRegUSGraphK∧P∈V→w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G=K

Proof

Step Hyp Ref Expression
1 rusgrnumwrdl2.v ⊢V=Vtx⁡G
2 1 fvexi ⊢V∈V
3 2 wrdexi ⊢WordV∈V
4 3 rabex ⊢w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G∈V
5 2 a1i ⊢GRegUSGraphK→V∈V
6 wrd2f1tovbij ⊢V∈V∧P∈V→∃ff:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G⟶1-1 ontos∈V|Ps∈Edg⁡G
7 5 6 sylan ⊢GRegUSGraphK∧P∈V→∃ff:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G⟶1-1 ontos∈V|Ps∈Edg⁡G
8 hasheqf1oi ⊢w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G∈V→∃ff:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G⟶1-1 ontos∈V|Ps∈Edg⁡G→w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G=s∈V|Ps∈Edg⁡G
9 4 7 8 mpsyl ⊢GRegUSGraphK∧P∈V→w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G=s∈V|Ps∈Edg⁡G
10 1 rusgrpropadjvtx ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀p∈Vs∈V|ps∈Edg⁡G=K
11 preq1 ⊢p=P→ps=Ps
12 11 eleq1d ⊢p=P→ps∈Edg⁡G↔Ps∈Edg⁡G
13 12 rabbidv ⊢p=P→s∈V|ps∈Edg⁡G=s∈V|Ps∈Edg⁡G
14 13 fveqeq2d ⊢p=P→s∈V|ps∈Edg⁡G=K↔s∈V|Ps∈Edg⁡G=K
15 14 rspccv ⊢∀p∈Vs∈V|ps∈Edg⁡G=K→P∈V→s∈V|Ps∈Edg⁡G=K
16 15 3ad2ant3 ⊢G∈USGraph∧K∈ℕ0*∧∀p∈Vs∈V|ps∈Edg⁡G=K→P∈V→s∈V|Ps∈Edg⁡G=K
17 10 16 syl ⊢GRegUSGraphK→P∈V→s∈V|Ps∈Edg⁡G=K
18 17 imp ⊢GRegUSGraphK∧P∈V→s∈V|Ps∈Edg⁡G=K
19 9 18 eqtrd ⊢GRegUSGraphK∧P∈V→w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Edg⁡G=K