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 ∈ 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 ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → A = K N − B

Proof

Step Hyp Ref Expression
1 clwwlknclwwlkdif.a ⊢ A = w ∈ 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 ∈ N WWalksN G | w ⁡ 0 = X = w ∈ N WWalksN G | w ⁡ 0 = X
5 1 2 4 clwwlknclwwlkdif ⊢ A = w ∈ N WWalksN G | w ⁡ 0 = X ∖ B
6 5 fveq2i ⊢ A = w ∈ N WWalksN G | w ⁡ 0 = X ∖ B
7 6 a1i ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → A = w ∈ N WWalksN G | w ⁡ 0 = X ∖ B
8 3 eleq1i ⊢ V ∈ Fin ↔ Vtx ⁡ G ∈ Fin
9 8 bilani ⊢ G RegUSGraph K ∧ V ∈ Fin → Vtx ⁡ G ∈ Fin
10 9 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin
11 wwlksnfi ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
12 rabfi ⊢ N WWalksN G ∈ Fin → w ∈ N WWalksN G | w ⁡ 0 = X ∈ Fin
13 10 11 12 3syl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X ∈ Fin
14 3 iswwlksnon ⊢ X N WWalksNOn G X = w ∈ 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 ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
17 14 16 eqtri ⊢ X N WWalksNOn G X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
18 17 a1i ⊢ X ∈ V ∧ N ∈ ℕ 0 → X N WWalksNOn G X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
19 2 18 eqtrid ⊢ X ∈ V ∧ N ∈ ℕ 0 → B = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
20 simpr ⊢ w ⁡ N = X ∧ w ⁡ 0 = X → w ⁡ 0 = X
21 20 a1i ⊢ w ∈ N WWalksN G → w ⁡ N = X ∧ w ⁡ 0 = X → w ⁡ 0 = X
22 21 ss2rabi ⊢ w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
23 19 22 eqsstrdi ⊢ X ∈ V ∧ N ∈ ℕ 0 → B ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
24 23 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → B ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
25 hashssdif ⊢ w ∈ N WWalksN G | w ⁡ 0 = X ∈ Fin ∧ B ⊆ w ∈ N WWalksN G | w ⁡ 0 = X → w ∈ N WWalksN G | w ⁡ 0 = X ∖ B = w ∈ N WWalksN G | w ⁡ 0 = X − B
26 13 24 25 syl2anc ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X ∖ B = w ∈ N WWalksN G | w ⁡ 0 = X − B
27 simpl ⊢ G RegUSGraph K ∧ V ∈ Fin → G RegUSGraph K
28 27 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → G RegUSGraph K
29 simpr ⊢ G RegUSGraph K ∧ V ∈ Fin → V ∈ Fin
30 29 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → V ∈ Fin
31 simpl ⊢ X ∈ V ∧ N ∈ ℕ 0 → X ∈ V
32 31 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → X ∈ V
33 simpr ⊢ X ∈ V ∧ N ∈ ℕ 0 → N ∈ ℕ 0
34 33 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → N ∈ ℕ 0
35 3 rusgrnumwwlkg ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X = K N
36 28 30 32 34 35 syl13anc ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X = K N
37 36 oveq1d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X − B = K N − B
38 7 26 37 3eqtrd ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → A = K N − B