Metamath Proof Explorer


Theorem numclwwlk3lem2

Description: Lemma 1 for numclwwlk3 : The number of closed vertices of a fixed length N on a fixed vertex V is the sum of the number of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 1-Jun-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
numclwwlk3lem2.h H = v V , n 2 w v ClWWalksNOn G n | w n 2 v
Assertion numclwwlk3lem2 G FinUSGraph X V N 2 X ClWWalksNOn G N = X H N + X C N

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
2 numclwwlk3lem2.h H = v V , n 2 w v ClWWalksNOn G n | w n 2 v
3 1 2 numclwwlk3lem2lem X V N 2 X ClWWalksNOn G N = X H N X C N
4 3 adantll G FinUSGraph X V N 2 X ClWWalksNOn G N = X H N X C N
5 4 fveq2d G FinUSGraph X V N 2 X ClWWalksNOn G N = X H N X C N
6 2 numclwwlkovh0 X V N 2 X H N = w X ClWWalksNOn G N | w N 2 X
7 6 adantll G FinUSGraph X V N 2 X H N = w X ClWWalksNOn G N | w N 2 X
8 eqid Vtx G = Vtx G
9 8 fusgrvtxfi G FinUSGraph Vtx G Fin
10 9 ad2antrr G FinUSGraph X V N 2 Vtx G Fin
11 8 clwwlknonfin Vtx G Fin X ClWWalksNOn G N Fin
12 rabfi X ClWWalksNOn G N Fin w X ClWWalksNOn G N | w N 2 X Fin
13 10 11 12 3syl G FinUSGraph X V N 2 w X ClWWalksNOn G N | w N 2 X Fin
14 7 13 eqeltrd G FinUSGraph X V N 2 X H N Fin
15 1 2clwwlk X V N 2 X C N = w X ClWWalksNOn G N | w N 2 = X
16 15 adantll G FinUSGraph X V N 2 X C N = w X ClWWalksNOn G N | w N 2 = X
17 rabfi X ClWWalksNOn G N Fin w X ClWWalksNOn G N | w N 2 = X Fin
18 10 11 17 3syl G FinUSGraph X V N 2 w X ClWWalksNOn G N | w N 2 = X Fin
19 16 18 eqeltrd G FinUSGraph X V N 2 X C N Fin
20 7 16 ineq12d G FinUSGraph X V N 2 X H N X C N = w X ClWWalksNOn G N | w N 2 X w X ClWWalksNOn G N | w N 2 = X
21 inrab w X ClWWalksNOn G N | w N 2 X w X ClWWalksNOn G N | w N 2 = X = w X ClWWalksNOn G N | w N 2 X w N 2 = X
22 exmid w N 2 = X ¬ w N 2 = X
23 ianor ¬ w N 2 X w N 2 = X ¬ w N 2 X ¬ w N 2 = X
24 nne ¬ w N 2 X w N 2 = X
25 24 orbi1i ¬ w N 2 X ¬ w N 2 = X w N 2 = X ¬ w N 2 = X
26 23 25 bitri ¬ w N 2 X w N 2 = X w N 2 = X ¬ w N 2 = X
27 22 26 mpbir ¬ w N 2 X w N 2 = X
28 27 rgenw w X ClWWalksNOn G N ¬ w N 2 X w N 2 = X
29 rabeq0 w X ClWWalksNOn G N | w N 2 X w N 2 = X = w X ClWWalksNOn G N ¬ w N 2 X w N 2 = X
30 28 29 mpbir w X ClWWalksNOn G N | w N 2 X w N 2 = X =
31 21 30 eqtri w X ClWWalksNOn G N | w N 2 X w X ClWWalksNOn G N | w N 2 = X =
32 20 31 syl6eq G FinUSGraph X V N 2 X H N X C N =
33 hashun X H N Fin X C N Fin X H N X C N = X H N X C N = X H N + X C N
34 14 19 32 33 syl3anc G FinUSGraph X V N 2 X H N X C N = X H N + X C N
35 5 34 eqtrd G FinUSGraph X V N 2 X ClWWalksNOn G N = X H N + X C N