Metamath Proof Explorer

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 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion numclwwlkovh 
|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } )

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 1 numclwwlkovh0 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )
3 isclwwlknon 
 |-  ( w e. ( X ( ClWWalksNOn ` G ) N ) <-> ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) )
4 3 anbi1i 
 |-  ( ( w e. ( X ( ClWWalksNOn ` G ) N ) /\ ( w ` ( N - 2 ) ) =/= X ) <-> ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) )
5 simpll 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) -> w e. ( N ClWWalksN G ) )
6 simplr 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) -> ( w ` 0 ) = X )
7 neeq2 
 |-  ( X = ( w ` 0 ) -> ( ( w ` ( N - 2 ) ) =/= X <-> ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) )
8 7 eqcoms 
 |-  ( ( w ` 0 ) = X -> ( ( w ` ( N - 2 ) ) =/= X <-> ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) )
9 8 adantl 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> ( ( w ` ( N - 2 ) ) =/= X <-> ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) )
10 9 biimpa 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) -> ( w ` ( N - 2 ) ) =/= ( w ` 0 ) )
11 6 10 jca 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) -> ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) )
12 5 11 jca 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) -> ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) )
13 simpl 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) -> ( w ` 0 ) = X )
14 13 anim2i 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) -> ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) )
15 neeq2 
 |-  ( ( w ` 0 ) = X -> ( ( w ` ( N - 2 ) ) =/= ( w ` 0 ) <-> ( w ` ( N - 2 ) ) =/= X ) )
16 15 biimpa 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) -> ( w ` ( N - 2 ) ) =/= X )
17 16 adantl 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) -> ( w ` ( N - 2 ) ) =/= X )
18 14 17 jca 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) -> ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) )
19 12 18 impbii 
 |-  ( ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) =/= X ) <-> ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) )
20 4 19 bitri 
 |-  ( ( w e. ( X ( ClWWalksNOn ` G ) N ) /\ ( w ` ( N - 2 ) ) =/= X ) <-> ( w e. ( N ClWWalksN G ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) )
21 20 rabbia2 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } = { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) }
22 2 21 eqtrdi 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } )