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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
	extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
Assertion	numclwwlk1lem2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3		extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4		oveq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 prefix ( 𝑁 − 2 ) ) = ( 𝑢 prefix ( 𝑁 − 2 ) ) )
5		fveq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 ‘ ( 𝑁 − 1 ) ) = ( 𝑢 ‘ ( 𝑁 − 1 ) ) )
6	4 5	opeq12d	⊢ ( 𝑥 = 𝑢 → ⟨ ( 𝑥 prefix ( 𝑁 − 2 ) ) , ( 𝑥 ‘ ( 𝑁 − 1 ) ) ⟩ = ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
7	6	cbvmptv	⊢ ( 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑥 prefix ( 𝑁 − 2 ) ) , ( 𝑥 ‘ ( 𝑁 − 1 ) ) ⟩ ) = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
8	1 2 3 7	numclwwlk1lem2f1o	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑥 prefix ( 𝑁 − 2 ) ) , ( 𝑥 ‘ ( 𝑁 − 1 ) ) ⟩ ) : ( 𝑋 𝐶 𝑁 ) –1-1-onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
9		ovex	⊢ ( 𝑋 𝐶 𝑁 ) ∈ V
10	9	f1oen	⊢ ( ( 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑥 prefix ( 𝑁 − 2 ) ) , ( 𝑥 ‘ ( 𝑁 − 1 ) ) ⟩ ) : ( 𝑋 𝐶 𝑁 ) –1-1-onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) → ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
11	8 10	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )