# Metamath Proof Explorer

## Theorem rusgrnumwwlkb0

Description: Induction base 0 for rusgrnumwwlk . Here, we do not need the regularity of the graph yet. (Contributed by Alexander van der Vekens, 24-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypotheses rusgrnumwwlk.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
rusgrnumwwlk.l ${⊢}{L}=\left({v}\in {V},{n}\in {ℕ}_{0}⟼\left|\left\{{w}\in \left({n}\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={v}\right\}\right|\right)$
Assertion rusgrnumwwlkb0 ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to {P}{L}0=1$

### Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 rusgrnumwwlk.l ${⊢}{L}=\left({v}\in {V},{n}\in {ℕ}_{0}⟼\left|\left\{{w}\in \left({n}\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={v}\right\}\right|\right)$
3 simpr ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to {P}\in {V}$
4 0nn0 ${⊢}0\in {ℕ}_{0}$
5 1 2 rusgrnumwwlklem ${⊢}\left({P}\in {V}\wedge 0\in {ℕ}_{0}\right)\to {P}{L}0=\left|\left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}\right|$
6 3 4 5 sylancl ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to {P}{L}0=\left|\left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}\right|$
7 df-rab ${⊢}\left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}=\left\{{w}|\left({w}\in \left(0\mathrm{WWalksN}{G}\right)\wedge {w}\left(0\right)={P}\right)\right\}$
8 7 a1i ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}=\left\{{w}|\left({w}\in \left(0\mathrm{WWalksN}{G}\right)\wedge {w}\left(0\right)={P}\right)\right\}$
9 wwlksn0s ${⊢}0\mathrm{WWalksN}{G}=\left\{{w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)|\left|{w}\right|=1\right\}$
10 9 a1i ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to 0\mathrm{WWalksN}{G}=\left\{{w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)|\left|{w}\right|=1\right\}$
11 10 eleq2d ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left({w}\in \left(0\mathrm{WWalksN}{G}\right)↔{w}\in \left\{{w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)|\left|{w}\right|=1\right\}\right)$
12 rabid ${⊢}{w}\in \left\{{w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)|\left|{w}\right|=1\right\}↔\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)$
13 11 12 syl6bb ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left({w}\in \left(0\mathrm{WWalksN}{G}\right)↔\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\right)$
14 13 anbi1d ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left(\left({w}\in \left(0\mathrm{WWalksN}{G}\right)\wedge {w}\left(0\right)={P}\right)↔\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right)$
15 14 abbidv ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left\{{w}|\left({w}\in \left(0\mathrm{WWalksN}{G}\right)\wedge {w}\left(0\right)={P}\right)\right\}=\left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}$
16 wrdl1s1 ${⊢}{P}\in \mathrm{Vtx}\left({G}\right)\to \left({v}=⟨“{P}”⟩↔\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\wedge {v}\left(0\right)={P}\right)\right)$
17 df-3an ${⊢}\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\wedge {v}\left(0\right)={P}\right)↔\left(\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\right)\wedge {v}\left(0\right)={P}\right)$
18 16 17 syl6rbb ${⊢}{P}\in \mathrm{Vtx}\left({G}\right)\to \left(\left(\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\right)\wedge {v}\left(0\right)={P}\right)↔{v}=⟨“{P}”⟩\right)$
19 vex ${⊢}{v}\in \mathrm{V}$
20 eleq1w ${⊢}{w}={v}\to \left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)↔{v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)$
21 fveqeq2 ${⊢}{w}={v}\to \left(\left|{w}\right|=1↔\left|{v}\right|=1\right)$
22 20 21 anbi12d ${⊢}{w}={v}\to \left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)↔\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\right)\right)$
23 fveq1 ${⊢}{w}={v}\to {w}\left(0\right)={v}\left(0\right)$
24 23 eqeq1d ${⊢}{w}={v}\to \left({w}\left(0\right)={P}↔{v}\left(0\right)={P}\right)$
25 22 24 anbi12d ${⊢}{w}={v}\to \left(\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)↔\left(\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\right)\wedge {v}\left(0\right)={P}\right)\right)$
26 19 25 elab ${⊢}{v}\in \left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}↔\left(\left({v}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{v}\right|=1\right)\wedge {v}\left(0\right)={P}\right)$
27 velsn ${⊢}{v}\in \left\{⟨“{P}”⟩\right\}↔{v}=⟨“{P}”⟩$
28 18 26 27 3bitr4g ${⊢}{P}\in \mathrm{Vtx}\left({G}\right)\to \left({v}\in \left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}↔{v}\in \left\{⟨“{P}”⟩\right\}\right)$
29 28 1 eleq2s ${⊢}{P}\in {V}\to \left({v}\in \left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}↔{v}\in \left\{⟨“{P}”⟩\right\}\right)$
30 29 eqrdv ${⊢}{P}\in {V}\to \left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}=\left\{⟨“{P}”⟩\right\}$
31 30 adantl ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left\{{w}|\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|=1\right)\wedge {w}\left(0\right)={P}\right)\right\}=\left\{⟨“{P}”⟩\right\}$
32 8 15 31 3eqtrd ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}=\left\{⟨“{P}”⟩\right\}$
33 32 fveq2d ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left|\left\{{w}\in \left(0\mathrm{WWalksN}{G}\right)|{w}\left(0\right)={P}\right\}\right|=\left|\left\{⟨“{P}”⟩\right\}\right|$
34 s1cl ${⊢}{P}\in {V}\to ⟨“{P}”⟩\in \mathrm{Word}{V}$
35 hashsng ${⊢}⟨“{P}”⟩\in \mathrm{Word}{V}\to \left|\left\{⟨“{P}”⟩\right\}\right|=1$
36 34 35 syl ${⊢}{P}\in {V}\to \left|\left\{⟨“{P}”⟩\right\}\right|=1$
37 36 adantl ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to \left|\left\{⟨“{P}”⟩\right\}\right|=1$
38 6 33 37 3eqtrd ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {P}\in {V}\right)\to {P}{L}0=1$