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 biimpi 
 |-  ( V e. Fin -> ( Vtx ` G ) e. Fin )
10 9 adantl 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> ( Vtx ` G ) e. Fin )
11 10 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( Vtx ` G ) e. Fin )
12 wwlksnfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )
13 rabfi 
 |-  ( ( N WWalksN G ) e. Fin -> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } e. Fin )
14 11 12 13 3syl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } e. Fin )
15 3 iswwlksnon 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) }
16 ancom 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` N ) = X ) <-> ( ( w ` N ) = X /\ ( w ` 0 ) = X ) )
17 16 rabbii 
 |-  { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` N ) = X ) } = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) }
18 15 17 eqtri 
 |-  ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) }
19 18 a1i 
 |-  ( ( X e. V /\ N e. NN0 ) -> ( X ( N WWalksNOn G ) X ) = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } )
20 2 19 syl5eq 
 |-  ( ( X e. V /\ N e. NN0 ) -> B = { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } )
21 simpr 
 |-  ( ( ( w ` N ) = X /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X )
22 21 a1i 
 |-  ( w e. ( N WWalksN G ) -> ( ( ( w ` N ) = X /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X ) )
23 22 ss2rabi 
 |-  { w e. ( N WWalksN G ) | ( ( w ` N ) = X /\ ( w ` 0 ) = X ) } C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X }
24 20 23 eqsstrdi 
 |-  ( ( X e. V /\ N e. NN0 ) -> B C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
25 24 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> B C_ { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
26 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 ) ) )
27 14 25 26 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 ) ) )
28 simpl 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G RegUSGraph K )
29 28 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> G RegUSGraph K )
30 simpr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> V e. Fin )
31 30 adantr 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> V e. Fin )
32 simpl 
 |-  ( ( X e. V /\ N e. NN0 ) -> X e. V )
33 32 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> X e. V )
34 simpr 
 |-  ( ( X e. V /\ N e. NN0 ) -> N e. NN0 )
35 34 adantl 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> N e. NN0 )
36 3 rusgrnumwwlkg 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ X e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) = ( K ^ N ) )
37 29 31 33 35 36 syl13anc 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) = ( K ^ N ) )
38 37 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 ) ) )
39 7 27 38 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ N e. NN0 ) ) -> ( # ` A ) = ( ( K ^ N ) - ( # ` B ) ) )