Metamath Proof Explorer


Theorem numclwwlk3lem2lem

Description: Lemma for numclwwlk3lem2 : The set of closed vertices of a fixed length N on a fixed vertex V is the union of the set 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 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 numclwwlk3lem2lem 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 2 numclwwlkovh0 X V N 2 X H N = w X ClWWalksNOn G N | w N 2 X
4 1 2clwwlk X V N 2 X C N = w X ClWWalksNOn G N | w N 2 = X
5 3 4 uneq12d 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
6 unrab 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
7 exmidne w N 2 = X w N 2 X
8 orcom w N 2 X w N 2 = X w N 2 = X w N 2 X
9 7 8 mpbir w N 2 X w N 2 = X
10 9 a1i w X ClWWalksNOn G N w N 2 X w N 2 = X
11 10 rabeqc w X ClWWalksNOn G N | w N 2 X w N 2 = X = X ClWWalksNOn G N
12 6 11 eqtri w X ClWWalksNOn G N | w N 2 X w X ClWWalksNOn G N | w N 2 = X = X ClWWalksNOn G N
13 5 12 eqtr2di X V N 2 X ClWWalksNOn G N = X H N X C N