Theorem numclwwlk4

Description: The total number of closed walks in a finite simple graph is the sum of the numbers of closed walks starting at each of its vertices. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 2-Jun-2021) (Revised by AV, 7-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

	Ref	Expression
Hypothesis	numclwwlk3.v	|- V = ( Vtx ` G )
Assertion	numclwwlk4	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( # ` ( N ClWWalksN G ) ) = sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) N ) ) )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	|- V = ( Vtx ` G )
2		fusgrusgr	|- ( G e. FinUSGraph -> G e. USGraph )
3	2	adantr	|- ( ( G e. FinUSGraph /\ N e. NN ) -> G e. USGraph )
4	1	clwwlknun	|- ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x ( ClWWalksNOn ` G ) N ) )
5	3 4	syl	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( N ClWWalksN G ) = U_ x e. V ( x ( ClWWalksNOn ` G ) N ) )
6	5	fveq2d	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( # ` ( N ClWWalksN G ) ) = ( # ` U_ x e. V ( x ( ClWWalksNOn ` G ) N ) ) )
7	1	fusgrvtxfi	|- ( G e. FinUSGraph -> V e. Fin )
8	7	adantr	|- ( ( G e. FinUSGraph /\ N e. NN ) -> V e. Fin )
9	1	clwwlknonfin	|- ( V e. Fin -> ( x ( ClWWalksNOn ` G ) N ) e. Fin )
10	7 9	syl	|- ( G e. FinUSGraph -> ( x ( ClWWalksNOn ` G ) N ) e. Fin )
11	10	adantr	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( x ( ClWWalksNOn ` G ) N ) e. Fin )
12	11	adantr	|- ( ( ( G e. FinUSGraph /\ N e. NN ) /\ x e. V ) -> ( x ( ClWWalksNOn ` G ) N ) e. Fin )
13		clwwlknondisj	|- Disj_ x e. V ( x ( ClWWalksNOn ` G ) N )
14	13	a1i	|- ( ( G e. FinUSGraph /\ N e. NN ) -> Disj_ x e. V ( x ( ClWWalksNOn ` G ) N ) )
15	8 12 14	hashiun	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( # ` U_ x e. V ( x ( ClWWalksNOn ` G ) N ) ) = sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) N ) ) )
16	6 15	eqtrd	|- ( ( G e. FinUSGraph /\ N e. NN ) -> ( # ` ( N ClWWalksN G ) ) = sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) N ) ) )