Metamath Proof Explorer

Theorem numclwwlk3lem2

Description: Lemma 1 for numclwwlk3 : The number of closed vertices of a fixed length N on a fixed vertex V is the sum of the number of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 1-Jun-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
numclwwlk3lem2.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
Assertion numclwwlk3lem2 ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N + X C N

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
2 numclwwlk3lem2.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
3 1 2 numclwwlk3lem2lem ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N ∪ X C N
4 3 adantll ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N ∪ X C N
5 4 fveq2d ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N ∪ X C N
6 2 numclwwlkovh0 ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X
7 6 adantll ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X
8 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
9 8 fusgrvtxfi ⊢ G ∈ FinUSGraph → Vtx ⁡ G ∈ Fin
10 9 ad2antrr ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → Vtx ⁡ G ∈ Fin
11 8 clwwlknonfin ⊢ Vtx ⁡ G ∈ Fin → X ClWWalksNOn ⁡ G N ∈ Fin
12 rabfi ⊢ X ClWWalksNOn ⁡ G N ∈ Fin → w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∈ Fin
13 10 11 12 3syl ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∈ Fin
14 7 13 eqeltrd ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N ∈ Fin
15 1 2clwwlk ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
16 15 adantll ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
17 rabfi ⊢ X ClWWalksNOn ⁡ G N ∈ Fin → w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X ∈ Fin
18 10 11 17 3syl ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X ∈ Fin
19 16 18 eqeltrd ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N ∈ Fin
20 7 16 ineq12d ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N ∩ X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∩ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
21 inrab ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∩ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X
22 exmid ⊢ w ⁡ N − 2 = X ∨ ¬ w ⁡ N − 2 = X
23 ianor ⊢ ¬ w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X ↔ ¬ w ⁡ N − 2 ≠ X ∨ ¬ w ⁡ N − 2 = X
24 nne ⊢ ¬ w ⁡ N − 2 ≠ X ↔ w ⁡ N − 2 = X
25 24 orbi1i ⊢ ¬ w ⁡ N − 2 ≠ X ∨ ¬ w ⁡ N − 2 = X ↔ w ⁡ N − 2 = X ∨ ¬ w ⁡ N − 2 = X
26 23 25 bitri ⊢ ¬ w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X ↔ w ⁡ N − 2 = X ∨ ¬ w ⁡ N − 2 = X
27 22 26 mpbir ⊢ ¬ w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X
28 27 rgenw ⊢ ∀ w ∈ X ClWWalksNOn ⁡ G N ¬ w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X
29 rabeq0 ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X = ∅ ↔ ∀ w ∈ X ClWWalksNOn ⁡ G N ¬ w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X
30 28 29 mpbir ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∧ w ⁡ N − 2 = X = ∅
31 21 30 eqtri ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 ≠ X ∩ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X = ∅
32 20 31 eqtrdi ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N ∩ X C N = ∅
33 hashun ⊢ X H N ∈ Fin ∧ X C N ∈ Fin ∧ X H N ∩ X C N = ∅ → X H N ∪ X C N = X H N + X C N
34 14 19 32 33 syl3anc ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X H N ∪ X C N = X H N + X C N
35 5 34 eqtrd ⊢ G ∈ FinUSGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → X ClWWalksNOn ⁡ G N = X H N + X C N