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 e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
Assertion rusgrnumwwlkb0 
|- ( ( G e. USPGraph /\ P e. V ) -> ( P L 0 ) = 1 )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v 
 |-  V = ( Vtx ` G )
2 rusgrnumwwlk.l 
 |-  L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
3 simpr 
 |-  ( ( G e. USPGraph /\ P e. V ) -> P e. V )
4 0nn0 
 |-  0 e. NN0
5 1 2 rusgrnumwwlklem 
 |-  ( ( P e. V /\ 0 e. NN0 ) -> ( P L 0 ) = ( # ` { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } ) )
6 3 4 5 sylancl 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( P L 0 ) = ( # ` { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } ) )
7 df-rab 
 |-  { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } = { w | ( w e. ( 0 WWalksN G ) /\ ( w ` 0 ) = P ) }
8 7 a1i 
 |-  ( ( G e. USPGraph /\ P e. V ) -> { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } = { w | ( w e. ( 0 WWalksN G ) /\ ( w ` 0 ) = P ) } )
9 wwlksn0s 
 |-  ( 0 WWalksN G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 }
10 9 a1i 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( 0 WWalksN G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 } )
11 10 eleq2d 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( w e. ( 0 WWalksN G ) <-> w e. { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 } ) )
12 rabid 
 |-  ( w e. { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 } <-> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) )
13 11 12 bitrdi 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( w e. ( 0 WWalksN G ) <-> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) ) )
14 13 anbi1d 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( ( w e. ( 0 WWalksN G ) /\ ( w ` 0 ) = P ) <-> ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) ) )
15 14 abbidv 
 |-  ( ( G e. USPGraph /\ P e. V ) -> { w | ( w e. ( 0 WWalksN G ) /\ ( w ` 0 ) = P ) } = { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } )
16 wrdl1s1 
 |-  ( P e. ( Vtx ` G ) -> ( v = <" P "> <-> ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 /\ ( v ` 0 ) = P ) ) )
17 df-3an 
 |-  ( ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 /\ ( v ` 0 ) = P ) <-> ( ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 ) /\ ( v ` 0 ) = P ) )
18 16 17 bitr2di 
 |-  ( P e. ( Vtx ` G ) -> ( ( ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 ) /\ ( v ` 0 ) = P ) <-> v = <" P "> ) )
19 vex 
 |-  v e. _V
20 eleq1w 
 |-  ( w = v -> ( w e. Word ( Vtx ` G ) <-> v e. Word ( Vtx ` G ) ) )
21 fveqeq2 
 |-  ( w = v -> ( ( # ` w ) = 1 <-> ( # ` v ) = 1 ) )
22 20 21 anbi12d 
 |-  ( w = v -> ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) <-> ( v e. Word ( Vtx ` 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 e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) <-> ( ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 ) /\ ( v ` 0 ) = P ) ) )
26 19 25 elab 
 |-  ( v e. { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } <-> ( ( v e. Word ( Vtx ` G ) /\ ( # ` v ) = 1 ) /\ ( v ` 0 ) = P ) )
27 velsn 
 |-  ( v e. { <" P "> } <-> v = <" P "> )
28 18 26 27 3bitr4g 
 |-  ( P e. ( Vtx ` G ) -> ( v e. { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } <-> v e. { <" P "> } ) )
29 28 1 eleq2s 
 |-  ( P e. V -> ( v e. { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } <-> v e. { <" P "> } ) )
30 29 eqrdv 
 |-  ( P e. V -> { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } = { <" P "> } )
31 30 adantl 
 |-  ( ( G e. USPGraph /\ P e. V ) -> { w | ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) /\ ( w ` 0 ) = P ) } = { <" P "> } )
32 8 15 31 3eqtrd 
 |-  ( ( G e. USPGraph /\ P e. V ) -> { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } = { <" P "> } )
33 32 fveq2d 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( # ` { w e. ( 0 WWalksN G ) | ( w ` 0 ) = P } ) = ( # ` { <" P "> } ) )
34 s1cl 
 |-  ( P e. V -> <" P "> e. Word V )
35 hashsng 
 |-  ( <" P "> e. Word V -> ( # ` { <" P "> } ) = 1 )
36 34 35 syl 
 |-  ( P e. V -> ( # ` { <" P "> } ) = 1 )
37 36 adantl 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( # ` { <" P "> } ) = 1 )
38 6 33 37 3eqtrd 
 |-  ( ( G e. USPGraph /\ P e. V ) -> ( P L 0 ) = 1 )