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 \in FinUSGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \sum_{x \in V} \|x ClWWalksNOn (G) N\|$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	$⊢ V = Vtx (G)$
2		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
3	2	adantr	$⊢ (G \in FinUSGraph \land N \in ℕ) \to G \in USGraph$
4	1	clwwlknun	$⊢ G \in USGraph \to N ClWWalksN G = ⋃_{x \in V} (x ClWWalksNOn (G) N)$
5	3 4	syl	$⊢ (G \in FinUSGraph \land N \in ℕ) \to N ClWWalksN G = ⋃_{x \in V} (x ClWWalksNOn (G) N)$
6	5	fveq2d	$⊢ (G \in FinUSGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \|⋃_{x \in V} (x ClWWalksNOn (G) N)\|$
7	1	fusgrvtxfi	$⊢ G \in FinUSGraph \to V \in Fin$
8	7	adantr	$⊢ (G \in FinUSGraph \land N \in ℕ) \to V \in Fin$
9	1	clwwlknonfin	$⊢ V \in Fin \to x ClWWalksNOn (G) N \in Fin$
10	7 9	syl	$⊢ G \in FinUSGraph \to x ClWWalksNOn (G) N \in Fin$
11	10	adantr	$⊢ (G \in FinUSGraph \land N \in ℕ) \to x ClWWalksNOn (G) N \in Fin$
12	11	adantr	$⊢ ((G \in FinUSGraph \land N \in ℕ) \land x \in V) \to x ClWWalksNOn (G) N \in Fin$
13		clwwlknondisj	$⊢ \underset{x \in V}{Disj} (x ClWWalksNOn (G) N)$
14	13	a1i	$⊢ (G \in FinUSGraph \land N \in ℕ) \to \underset{x \in V}{Disj} (x ClWWalksNOn (G) N)$
15	8 12 14	hashiun	$⊢ (G \in FinUSGraph \land N \in ℕ) \to \|⋃_{x \in V} (x ClWWalksNOn (G) N)\| = \sum_{x \in V} \|x ClWWalksNOn (G) N\|$
16	6 15	eqtrd	$⊢ (G \in FinUSGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \sum_{x \in V} \|x ClWWalksNOn (G) N\|$

Metamath Proof Explorer

Theorem numclwwlk4

Proof