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 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
Assertion numclwwlkqhash ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 1 2 numclwwlkovq ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
4 3 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
5 4 fveq2d ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) )
6 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
7 eqid { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) }
8 eqid ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 )
9 7 8 1 clwwlknclwwlkdifnum ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) )
10 6 9 sylanr2 ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) )
11 1 iswwlksnon ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤𝑁 ) = 𝑋 ) }
12 wwlknlsw ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤𝑁 ) = ( lastS ‘ 𝑤 ) )
13 eqcom ( ( 𝑤 ‘ 0 ) = 𝑋𝑋 = ( 𝑤 ‘ 0 ) )
14 13 biimpi ( ( 𝑤 ‘ 0 ) = 𝑋𝑋 = ( 𝑤 ‘ 0 ) )
15 12 14 eqeqan12d ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( ( 𝑤𝑁 ) = 𝑋 ↔ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) )
16 15 pm5.32da ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤𝑁 ) = 𝑋 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ) )
17 16 biancomd ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤𝑁 ) = 𝑋 ) ↔ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
18 17 rabbiia { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤𝑁 ) = 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
19 11 18 eqtri ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
20 19 fveq2i ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } )
21 20 a1i ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) )
22 21 oveq2d ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) )
23 10 22 eqtrd ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) )
24 ovex ( 𝑁 WWalksN 𝐺 ) ∈ V
25 24 rabex { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ∈ V
26 clwwlkvbij ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
27 26 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
28 hasheqf1oi ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ∈ V → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) )
29 25 27 28 mpsyl ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
30 29 oveq2d ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ( 𝐾𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) )
31 5 23 30 3eqtrd ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ( 𝐾𝑁 ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) )