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∈NWWalksNG|w⁡0=X∧lastS⁡w≠X
clwwlknclwwlkdif.b ⊢B=XNWWalksNOnGX
clwwlknclwwlkdif.c ⊢C=w∈NWWalksNG|w⁡0=X
Assertion clwwlknclwwlkdif ⊢A=C∖B

Proof

Step Hyp Ref Expression
1 clwwlknclwwlkdif.a ⊢A=w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X
2 clwwlknclwwlkdif.b ⊢B=XNWWalksNOnGX
3 clwwlknclwwlkdif.c ⊢C=w∈NWWalksNG|w⁡0=X
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 4 iswwlksnon ⊢XNWWalksNOnGX=w∈NWWalksNG|w⁡0=X∧w⁡N=X
6 2 5 eqtri ⊢B=w∈NWWalksNG|w⁡0=X∧w⁡N=X
7 3 6 difeq12i ⊢C∖B=w∈NWWalksNG|w⁡0=X∖w∈NWWalksNG|w⁡0=X∧w⁡N=X
8 difrab ⊢w∈NWWalksNG|w⁡0=X∖w∈NWWalksNG|w⁡0=X∧w⁡N=X=w∈NWWalksNG|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∈NWWalksNG→w⁡N=lastS⁡w
12 11 neeq1d ⊢w∈NWWalksNG→w⁡N≠X↔lastS⁡w≠X
13 10 12 bitr3id ⊢w∈NWWalksNG→¬w⁡N=X↔lastS⁡w≠X
14 13 anbi2d ⊢w∈NWWalksNG→w⁡0=X∧¬w⁡N=X↔w⁡0=X∧lastS⁡w≠X
15 9 14 bitrid ⊢w∈NWWalksNG→w⁡0=X∧¬w⁡0=X∧w⁡N=X↔w⁡0=X∧lastS⁡w≠X
16 15 rabbiia ⊢w∈NWWalksNG|w⁡0=X∧¬w⁡0=X∧w⁡N=X=w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X
17 7 8 16 3eqtrri ⊢w∈NWWalksNG|w⁡0=X∧lastS⁡w≠X=C∖B
18 1 17 eqtri ⊢A=C∖B