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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	numclwwlk.q	⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
Assertion	numclwwlkovq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		numclwwlk.q	⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 ) )
4	3	adantl	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑛 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 ) )
5		eqeq2	⊢ ( 𝑣 = 𝑋 → ( ( 𝑤 ‘ 0 ) = 𝑣 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
6		neeq2	⊢ ( 𝑣 = 𝑋 → ( ( lastS ‘ 𝑤 ) ≠ 𝑣 ↔ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) )
7	5 6	anbi12d	⊢ ( 𝑣 = 𝑋 → ( ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ) )
8	7	adantr	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ) )
9	4 8	rabeqbidv	⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
10		ovex	⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V
11	10	rabex	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ∈ V
12	9 2 11	ovmpoa	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )