Metamath Proof Explorer


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 ‘ 𝐺 ) 𝑁 ) ) )