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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	numclwwlk4	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
3	2	adantr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → 𝐺 ∈ USGraph )
4	1	clwwlknun	⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
5	3 4	syl	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
6	5	fveq2d	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
7	1	fusgrvtxfi	⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
8	7	adantr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → 𝑉 ∈ Fin )
9	1	clwwlknonfin	⊢ ( 𝑉 ∈ Fin → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
10	7 9	syl	⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
11	10	adantr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
12	11	adantr	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin )
13		clwwlknondisj	⊢ Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )
14	13	a1i	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
15	8 12 14	hashiun	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
16	6 15	eqtrd	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )