This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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