Theorem rusgranumwlks 30600

Description: Induction step for rusgranumwlk 30601. (Contributed by Alexander van der Vekens, 24-Aug-2018.)

Hypotheses

Ref	Expression
rusgranumwlk.w	|- W = ( n e. NN0 |-> { c e. ( V Walks E ) | ( # ` ( 1st ` c ) ) = n } )
rusgranumwlk.l	|- L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( W ` n ) | ( ( 2nd ` w ) ` 0 ) = v } ) )

Assertion

Ref	Expression
rusgranumwlks	|- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) ) )

Distinct variable groups:   E, c, n   N, c, n   V, c, n   v, N, w   P, n, v, w   v, V   n, W, v, w   w, V, c   v, E, w   w, K

Allowed substitution hints:   P( c)   K( v, n, c)   L( w, v, n, c)   W( c)

Proof of Theorem rusgranumwlks

Dummy variables i p y x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rusisusgra 30574	. . . 4 |- ( <. V , E >. RegUSGrph K -> V USGrph E )
2	1	adantr 465	. . 3 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> V USGrph E )
3		simpr2 995	. . 3 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> P e. V )
4		simp3 990	. . . 4 |- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> N e. NN0 )
5	4	adantl 466	. . 3 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> N e. NN0 )
6		rusgranumwlk.w	. . . . 5 |- W = ( n e. NN0 |-> { c e. ( V Walks E ) | ( # ` ( 1st ` c ) ) = n } )
7		rusgranumwlk.l	. . . . 5 |- L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( W ` n ) | ( ( 2nd ` w ) ` 0 ) = v } ) )
8	6, 7	rusgranumwlklem4 30596	. . . 4 |- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> ( P L N ) = ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) )
9	8	eqeq1d 2451	. . 3 |- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> ( ( P L N ) = ( K ^ N ) <-> ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) )
10	2, 3, 5, 9	syl3anc 1218	. 2 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) <-> ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) )
11		wwlknredwwlkn0 30385	. . . . . . . . . . . 12 |- ( ( N e. NN0 /\ w e. ( ( V WWalksN E ) ` ( N + 1 ) ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) )
12	11	ex 434	. . . . . . . . . . 11 |- ( N e. NN0 -> ( w e. ( ( V WWalksN E ) ` ( N + 1 ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) ) )
13	12	3ad2ant3 1011	. . . . . . . . . 10 |- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( w e. ( ( V WWalksN E ) ` ( N + 1 ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) ) )
14	13	adantl 466	. . . . . . . . 9 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( w e. ( ( V WWalksN E ) ` ( N + 1 ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) ) )
15	14	imp 429	. . . . . . . 8 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( V WWalksN E ) ` ( N + 1 ) ) ) -> ( ( w ` 0 ) = P <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) )
16	15	rabbidva 2984	. . . . . . 7 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
17	16	adantr 465	. . . . . 6 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
18	17	fveq2d 5716	. . . . 5 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) = ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
19		simp2 989	. . . . . . . . . . . . 13 |- ( ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) -> ( y ` 0 ) = P )
20	19	pm4.71ri 633	. . . . . . . . . . . 12 |- ( ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) <-> ( ( y ` 0 ) = P /\ ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) )
21	20	a1i 11	. . . . . . . . . . 11 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( V WWalksN E ) ` ( N + 1 ) ) ) /\ y e. ( ( V WWalksN E ) ` N ) ) -> ( ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) <-> ( ( y ` 0 ) = P /\ ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) ) )
22	21	rexbidva 2753	. . . . . . . . . 10 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( V WWalksN E ) ` ( N + 1 ) ) ) -> ( E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( y ` 0 ) = P /\ ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) ) )
23		fveq1 5711	. . . . . . . . . . . 12 |- ( x = y -> ( x ` 0 ) = ( y ` 0 ) )
24	23	eqeq1d 2451	. . . . . . . . . . 11 |- ( x = y -> ( ( x ` 0 ) = P <-> ( y ` 0 ) = P ) )
25	24	rexrab 3144	. . . . . . . . . 10 |- ( E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) <-> E. y e. ( ( V WWalksN E ) ` N ) ( ( y ` 0 ) = P /\ ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) )
26	22, 25	syl6bbr 263	. . . . . . . . 9 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ w e. ( ( V WWalksN E ) ` ( N + 1 ) ) ) -> ( E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) <-> E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) ) )
27	26	rabbidva 2984	. . . . . . . 8 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
28	27	adantr 465	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
29	28	fveq2d 5716	. . . . . 6 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
30		simplr1 1030	. . . . . . . 8 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> V e. Fin )
31		eqid 2443	. . . . . . . . 9 |- ( ( V WWalksN E ) ` ( N + 1 ) ) = ( ( V WWalksN E ) ` ( N + 1 ) )
32		eqid 2443	. . . . . . . . 9 |- { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } = { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P }
33	31, 32	hashwwlkext 30591	. . . . . . . 8 |- ( V e. Fin -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
34	30, 33	syl 16	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
35		fveq1 5711	. . . . . . . . . . 11 |- ( x = w -> ( x ` 0 ) = ( w ` 0 ) )
36	35	eqeq1d 2451	. . . . . . . . . 10 |- ( x = w -> ( ( x ` 0 ) = P <-> ( w ` 0 ) = P ) )
37	36	cbvrabv 2992	. . . . . . . . 9 |- { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }
38	37	sumeq1i 13196	. . . . . . . 8 |- sum_ y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
39	38	a1i 11	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
40	34, 39	eqtrd 2475	. . . . . 6 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. { x e. ( ( V WWalksN E ) ` N ) | ( x ` 0 ) = P } ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
41	29, 40	eqtrd 2475	. . . . 5 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | E. y e. ( ( V WWalksN E ) ` N ) ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
42		rusgranumwlklem0 30592	. . . . . . . . . . . 12 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
43	42	eqcomd 2448	. . . . . . . . . . 11 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } = { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } )
44	43	fveq2d 5716	. . . . . . . . . 10 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
45	44	adantl 466	. . . . . . . . 9 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) )
46		fveq1 5711	. . . . . . . . . . . . . 14 |- ( w = y -> ( w ` 0 ) = ( y ` 0 ) )
47	46	eqeq1d 2451	. . . . . . . . . . . . 13 |- ( w = y -> ( ( w ` 0 ) = P <-> ( y ` 0 ) = P ) )
48	47	elrab 3138	. . . . . . . . . . . 12 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } <-> ( y e. ( ( V WWalksN E ) ` N ) /\ ( y ` 0 ) = P ) )
49	48	simplbi 460	. . . . . . . . . . 11 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> y e. ( ( V WWalksN E ) ` N ) )
50	49	adantl 466	. . . . . . . . . 10 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) -> y e. ( ( V WWalksN E ) ` N ) )
51		wwlkexthasheq 30392	. . . . . . . . . 10 |- ( y e. ( ( V WWalksN E ) ` N ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) )
52	50, 51	syl 16	. . . . . . . . 9 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) )
53		rusgraprop3 30581	. . . . . . . . . . 11 |- ( <. V , E >. RegUSGrph K -> ( V USGrph E /\ K e. NN0 /\ A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K ) )
54		wwlknimp 30347	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( V WWalksN E ) ` N ) -> ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ran E ) )
55	54	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. ( ( V WWalksN E ) ` N ) /\ ( y ` 0 ) = P ) -> ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ran E ) )
56		simpll 753	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> y e. Word V )
57		nn0re 10609	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. NN0 -> N e. RR )
58		1re 9406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 1 e. RR
59	58	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. NN0 -> 1 e. RR )
60		nn0ge0 10626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. NN0 -> 0 <_ N )
61		0lt1 9883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 0 < 1
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. NN0 -> 0 < 1 )
63	57, 59, 60, 62	addgegt0d 9934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( N e. NN0 -> 0 < ( N + 1 ) )
64	63	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> 0 < ( N + 1 ) )
65	64	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> 0 < ( N + 1 ) )
66		breq2 4317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( # ` y ) = ( N + 1 ) -> ( 0 < ( # ` y ) <-> 0 < ( N + 1 ) ) )
67	66	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` y ) <-> 0 < ( N + 1 ) ) )
68	65, 67	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> 0 < ( # ` y ) )
69		hashle00 12179	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. Word V -> ( ( # ` y ) <_ 0 <-> y = (/) ) )
70		lencl 12270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y e. Word V -> ( # ` y ) e. NN0 )
71	70	nn0red 10658	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y e. Word V -> ( # ` y ) e. RR )
72		0re 9407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 0 e. RR
73		lenlt 9474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( # ` y ) e. RR /\ 0 e. RR ) -> ( ( # ` y ) <_ 0 <-> -. 0 < ( # ` y ) ) )
74	73	bicomd 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( # ` y ) e. RR /\ 0 e. RR ) -> ( -. 0 < ( # ` y ) <-> ( # ` y ) <_ 0 ) )
75	71, 72, 74	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. Word V -> ( -. 0 < ( # ` y ) <-> ( # ` y ) <_ 0 ) )
76		nne 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. y =/= (/) <-> y = (/) )
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. Word V -> ( -. y =/= (/) <-> y = (/) ) )
78	69, 75, 77	3bitr4rd 286	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. Word V -> ( -. y =/= (/) <-> -. 0 < ( # ` y ) ) )
79	78	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( -. y =/= (/) <-> -. 0 < ( # ` y ) ) )
80	79	con4bid 293	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y =/= (/) <-> 0 < ( # ` y ) ) )
81	68, 80	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> y =/= (/) )
82	56, 81	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y e. Word V /\ y =/= (/) ) )
83	82	ex 434	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
84	83	3adant3 1008	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. Word V /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ran E ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
85	55, 84	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( ( V WWalksN E ) ` N ) /\ ( y ` 0 ) = P ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
86	48, 85	sylbi 195	. . . . . . . . . . . . . . . . . 18 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( y e. Word V /\ y =/= (/) ) ) )
87	86	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( y e. Word V /\ y =/= (/) ) )
88		lswcl 12291	. . . . . . . . . . . . . . . . 17 |- ( ( y e. Word V /\ y =/= (/) ) -> ( lastS ` y ) e. V )
89	87, 88	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( lastS ` y ) e. V )
90	89	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K ) -> ( lastS ` y ) e. V )
91		preq1 3975	. . . . . . . . . . . . . . . . . . . 20 |- ( p = ( lastS ` y ) -> { p , n } = { ( lastS ` y ) , n } )
92	91	eleq1d 2509	. . . . . . . . . . . . . . . . . . 19 |- ( p = ( lastS ` y ) -> ( { p , n } e. ran E <-> { ( lastS ` y ) , n } e. ran E ) )
93	92	rabbidv 2985	. . . . . . . . . . . . . . . . . 18 |- ( p = ( lastS ` y ) -> { n e. V | { p , n } e. ran E } = { n e. V | { ( lastS ` y ) , n } e. ran E } )
94	93	fveq2d 5716	. . . . . . . . . . . . . . . . 17 |- ( p = ( lastS ` y ) -> ( # ` { n e. V | { p , n } e. ran E } ) = ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) )
95	94	eqeq1d 2451	. . . . . . . . . . . . . . . 16 |- ( p = ( lastS ` y ) -> ( ( # ` { n e. V | { p , n } e. ran E } ) = K <-> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K ) )
96	95	rspcva 3092	. . . . . . . . . . . . . . 15 |- ( ( ( lastS ` y ) e. V /\ A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K )
97	90, 96	sylancom 667	. . . . . . . . . . . . . 14 |- ( ( ( ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K )
98	97	exp41 610	. . . . . . . . . . . . 13 |- ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K ) ) ) )
99	98	com14 88	. . . . . . . . . . . 12 |- ( A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K ) ) ) )
100	99	3ad2ant3 1011	. . . . . . . . . . 11 |- ( ( V USGrph E /\ K e. NN0 /\ A. p e. V ( # ` { n e. V | { p , n } e. ran E } ) = K ) -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K ) ) ) )
101	53, 100	syl 16	. . . . . . . . . 10 |- ( <. V , E >. RegUSGrph K -> ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K ) ) ) )
102	101	imp41 593	. . . . . . . . 9 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) -> ( # ` { n e. V | { ( lastS ` y ) , n } e. ran E } ) = K )
103	45, 52, 102	3eqtrd 2479	. . . . . . . 8 |- ( ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) /\ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = K )
104	103	ralrimiva 2820	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> A. y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = K )
105	104	sumeq2d 13200	. . . . . 6 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } K )
106		oveq1 6119	. . . . . . . 8 |- ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) x. K ) = ( ( K ^ N ) x. K ) )
107	106	adantl 466	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) x. K ) = ( ( K ^ N ) x. K ) )
108		wwlknfi 30396	. . . . . . . . . . 11 |- ( V e. Fin -> ( ( V WWalksN E ) ` N ) e. Fin )
109	108	3ad2ant1 1009	. . . . . . . . . 10 |- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( ( V WWalksN E ) ` N ) e. Fin )
110	109	ad2antlr 726	. . . . . . . . 9 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( ( V WWalksN E ) ` N ) e. Fin )
111		rabfi 7558	. . . . . . . . 9 |- ( ( ( V WWalksN E ) ` N ) e. Fin -> { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } e. Fin )
112	110, 111	syl 16	. . . . . . . 8 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } e. Fin )
113		rusgraprop 30572	. . . . . . . . . 10 |- ( <. V , E >. RegUSGrph K -> ( V USGrph E /\ K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) )
114		nn0cn 10610	. . . . . . . . . . 11 |- ( K e. NN0 -> K e. CC )
115	114	3ad2ant2 1010	. . . . . . . . . 10 |- ( ( V USGrph E /\ K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) -> K e. CC )
116	113, 115	syl 16	. . . . . . . . 9 |- ( <. V , E >. RegUSGrph K -> K e. CC )
117	116	ad2antrr 725	. . . . . . . 8 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> K e. CC )
118		fsumconst 13278	. . . . . . . 8 |- ( ( { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } e. Fin /\ K e. CC ) -> sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } K = ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) x. K ) )
119	112, 117, 118	syl2anc 661	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } K = ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) x. K ) )
120		expp1 11893	. . . . . . . . 9 |- ( ( K e. CC /\ N e. NN0 ) -> ( K ^ ( N + 1 ) ) = ( ( K ^ N ) x. K ) )
121	116, 4, 120	syl2an 477	. . . . . . . 8 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( K ^ ( N + 1 ) ) = ( ( K ^ N ) x. K ) )
122	121	adantr 465	. . . . . . 7 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( K ^ ( N + 1 ) ) = ( ( K ^ N ) x. K ) )
123	107, 119, 122	3eqtr4d 2485	. . . . . 6 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } K = ( K ^ ( N + 1 ) ) )
124	105, 123	eqtrd 2475	. . . . 5 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> sum_ y e. { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` w ) } e. ran E ) } ) = ( K ^ ( N + 1 ) ) )
125	18, 41, 124	3eqtrd 2479	. . . 4 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) )
126		peano2nn0 10641	. . . . . . . 8 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
127	126	3ad2ant3 1011	. . . . . . 7 |- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( N + 1 ) e. NN0 )
128	127	adantl 466	. . . . . 6 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( N + 1 ) e. NN0 )
129	6, 7	rusgranumwlklem4 30596	. . . . . . 7 |- ( ( V USGrph E /\ P e. V /\ ( N + 1 ) e. NN0 ) -> ( P L ( N + 1 ) ) = ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) )
130	129	eqeq1d 2451	. . . . . 6 |- ( ( V USGrph E /\ P e. V /\ ( N + 1 ) e. NN0 ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
131	2, 3, 128, 130	syl3anc 1218	. . . . 5 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
132	131	adantr 465	. . . 4 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) <-> ( # ` { w e. ( ( V WWalksN E ) ` ( N + 1 ) ) | ( w ` 0 ) = P } ) = ( K ^ ( N + 1 ) ) ) )
133	125, 132	mpbird 232	. . 3 |- ( ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) /\ ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) )
134	133	ex 434	. 2 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( # ` { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) ) )
135	10, 134	sylbid 215	1 |- ( ( <. V , E >. RegUSGrph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( ( P L N ) = ( K ^ N ) -> ( P L ( N + 1 ) ) = ( K ^ ( N + 1 ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2620   A.wral 2736   E.wrex 2737   {crab 2740   (/)c0 3658   {cpr 3900   <.cop 3904   class class class wbr 4313   e. cmpt 4371   ran crn 4862   ` cfv 5439  (class class class)co 6112   e. cmpt2 6114   1stc1st 6596   2ndc2nd 6597   Fincfn 7331   CCcc 9301   RRcr 9302   0cc0 9303   1c1 9304   + caddc 9306   x. cmul 9308   < clt 9439   <_ cle 9440   NN0cn0 10600  ..^cfzo 11569   ^cexp 11886   #chash 12124  Word cword 12242   lastS clsw 12243   substr csubstr 12246   sum_csu 13184   USGrph cusg 23286   Walks cwalk 23427   VDeg cvdg 23585   WWalksN cwwlkn 30338   RegUSGrph crusgra 30566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-disj 4284  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-pm 7238  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-sup 7712  df-oi 7745  df-card 8130  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-n0 10601  df-z 10668  df-uz 10883  df-rp 11013  df-xadd 11111  df-fz 11459  df-fzo 11570  df-seq 11828  df-exp 11887  df-hash 12125  df-word 12250  df-lsw 12251  df-concat 12252  df-s1 12253  df-substr 12254  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-clim 12987  df-sum 13185  df-usgra 23288  df-nbgra 23354  df-wlk 23437  df-vdgr 23586  df-wwlk 30339  df-wwlkn 30340  df-rgra 30567  df-rusgra 30568

This theorem is referenced by:  rusgranumwlk  30601