Metamath Proof Explorer


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 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion numclwwlkovh0 ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )

Proof

Step Hyp Ref Expression
1 numclwwlkovh.h 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
2 oveq12 ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
3 oveq1 ( 𝑛 = 𝑁 → ( 𝑛 − 2 ) = ( 𝑁 − 2 ) )
4 3 adantl ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → ( 𝑛 − 2 ) = ( 𝑁 − 2 ) )
5 4 fveq2d ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) )
6 simpl ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → 𝑣 = 𝑋 )
7 5 6 neeq12d ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → ( ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) )
8 2 7 rabeqbidv ( ( 𝑣 = 𝑋𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )
9 ovex ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V
10 9 rabex { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∈ V
11 8 1 10 ovmpoa ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )