Theorem hashwwlksnext

Description: Number of walks (as words) extended by an edge as a sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnextprop.x	|- X = ( ( N + 1 ) WWalksN G )
	wwlksnextprop.e	|- E = ( Edg ` G )
	wwlksnextprop.y	|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
Assertion	hashwwlksnext	|- ( ( Vtx ` G ) e. Fin -> ( # ` { x e. X | E. y e. Y ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) = sum_ y e. Y ( # ` { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) )

Proof

Step	Hyp	Ref	Expression
1		wwlksnextprop.x	|- X = ( ( N + 1 ) WWalksN G )
2		wwlksnextprop.e	|- E = ( Edg ` G )
3		wwlksnextprop.y	|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
4		wwlksnfi	|- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )
5		ssrab2	|- { w e. ( N WWalksN G ) | ( w ` 0 ) = P } C_ ( N WWalksN G )
6		ssfi	|- ( ( ( N WWalksN G ) e. Fin /\ { w e. ( N WWalksN G ) | ( w ` 0 ) = P } C_ ( N WWalksN G ) ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin )
7	4 5 6	sylancl	|- ( ( Vtx ` G ) e. Fin -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } e. Fin )
8	3 7	eqeltrid	|- ( ( Vtx ` G ) e. Fin -> Y e. Fin )
9		wwlksnfi	|- ( ( Vtx ` G ) e. Fin -> ( ( N + 1 ) WWalksN G ) e. Fin )
10	1 9	eqeltrid	|- ( ( Vtx ` G ) e. Fin -> X e. Fin )
11		rabfi	|- ( X e. Fin -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin )
12	10 11	syl	|- ( ( Vtx ` G ) e. Fin -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin )
13	12	adantr	|- ( ( ( Vtx ` G ) e. Fin /\ y e. Y ) -> { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } e. Fin )
14	1 2 3	disjxwwlkn	|- Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }
15	14	a1i	|- ( ( Vtx ` G ) e. Fin -> Disj_ y e. Y { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } )
16	8 13 15	hashrabrex	|- ( ( Vtx ` G ) e. Fin -> ( # ` { x e. X | E. y e. Y ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) = sum_ y e. Y ( # ` { x e. X | ( ( x prefix M ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } ) )