Metamath Proof Explorer

Theorem numclwwlkqhash

Description: In a K-regular graph, the size of the set of walks of length N starting with a fixed vertex X and ending not at this vertex is the difference between K to the power of N and the size of the set of closed walks of length N on vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 30-May-2021) (Revised by AV, 5-Mar-2022) (Proof shortened by AV, 7-Jul-2022)

Ref Expression
Hypotheses numclwwlk.v 
|- V = ( Vtx ` G )
numclwwlk.q 
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
Assertion numclwwlkqhash 
|- ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` ( X Q N ) ) = ( ( K ^ N ) - ( # ` ( X ( ClWWalksNOn ` G ) N ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 
 |-  V = ( Vtx ` G )
2 numclwwlk.q 
 |-  Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3 1 2 numclwwlkovq 
 |-  ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
4 3 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
5 4 fveq2d 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` ( X Q N ) ) = ( # ` { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
6 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
7 eqid 
 |-  { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
8 eqid 
 |-  ( X ( N WWalksNOn G ) X ) = ( X ( N WWalksNOn G ) X )
9 7 8 1 clwwlknclwwlkdifnum 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) = ( ( K ^ N ) - ( # ` ( X ( N WWalksNOn G ) X ) ) ) )
10 6 9 sylanr2 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) = ( ( K ^ N ) - ( # ` ( X ( N WWalksNOn G ) X ) ) ) )
11 1 iswwlksnon 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) }
12 wwlknlsw 
 |-  ( w e. ( N WWalksN G ) -> ( w ` N ) = ( lastS ` w ) )
13 eqcom 
 |-  ( ( w ` 0 ) = X <-> X = ( w ` 0 ) )
14 13 biimpi 
 |-  ( ( w ` 0 ) = X -> X = ( w ` 0 ) )
15 12 14 eqeqan12d 
 |-  ( ( w e. ( N WWalksN G ) /\ ( w ` 0 ) = X ) -> ( ( w ` N ) = X <-> ( lastS ` w ) = ( w ` 0 ) ) )
16 15 pm5.32da 
 |-  ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = X /\ ( w ` N ) = X ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) = ( w ` 0 ) ) ) )
17 16 biancomd 
 |-  ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = X /\ ( w ` N ) = X ) <-> ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) )
18 17 rabbiia 
 |-  { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) } = { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) }
19 11 18 eqtri 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) }
20 19 fveq2i 
 |-  ( # ` ( X ( N WWalksNOn G ) X ) ) = ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } )
21 20 a1i 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` ( X ( N WWalksNOn G ) X ) ) = ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) )
22 21 oveq2d 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( ( K ^ N ) - ( # ` ( X ( N WWalksNOn G ) X ) ) ) = ( ( K ^ N ) - ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) ) )
23 10 22 eqtrd 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) = ( ( K ^ N ) - ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) ) )
24 ovex 
 |-  ( N WWalksN G ) e. _V
25 24 rabex 
 |-  { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } e. _V
26 clwwlkvbij 
 |-  ( ( X e. V /\ N e. NN ) -> E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
27 26 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
28 hasheqf1oi 
 |-  ( { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } e. _V -> ( E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) -> ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) = ( # ` ( X ( ClWWalksNOn ` G ) N ) ) ) )
29 25 27 28 mpsyl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) = ( # ` ( X ( ClWWalksNOn ` G ) N ) ) )
30 29 oveq2d 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( ( K ^ N ) - ( # ` { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } ) ) = ( ( K ^ N ) - ( # ` ( X ( ClWWalksNOn ` G ) N ) ) ) )
31 5 23 30 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN ) ) -> ( # ` ( X Q N ) ) = ( ( K ^ N ) - ( # ` ( X ( ClWWalksNOn ` G ) N ) ) ) )