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 ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
Assertion numclwwlkqhash ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → 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 ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
3 1 2 numclwwlkovq ⊢ X ∈ V ∧ N ∈ ℕ → X Q N = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
4 3 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → X Q N = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
5 4 fveq2d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → X Q N = w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X
6 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
7 eqid ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X = w ∈ 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 ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X = K N − X N WWalksNOn G X
10 6 9 sylanr2 ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → w ∈ 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 ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X
12 wwlknlsw ⊢ w ∈ 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 ∈ N WWalksN G ∧ w ⁡ 0 = X → w ⁡ N = X ↔ lastS ⁡ w = w ⁡ 0
16 15 pm5.32da ⊢ w ∈ N WWalksN G → w ⁡ 0 = X ∧ w ⁡ N = X ↔ w ⁡ 0 = X ∧ lastS ⁡ w = w ⁡ 0
17 16 biancomd ⊢ w ∈ N WWalksN G → w ⁡ 0 = X ∧ w ⁡ N = X ↔ lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
18 17 rabbiia ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
19 11 18 eqtri ⊢ X N WWalksNOn G X = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
20 19 fveq2i ⊢ X N WWalksNOn G X = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
21 20 a1i ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → X N WWalksNOn G X = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
22 21 oveq2d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → K N − X N WWalksNOn G X = K N − w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
23 10 22 eqtrd ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G | w ⁡ 0 = X ∧ lastS ⁡ w ≠ X = K N − w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X
24 ovex ⊢ N WWalksN G ∈ V
25 24 rabex ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X ∈ V
26 clwwlkvbij ⊢ X ∈ V ∧ N ∈ ℕ → ∃ f f : w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X ⟶ 1-1 onto X ClWWalksNOn ⁡ G N
27 26 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → ∃ f f : w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X ⟶ 1-1 onto X ClWWalksNOn ⁡ G N
28 hasheqf1oi ⊢ w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X ∈ V → ∃ f f : w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X ⟶ 1-1 onto X ClWWalksNOn ⁡ G N → w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X = X ClWWalksNOn ⁡ G N
29 25 27 28 mpsyl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0 ∧ w ⁡ 0 = X = X ClWWalksNOn ⁡ G N
30 29 oveq2d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → K N − w ∈ 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 ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ → X Q N = K N − X ClWWalksNOn ⁡ G N