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 biimpi ⊢ V ∈ Fin → Vtx ⁡ G ∈ Fin
10 9 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin → Vtx ⁡ G ∈ Fin
11 10 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin
12 wwlksnfi ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
13 rabfi ⊢ N WWalksN G ∈ Fin → w ∈ N WWalksN G | w ⁡ 0 = X ∈ Fin
14 11 12 13 3syl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X ∈ Fin
15 3 iswwlksnon ⊢ X N WWalksNOn G X = w ∈ 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 ∈ N WWalksN G | w ⁡ 0 = X ∧ w ⁡ N = X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
18 15 17 eqtri ⊢ X N WWalksNOn G X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
19 18 a1i ⊢ X ∈ V ∧ N ∈ ℕ 0 → X N WWalksNOn G X = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
20 2 19 syl5eq ⊢ X ∈ V ∧ N ∈ ℕ 0 → B = w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X
21 simpr ⊢ w ⁡ N = X ∧ w ⁡ 0 = X → w ⁡ 0 = X
22 21 a1i ⊢ w ∈ N WWalksN G → w ⁡ N = X ∧ w ⁡ 0 = X → w ⁡ 0 = X
23 22 ss2rabi ⊢ w ∈ N WWalksN G | w ⁡ N = X ∧ w ⁡ 0 = X ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
24 20 23 eqsstrdi ⊢ X ∈ V ∧ N ∈ ℕ 0 → B ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
25 24 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → B ⊆ w ∈ N WWalksN G | w ⁡ 0 = X
26 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
27 14 25 26 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
28 simpl ⊢ G RegUSGraph K ∧ V ∈ Fin → G RegUSGraph K
29 28 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → G RegUSGraph K
30 simpr ⊢ G RegUSGraph K ∧ V ∈ Fin → V ∈ Fin
31 30 adantr ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → V ∈ Fin
32 simpl ⊢ X ∈ V ∧ N ∈ ℕ 0 → X ∈ V
33 32 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → X ∈ V
34 simpr ⊢ X ∈ V ∧ N ∈ ℕ 0 → N ∈ ℕ 0
35 34 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → N ∈ ℕ 0
36 3 rusgrnumwwlkg ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X = K N
37 29 31 33 35 36 syl13anc ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X = K N
38 37 oveq1d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = X − B = K N − B
39 7 27 38 3eqtrd ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℕ 0 → A = K N − B