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 ‘ 𝐺 ) 𝑁 ) ) ) )