Metamath Proof Explorer

Theorem clwwlknclwwlkdifnum

Description: In a K-regular graph, the size of the set A 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 B of closed walks of length N anchored at this vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 7-May-2021) (Revised by AV, 8-Mar-2022) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypotheses clwwlknclwwlkdif.a 
|- A = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
clwwlknclwwlkdif.b 
|- B = ( X ( N WWalksNOn G ) X )
clwwlknclwwlkdifnum.v 
|- V = ( Vtx ` G )
Assertion clwwlknclwwlkdifnum 
|- ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` A ) = ( ( K ^ N ) - ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 clwwlknclwwlkdif.a 
 |-  A = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) }
2 clwwlknclwwlkdif.b 
 |-  B = ( X ( N WWalksNOn G ) X )
3 clwwlknclwwlkdifnum.v 
 |-  V = ( Vtx ` G )
4 eqid 
 |-  { w e. ( N WWalksN G ) | ( w ` 0 ) = X } = { w e. ( N WWalksN G ) | ( w ` 0 ) = X }
5 1 2 4 clwwlknclwwlkdif 
 |-  A = ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B )
6 5 fveq2i 
 |-  ( # ` A ) = ( # ` ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B ) )
7 6 a1i 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` A ) = ( # ` ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B ) ) )
8 3 eleq1i 
 |-  ( V e. Fin <-> ( Vtx ` G ) e. Fin )
9 8 bilani 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> ( Vtx ` G ) e. Fin )
10 9 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( Vtx ` G ) e. Fin )
11 wwlksnfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )
12 rabfi 
 |-  ( ( N WWalksN G ) e. Fin -> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } e. Fin )
13 10 11 12 3syl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } e. Fin )
14 3 iswwlksnon 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) }
15 ancom 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` N ) = X ) <-> ( ( w ` N ) = X /\ ( w ` 0 ) = X ) )
16 15 rabbii 
 |-  { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) } = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) }
17 14 16 eqtri 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) }
18 17 a1i 
 |-  ( ( X e. V /\ N e. NN0 ) -> ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } )
19 2 18 eqtrid 
 |-  ( ( X e. V /\ N e. NN0 ) -> B = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } )
20 simpr 
 |-  ( ( ( w ` N ) = X /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X )
21 20 a1i 
 |-  ( w e. ( N WWalksN G ) -> ( ( ( w ` N ) = X /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X ) )
22 21 ss2rabi 
 |-  { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X }
23 19 22 eqsstrdi 
 |-  ( ( X e. V /\ N e. NN0 ) -> B C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
24 23 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> B C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
25 hashssdif 
 |-  ( ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } e. Fin /\ B C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) -> ( # ` ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B ) ) = ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) - ( # ` B ) ) )
26 13 24 25 syl2anc 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` ( { w e. ( N WWalksN G ) | ( w ` 0 ) = X } \ B ) ) = ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) - ( # ` B ) ) )
27 simpl 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G RegUSGraph K )
28 27 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> G RegUSGraph K )
29 simpr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> V e. Fin )
30 29 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> V e. Fin )
31 simpl 
 |-  ( ( X e. V /\ N e. NN0 ) -> X e. V )
32 31 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> X e. V )
33 simpr 
 |-  ( ( X e. V /\ N e. NN0 ) -> N e. NN0 )
34 33 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> N e. NN0 )
35 3 rusgrnumwwlkg 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ X e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) = ( K ^ N ) )
36 28 30 32 34 35 syl13anc 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) = ( K ^ N ) )
37 36 oveq1d 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) - ( # ` B ) ) = ( ( K ^ N ) - ( # ` B ) ) )
38 7 26 37 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` A ) = ( ( K ^ N ) - ( # ` B ) ) )