Theorem 2clwwlk

Description: Value of operation C , mapping a vertex v and an integer n greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v" according to definition 6 in Huneke p. 2. Such closed walks are "double loops" consisting of a closed (n-2)-walk v = v(0) ... v(n-2) = v and a closed 2-walk v = v(n-2) v(n-1) v(n) = v, see 2clwwlk2clwwlk . ( X C N ) is called the "set of double loops of length N on vertex X " in the following. (Contributed by Alexander van der Vekens, 14-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 20-Apr-2022)

	Ref	Expression
Hypothesis	2clwwlk.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
Assertion	2clwwlk	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2		oveq12	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
3		fvoveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) )
4	3	adantl	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) )
5		simpl	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → 𝑣 = 𝑋 )
6	4 5	eqeq12d	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
7	2 6	rabeqbidv	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
8		ovex	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V
9	8	rabex	⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ∈ V
10	7 1 9	ovmpoa	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )