Metamath Proof Explorer

Theorem numclwwlk1lem2

Description: The set of double loops of length N on vertex X and the set of closed walks of length less by 2 on X combined with the neighbors of X are equinumerous. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 29-May-2021) (Revised by AV, 31-Jul-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ V = Vtx ⁡ G
extwwlkfab.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
Assertion numclwwlk1lem2 ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X C N ≈ F × G NeighbVtx X

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ V = Vtx ⁡ G
2 extwwlkfab.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
3 extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
4 oveq1 ⊢ x = u → x prefix N − 2 = u prefix N − 2
5 fveq1 ⊢ x = u → x ⁡ N − 1 = u ⁡ N − 1
6 4 5 opeq12d ⊢ x = u → x prefix N − 2 x ⁡ N − 1 = u prefix N − 2 u ⁡ N − 1
7 6 cbvmptv ⊢ x ∈ X C N ⟼ x prefix N − 2 x ⁡ N − 1 = u ∈ X C N ⟼ u prefix N − 2 u ⁡ N − 1
8 1 2 3 7 numclwwlk1lem2f1o ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → x ∈ X C N ⟼ x prefix N − 2 x ⁡ N − 1 : X C N ⟶ 1-1 onto F × G NeighbVtx X
9 ovex ⊢ X C N ∈ V
10 9 f1oen ⊢ x ∈ X C N ⟼ x prefix N − 2 x ⁡ N − 1 : X C N ⟶ 1-1 onto F × G NeighbVtx X → X C N ≈ F × G NeighbVtx X
11 8 10 syl ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X C N ≈ F × G NeighbVtx X