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 \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
Assertion	numclwwlk1lem2	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (X C N) \approx (F \times (G NeighbVtx X))$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		oveq1	$⊢ x = u \to x prefix (N - 2) = u prefix (N - 2)$
5		fveq1	$⊢ x = u \to x (N - 1) = u (N - 1)$
6	4 5	opeq12d	$⊢ x = u \to ⟨x prefix (N - 2), x (N - 1)⟩ = ⟨u prefix (N - 2), u (N - 1)⟩$
7	6	cbvmptv	$⊢ (x \in (X C N) ⟼ ⟨x prefix (N - 2), x (N - 1)⟩) = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
8	1 2 3 7	numclwwlk1lem2f1o	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (x \in (X C N) ⟼ ⟨x prefix (N - 2), x (N - 1)⟩) : X C N \underset{1-1 onto}{⟶} F \times (G NeighbVtx X)$
9		ovex	$⊢ X C N \in V$
10	9	f1oen	$⊢ (x \in (X C N) ⟼ ⟨x prefix (N - 2), x (N - 1)⟩) : X C N \underset{1-1 onto}{⟶} F \times (G NeighbVtx X) \to (X C N) \approx (F \times (G NeighbVtx X))$
11	8 10	syl	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (X C N) \approx (F \times (G NeighbVtx X))$

Metamath Proof Explorer

Theorem numclwwlk1lem2

Proof