# 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}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
numclwwlk3lem2.h ${⊢}{H}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)\ne {v}\right\}\right)$
Assertion numclwwlk3lem2 ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left|{X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right|=\left|{X}{H}{N}\right|+\left|{X}{C}{N}\right|$

### Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
2 numclwwlk3lem2.h ${⊢}{H}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)\ne {v}\right\}\right)$
3 1 2 numclwwlk3lem2lem ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}\mathrm{ClWWalksNOn}\left({G}\right){N}=\left({X}{H}{N}\right)\cup \left({X}{C}{N}\right)$
4 3 adantll ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}\mathrm{ClWWalksNOn}\left({G}\right){N}=\left({X}{H}{N}\right)\cup \left({X}{C}{N}\right)$
5 4 fveq2d ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left|{X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right|=\left|\left({X}{H}{N}\right)\cup \left({X}{C}{N}\right)\right|$
6 2 numclwwlkovh0 ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{H}{N}=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}$
7 6 adantll ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{H}{N}=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}$
8 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
9 8 fusgrvtxfi ${⊢}{G}\in \mathrm{FinUSGraph}\to \mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}$
10 9 ad2antrr ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}$
11 8 clwwlknonfin ${⊢}\mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}\to {X}\mathrm{ClWWalksNOn}\left({G}\right){N}\in \mathrm{Fin}$
12 rabfi ${⊢}{X}\mathrm{ClWWalksNOn}\left({G}\right){N}\in \mathrm{Fin}\to \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}\in \mathrm{Fin}$
13 10 11 12 3syl ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}\in \mathrm{Fin}$
14 7 13 eqeltrd ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{H}{N}\in \mathrm{Fin}$
15 1 2clwwlk ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{C}{N}=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}$
16 15 adantll ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{C}{N}=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}$
17 rabfi ${⊢}{X}\mathrm{ClWWalksNOn}\left({G}\right){N}\in \mathrm{Fin}\to \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}\in \mathrm{Fin}$
18 10 11 17 3syl ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}\in \mathrm{Fin}$
19 16 18 eqeltrd ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to {X}{C}{N}\in \mathrm{Fin}$
20 7 16 ineq12d ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({X}{H}{N}\right)\cap \left({X}{C}{N}\right)=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}\cap \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}$
21 inrab ${⊢}\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}\cap \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}=\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)\right\}$
22 exmid ${⊢}\left({w}\left({N}-2\right)={X}\vee ¬{w}\left({N}-2\right)={X}\right)$
23 ianor ${⊢}¬\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)↔\left(¬{w}\left({N}-2\right)\ne {X}\vee ¬{w}\left({N}-2\right)={X}\right)$
24 nne ${⊢}¬{w}\left({N}-2\right)\ne {X}↔{w}\left({N}-2\right)={X}$
25 24 orbi1i ${⊢}\left(¬{w}\left({N}-2\right)\ne {X}\vee ¬{w}\left({N}-2\right)={X}\right)↔\left({w}\left({N}-2\right)={X}\vee ¬{w}\left({N}-2\right)={X}\right)$
26 23 25 bitri ${⊢}¬\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)↔\left({w}\left({N}-2\right)={X}\vee ¬{w}\left({N}-2\right)={X}\right)$
27 22 26 mpbir ${⊢}¬\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)$
28 27 rgenw ${⊢}\forall {w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\phantom{\rule{.4em}{0ex}}¬\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)$
29 rabeq0 ${⊢}\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)\right\}=\varnothing ↔\forall {w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\phantom{\rule{.4em}{0ex}}¬\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)$
30 28 29 mpbir ${⊢}\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|\left({w}\left({N}-2\right)\ne {X}\wedge {w}\left({N}-2\right)={X}\right)\right\}=\varnothing$
31 21 30 eqtri ${⊢}\left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)\ne {X}\right\}\cap \left\{{w}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)|{w}\left({N}-2\right)={X}\right\}=\varnothing$
32 20 31 syl6eq ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({X}{H}{N}\right)\cap \left({X}{C}{N}\right)=\varnothing$
33 hashun ${⊢}\left({X}{H}{N}\in \mathrm{Fin}\wedge {X}{C}{N}\in \mathrm{Fin}\wedge \left({X}{H}{N}\right)\cap \left({X}{C}{N}\right)=\varnothing \right)\to \left|\left({X}{H}{N}\right)\cup \left({X}{C}{N}\right)\right|=\left|{X}{H}{N}\right|+\left|{X}{C}{N}\right|$
34 14 19 32 33 syl3anc ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left|\left({X}{H}{N}\right)\cup \left({X}{C}{N}\right)\right|=\left|{X}{H}{N}\right|+\left|{X}{C}{N}\right|$
35 5 34 eqtrd ${⊢}\left(\left({G}\in \mathrm{FinUSGraph}\wedge {X}\in {V}\right)\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left|{X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right|=\left|{X}{H}{N}\right|+\left|{X}{C}{N}\right|$