Metamath Proof Explorer


Theorem clwwlknclwwlkdif

Description: The set A of walks of length N starting with a fixed vertex V and ending not at this vertex is the difference between the set C of walks of length N starting with this vertex X and 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, 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
clwwlknclwwlkdif.c C = w N WWalksN G | w 0 = X
Assertion clwwlknclwwlkdif A = C 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 clwwlknclwwlkdif.c C = w N WWalksN G | w 0 = X
4 eqid Vtx G = Vtx G
5 4 iswwlksnon X N WWalksNOn G X = w N WWalksN G | w 0 = X w N = X
6 2 5 eqtri B = w N WWalksN G | w 0 = X w N = X
7 3 6 difeq12i C B = w N WWalksN G | w 0 = X w N WWalksN G | w 0 = X w N = X
8 difrab w N WWalksN G | w 0 = X w N WWalksN G | w 0 = X w N = X = w N WWalksN G | w 0 = X ¬ w 0 = X w N = X
9 annotanannot w 0 = X ¬ w 0 = X w N = X w 0 = X ¬ w N = X
10 df-ne w N X ¬ w N = X
11 wwlknlsw w N WWalksN G w N = lastS w
12 11 neeq1d w N WWalksN G w N X lastS w X
13 10 12 bitr3id w N WWalksN G ¬ w N = X lastS w X
14 13 anbi2d w N WWalksN G w 0 = X ¬ w N = X w 0 = X lastS w X
15 9 14 syl5bb w N WWalksN G w 0 = X ¬ w 0 = X w N = X w 0 = X lastS w X
16 15 rabbiia w N WWalksN G | w 0 = X ¬ w 0 = X w N = X = w N WWalksN G | w 0 = X lastS w X
17 7 8 16 3eqtrri w N WWalksN G | w 0 = X lastS w X = C B
18 1 17 eqtri A = C B