Theorem numclwwlkovq

Description: Value of operation Q , mapping a vertex v and a positive integer n to the not closed walks v(0) ... v(n) of length n from a fixed vertex v = v(0). "Not closed" means v(n) =/= v(0). Remark: n e. NN0 would not be useful: numclwwlkqhash would not hold, because ( K ^ 0 ) = 1 ! (Contributed by Alexander van der Vekens, 27-Sep-2018) (Revised by AV, 30-May-2021)

	Ref	Expression
Hypotheses	numclwwlk.v	|- V = ( Vtx ` G )
	numclwwlk.q	|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
Assertion	numclwwlkovq	|- ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	|- V = ( Vtx ` G )
2		numclwwlk.q	|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3		oveq1	|- ( n = N -> ( n WWalksN G ) = ( N WWalksN G ) )
4	3	adantl	|- ( ( v = X /\ n = N ) -> ( n WWalksN G ) = ( N WWalksN G ) )
5		eqeq2	|- ( v = X -> ( ( w ` 0 ) = v <-> ( w ` 0 ) = X ) )
6		neeq2	|- ( v = X -> ( ( lastS ` w ) =/= v <-> ( lastS ` w ) =/= X ) )
7	5 6	anbi12d	|- ( v = X -> ( ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
8	7	adantr	|- ( ( v = X /\ n = N ) -> ( ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) <-> ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) ) )
9	4 8	rabeqbidv	|- ( ( v = X /\ n = N ) -> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
10		ovex	|- ( N WWalksN G ) e. _V
11	10	rabex	|- { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } e. _V
12	9 2 11	ovmpoa	|- ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )