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 ⊢ V = Vtx ⁡ G
Assertion numclwwlk4 ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → N ClWWalksN G = ∑ x ∈ V x ClWWalksNOn ⁡ G N

Proof

Step Hyp Ref Expression
1 numclwwlk3.v ⊢ V = Vtx ⁡ G
2 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
3 2 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → G ∈ USGraph
4 1 clwwlknun ⊢ G ∈ USGraph → N ClWWalksN G = ⋃ x ∈ V x ClWWalksNOn ⁡ G N
5 3 4 syl ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → N ClWWalksN G = ⋃ x ∈ V x ClWWalksNOn ⁡ G N
6 5 fveq2d ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → N ClWWalksN G = ⋃ x ∈ V x ClWWalksNOn ⁡ G N
7 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
8 7 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → V ∈ Fin
9 1 clwwlknonfin ⊢ V ∈ Fin → x ClWWalksNOn ⁡ G N ∈ Fin
10 7 9 syl ⊢ G ∈ FinUSGraph → x ClWWalksNOn ⁡ G N ∈ Fin
11 10 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → x ClWWalksNOn ⁡ G N ∈ Fin
12 11 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ ∧ x ∈ V → x ClWWalksNOn ⁡ G N ∈ Fin
13 clwwlknondisj ⊢ Disj x ∈ V x ClWWalksNOn ⁡ G N
14 13 a1i ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → Disj x ∈ V x ClWWalksNOn ⁡ G N
15 8 12 14 hashiun ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → ⋃ x ∈ V x ClWWalksNOn ⁡ G N = ∑ x ∈ V x ClWWalksNOn ⁡ G N
16 6 15 eqtrd ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ → N ClWWalksN G = ∑ x ∈ V x ClWWalksNOn ⁡ G N