Theorem numclwwlkovh0

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. (Contributed by AV, 1-May-2022)

	Ref	Expression
Hypothesis	numclwwlkovh.h	|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion	numclwwlkovh0	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )

Proof

Step	Hyp	Ref	Expression
1		numclwwlkovh.h	|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
2		oveq12	|- ( ( v = X /\ n = N ) -> ( v ( ClWWalksNOn ` G ) n ) = ( X ( ClWWalksNOn ` G ) N ) )
3		oveq1	|- ( n = N -> ( n - 2 ) = ( N - 2 ) )
4	3	adantl	|- ( ( v = X /\ n = N ) -> ( n - 2 ) = ( N - 2 ) )
5	4	fveq2d	|- ( ( v = X /\ n = N ) -> ( w ` ( n - 2 ) ) = ( w ` ( N - 2 ) ) )
6		simpl	|- ( ( v = X /\ n = N ) -> v = X )
7	5 6	neeq12d	|- ( ( v = X /\ n = N ) -> ( ( w ` ( n - 2 ) ) =/= v <-> ( w ` ( N - 2 ) ) =/= X ) )
8	2 7	rabeqbidv	|- ( ( v = X /\ n = N ) -> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )
9		ovex	|- ( X ( ClWWalksNOn ` G ) N ) e. _V
10	9	rabex	|- { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } e. _V
11	8 1 10	ovmpoa	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )