Metamath Proof Explorer

Theorem rusgrnumwwlks

Description: Induction step for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 27-May-2022)

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 rusgrnumwwlks 
|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 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 simpr2 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> P e. V )
4 simpr3 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> N e. NN0 )
5 1 2 rusgrnumwwlklem 
 |-  ( ( P e. V /\ N e. NN0 ) -> ( P L N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
6 5 eqeq1d 
 |-  ( ( P e. V /\ N e. NN0 ) -> ( ( P L N ) = ( K ^ N ) <-> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) )
7 3 4 6 syl2anc 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) <-> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) )
8 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
9 8 wwlksnredwwlkn0 
 |-  ( ( N e. NN0 /\ w e. ( ( N + 1 ) WWalksN G ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) )
10 9 ex 
 |-  ( N e. NN0 -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( ( w ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) ) )
11 10 3ad2ant3 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( ( w ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) ) )
12 11 adantl 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( ( w ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) ) )
13 12 imp 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( N + 1 ) WWalksN G ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) )
14 13 rabbidva 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } = { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
15 14 adantr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } = { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
16 15 fveq2d 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) = ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
17 simp2 
 |-  ( ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) -> ( y ` 0 ) = P )
18 17 pm4.71ri 
 |-  ( ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) <-> ( ( y ` 0 ) = P /\ ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) )
19 18 a1i 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( N + 1 ) WWalksN G ) ) /\ y e. ( N WWalksN G ) ) -> ( ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) <-> ( ( y ` 0 ) = P /\ ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) ) )
20 19 rexbidva 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( N + 1 ) WWalksN G ) ) -> ( E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) <-> E. y e. ( N WWalksN G ) ( ( y ` 0 ) = P /\ ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) ) )
21 fveq1 
 |-  ( x = y -> ( x ` 0 ) = ( y ` 0 ) )
22 21 eqeq1d 
 |-  ( x = y -> ( ( x ` 0 ) = P <-> ( y ` 0 ) = P ) )
23 22 rexrab 
 |-  ( E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) <-> E. y e. ( N WWalksN G ) ( ( y ` 0 ) = P /\ ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) )
24 20 23 bitr4di 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( N + 1 ) WWalksN G ) ) -> ( E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) <-> E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) ) )
25 24 rabbidva 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } = { w e. ( ( N + 1 ) WWalksN G ) | E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
26 25 adantr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } = { w e. ( ( N + 1 ) WWalksN G ) | E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
27 26 fveq2d 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
28 simplr1 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> V e. Fin )
29 1 eleq1i 
 |-  ( V e. Fin <-> ( Vtx ` G ) e. Fin )
30 29 biimpi 
 |-  ( V e. Fin -> ( Vtx ` G ) e. Fin )
31 eqid 
 |-  ( ( N + 1 ) WWalksN G ) = ( ( N + 1 ) WWalksN G )
32 eqid 
 |-  { x e. ( N WWalksN G ) | ( x ` 0 ) = P } = { x e. ( N WWalksN G ) | ( x ` 0 ) = P }
33 31 8 32 hashwwlksnext 
 |-  ( ( Vtx ` G ) e. Fin -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
34 28 30 33 3syl 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
35 fveq1 
 |-  ( x = w -> ( x ` 0 ) = ( w ` 0 ) )
36 35 eqeq1d 
 |-  ( x = w -> ( ( x ` 0 ) = P <-> ( w ` 0 ) = P ) )
37 36 cbvrabv 
 |-  { x e. ( N WWalksN G ) | ( x ` 0 ) = P } = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
38 37 sumeq1i 
 |-  sum_ y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
39 38 a1i 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { x e. ( N WWalksN G ) | ( x ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
40 27 34 39 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | E. y e. ( N WWalksN G ) ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
41 rusgrnumwwlkslem 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
42 41 eqcomd 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } )
43 42 fveq2d 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
44 43 adantl 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) )
45 elrabi 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> y e. ( N WWalksN G ) )
46 45 adantl 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) -> y e. ( N WWalksN G ) )
47 1 8 wwlksnexthasheq 
 |-  ( y e. ( N WWalksN G ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) )
48 46 47 syl 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) )
49 1 rusgrpropadjvtx 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K ) )
50 fveq1 
 |-  ( w = y -> ( w ` 0 ) = ( y ` 0 ) )
51 50 eqeq1d 
 |-  ( w = y -> ( ( w ` 0 ) = P <-> ( y ` 0 ) = P ) )
52 51 elrab 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } <-> ( y e. ( N WWalksN G ) /\ ( y ` 0 ) = P ) )
53 1 8 wwlknp 
 |-  ( y e. ( N WWalksN G ) -> ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
54 53 adantr 
 |-  ( ( y e. ( N WWalksN G ) /\ ( y ` 0 ) = P ) -> ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
55 simpll 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> y e. Word V )
56 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
57 56 3ad2ant3 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> 0 < ( N + 1 ) )
58 57 adantl 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> 0 < ( N + 1 ) )
59 breq2 
 |-  ( ( # ` y ) = ( N + 1 ) -> ( 0 < ( # ` y ) <-> 0 < ( N + 1 ) ) )
60 59 ad2antlr 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` y ) <-> 0 < ( N + 1 ) ) )
61 58 60 mpbird 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> 0 < ( # ` y ) )
62 hashle00 
 |-  ( y e. Word V -> ( ( # ` y ) <_ 0 <-> y = (/) ) )
63 lencl 
 |-  ( y e. Word V -> ( # ` y ) e. NN0 )
64 63 nn0red 
 |-  ( y e. Word V -> ( # ` y ) e. RR )
65 0re 
 |-  0 e. RR
66 lenlt 
 |-  ( ( ( # ` y ) e. RR /\ 0 e. RR ) -> ( ( # ` y ) <_ 0 <-> -. 0 < ( # ` y ) ) )
67 66 bicomd 
 |-  ( ( ( # ` y ) e. RR /\ 0 e. RR ) -> ( -. 0 < ( # ` y ) <-> ( # ` y ) <_ 0 ) )
68 64 65 67 sylancl 
 |-  ( y e. Word V -> ( -. 0 < ( # ` y ) <-> ( # ` y ) <_ 0 ) )
69 nne 
 |-  ( -. y =/= (/) <-> y = (/) )
70 69 a1i 
 |-  ( y e. Word V -> ( -. y =/= (/) <-> y = (/) ) )
71 62 68 70 3bitr4rd 
 |-  ( y e. Word V -> ( -. y =/= (/) <-> -. 0 < ( # ` y ) ) )
72 71 ad2antrr 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( -. y =/= (/) <-> -. 0 < ( # ` y ) ) )
73 72 con4bid 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y =/= (/) <-> 0 < ( # ` y ) ) )
74 61 73 mpbird 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> y =/= (/) )
75 55 74 jca 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y e. Word V /\ y =/= (/) ) )
76 75 ex 
 |-  ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
77 76 3adant3 
 |-  ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
78 54 77 syl 
 |-  ( ( y e. ( N WWalksN G ) /\ ( y ` 0 ) = P ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
79 52 78 sylbi 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
80 79 imp 
 |-  ( ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y e. Word V /\ y =/= (/) ) )
81 lswcl 
 |-  ( ( y e. Word V /\ y =/= (/) ) -> ( lastS ` y ) e. V )
82 80 81 syl 
 |-  ( ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( lastS ` y ) e. V )
83 82 ad2antrr 
 |-  ( ( ( ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K ) -> ( lastS ` y ) e. V )
84 preq1 
 |-  ( p = ( lastS ` y ) -> { p , n } = { ( lastS ` y ) , n } )
85 84 eleq1d 
 |-  ( p = ( lastS ` y ) -> ( { p , n } e. ( Edg ` G ) <-> { ( lastS ` y ) , n } e. ( Edg ` G ) ) )
86 85 rabbidv 
 |-  ( p = ( lastS ` y ) -> { n e. V | { p , n } e. ( Edg ` G ) } = { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } )
87 86 fveqeq2d 
 |-  ( p = ( lastS ` y ) -> ( ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K <-> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K ) )
88 87 rspcva 
 |-  ( ( ( lastS ` y ) e. V /\ A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K )
89 83 88 sylancom 
 |-  ( ( ( ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K )
90 89 exp41 
 |-  ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K ) ) ) )
91 90 com14 
 |-  ( A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K ) ) ) )
92 91 3ad2ant3 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. p e. V ( # ` { n e. V | { p , n } e. ( Edg ` G ) } ) = K ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K ) ) ) )
93 49 92 syl 
 |-  ( G RegUSGraph K -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K ) ) ) )
94 93 imp41 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ( Edg ` G ) } ) = K )
95 44 48 94 3eqtrd 
 |-  ( ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = K )
96 95 sumeq2dv 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } K )
97 oveq1 
 |-  ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) x. K ) = ( ( K ^ N ) x. K ) )
98 97 adantl 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) x. K ) = ( ( K ^ N ) x. K ) )
99 wwlksnfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )
100 29 99 sylbi 
 |-  ( V e. Fin -> ( N WWalksN G ) e. Fin )
101 100 3ad2ant1 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( N WWalksN G ) e. Fin )
102 101 ad2antlr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( N WWalksN G ) e. Fin )
103 rabfi 
 |-  ( ( N WWalksN G ) e. Fin -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin )
104 102 103 syl 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin )
105 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
106 simp1 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> V e. Fin )
107 105 106 anim12i 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( G e. USGraph /\ V e. Fin ) )
108 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
109 107 108 sylibr 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> G e. FinUSGraph )
110 simpl 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> G RegUSGraph K )
111 ne0i 
 |-  ( P e. V -> V =/= (/) )
112 111 3ad2ant2 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> V =/= (/) )
113 112 adantl 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> V =/= (/) )
114 1 frusgrnn0 
 |-  ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )
115 109 110 113 114 syl3anc 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> K e. NN0 )
116 115 nn0cnd 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> K e. CC )
117 116 adantr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> K e. CC )
118 fsumconst 
 |-  ( ( { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin /\ K e. CC ) -> sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } K = ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) x. K ) )
119 104 117 118 syl2anc 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } K = ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) x. K ) )
120 116 4 expp1d 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( K ^ ( N + 1 ) ) = ( ( K ^ N ) x. K ) )
121 120 adantr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( K ^ ( N + 1 ) ) = ( ( K ^ N ) x. K ) )
122 98 119 121 3eqtr4d 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } K = ( K ^ ( N + 1 ) ) )
123 96 122 eqtrd 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ( Edg ` G ) ) } ) = ( K ^ ( N + 1 ) ) )
124 16 40 123 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) )
125 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
126 125 3ad2ant3 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( N + 1 ) e. NN0 )
127 126 adantl 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( N + 1 ) e. NN0 )
128 1 2 rusgrnumwwlklem 
 |-  ( ( P e. V /\ ( N + 1 ) e. NN0 ) -> ( P L ( N + 1 ) ) = ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) )
129 128 eqeq1d 
 |-  ( ( P e. V /\ ( N + 1 ) e. NN0 ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
130 3 127 129 syl2anc 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
131 130 adantr 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
132 124 131 mpbird 
 |-  ( ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) )
133 132 ex 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) ) )
134 7 133 sylbid 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) ) )