Metamath Proof Explorer


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 ) } ) )