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=Vtx⁡G
rusgrnumwwlk.l ⊢L=v∈V,n∈ℕ0⟼w∈nWWalksNG|w⁡0=v
Assertion rusgrnumwwlkb0 ⊢G∈USHGraph∧P∈V→PL0=1

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢V=Vtx⁡G
2 rusgrnumwwlk.l ⊢L=v∈V,n∈ℕ0⟼w∈nWWalksNG|w⁡0=v
3 simpr ⊢G∈USHGraph∧P∈V→P∈V
4 0nn0 ⊢0∈ℕ0
5 1 2 rusgrnumwwlklem ⊢P∈V∧0∈ℕ0→PL0=w∈0WWalksNG|w⁡0=P
6 3 4 5 sylancl ⊢G∈USHGraph∧P∈V→PL0=w∈0WWalksNG|w⁡0=P
7 df-rab ⊢w∈0WWalksNG|w⁡0=P=w|w∈0WWalksNG∧w⁡0=P
8 7 a1i ⊢G∈USHGraph∧P∈V→w∈0WWalksNG|w⁡0=P=w|w∈0WWalksNG∧w⁡0=P
9 wwlksn0s ⊢0WWalksNG=w∈WordVtx⁡G|w=1
10 9 a1i ⊢G∈USHGraph∧P∈V→0WWalksNG=w∈WordVtx⁡G|w=1
11 10 eleq2d ⊢G∈USHGraph∧P∈V→w∈0WWalksNG↔w∈w∈WordVtx⁡G|w=1
12 rabid ⊢w∈w∈WordVtx⁡G|w=1↔w∈WordVtx⁡G∧w=1
13 11 12 bitrdi ⊢G∈USHGraph∧P∈V→w∈0WWalksNG↔w∈WordVtx⁡G∧w=1
14 13 anbi1d ⊢G∈USHGraph∧P∈V→w∈0WWalksNG∧w⁡0=P↔w∈WordVtx⁡G∧w=1∧w⁡0=P
15 14 abbidv ⊢G∈USHGraph∧P∈V→w|w∈0WWalksNG∧w⁡0=P=w|w∈WordVtx⁡G∧w=1∧w⁡0=P
16 wrdl1s1 ⊢P∈Vtx⁡G→v=⟨“P”⟩↔v∈WordVtx⁡G∧v=1∧v⁡0=P
17 df-3an ⊢v∈WordVtx⁡G∧v=1∧v⁡0=P↔v∈WordVtx⁡G∧v=1∧v⁡0=P
18 16 17 bitr2di ⊢P∈Vtx⁡G→v∈WordVtx⁡G∧v=1∧v⁡0=P↔v=⟨“P”⟩
19 vex ⊢v∈V
20 eleq1w ⊢w=v→w∈WordVtx⁡G↔v∈WordVtx⁡G
21 fveqeq2 ⊢w=v→w=1↔v=1
22 20 21 anbi12d ⊢w=v→w∈WordVtx⁡G∧w=1↔v∈WordVtx⁡G∧v=1
23 fveq1 ⊢w=v→w⁡0=v⁡0
24 23 eqeq1d ⊢w=v→w⁡0=P↔v⁡0=P
25 22 24 anbi12d ⊢w=v→w∈WordVtx⁡G∧w=1∧w⁡0=P↔v∈WordVtx⁡G∧v=1∧v⁡0=P
26 19 25 elab ⊢v∈w|w∈WordVtx⁡G∧w=1∧w⁡0=P↔v∈WordVtx⁡G∧v=1∧v⁡0=P
27 velsn ⊢v∈⟨“P”⟩↔v=⟨“P”⟩
28 18 26 27 3bitr4g ⊢P∈Vtx⁡G→v∈w|w∈WordVtx⁡G∧w=1∧w⁡0=P↔v∈⟨“P”⟩
29 28 1 eleq2s ⊢P∈V→v∈w|w∈WordVtx⁡G∧w=1∧w⁡0=P↔v∈⟨“P”⟩
30 29 eqrdv ⊢P∈V→w|w∈WordVtx⁡G∧w=1∧w⁡0=P=⟨“P”⟩
31 30 adantl ⊢G∈USHGraph∧P∈V→w|w∈WordVtx⁡G∧w=1∧w⁡0=P=⟨“P”⟩
32 8 15 31 3eqtrd ⊢G∈USHGraph∧P∈V→w∈0WWalksNG|w⁡0=P=⟨“P”⟩
33 32 fveq2d ⊢G∈USHGraph∧P∈V→w∈0WWalksNG|w⁡0=P=⟨“P”⟩
34 s1cl ⊢P∈V→⟨“P”⟩∈WordV
35 hashsng ⊢⟨“P”⟩∈WordV→⟨“P”⟩=1
36 34 35 syl ⊢P∈V→⟨“P”⟩=1
37 36 adantl ⊢G∈USHGraph∧P∈V→⟨“P”⟩=1
38 6 33 37 3eqtrd ⊢G∈USHGraph∧P∈V→PL0=1