Theorem numclwwlkovh

Description: Value of operation H , 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 7 in Huneke p. 2. Definition of ClWWalksNOn resolved. (Contributed by Alexander van der Vekens, 26-Aug-2018) (Revised by AV, 30-May-2021) (Revised by AV, 1-May-2022)

	Ref	Expression
Hypothesis	numclwwlkovh.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion	numclwwlkovh	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		numclwwlkovh.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
2	1	numclwwlkovh0	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )
3		isclwwlknon	⊢ ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
4	3	anbi1i	⊢ ( ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) ↔ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) )
5		simpll	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
6		simplr	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
7		neeq2	⊢ ( 𝑋 = ( 𝑤 ‘ 0 ) → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) )
8	7	eqcoms	⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) )
9	8	adantl	⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) )
10	9	biimpa	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) )
11	6 10	jca	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) )
12	5 11	jca	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) )
13		simpl	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) → ( 𝑤 ‘ 0 ) = 𝑋 )
14	13	anim2i	⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
15		neeq2	⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) )
16	15	biimpa	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 )
17	16	adantl	⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 )
18	14 17	jca	⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) → ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) )
19	12 18	impbii	⊢ ( ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) ↔ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) )
20	4 19	bitri	⊢ ( ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) ↔ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ) )
21	20	rabbia2	⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) }
22	2 21	eqtrdi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )