Metamath Proof Explorer

Theorem extwwlkfabel

Description: Characterization of an element of the set ( X C N ) , i.e., a double loop of length N on vertex X with a construction from the set F of closed walks on X with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). (Contributed by AV, 22-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v 
|- V = ( Vtx ` G )
extwwlkfab.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
extwwlkfab.f 
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
Assertion extwwlkfabel 
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> ( W e. ( N ClWWalksN G ) /\ ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v 
 |-  V = ( Vtx ` G )
2 extwwlkfab.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
3 extwwlkfab.f 
 |-  F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
4 1 2 3 extwwlkfab 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) = { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } )
5 4 eleq2d 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> W e. { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } ) )
6 oveq1 
 |-  ( w = W -> ( w prefix ( N - 2 ) ) = ( W prefix ( N - 2 ) ) )
7 6 eleq1d 
 |-  ( w = W -> ( ( w prefix ( N - 2 ) ) e. F <-> ( W prefix ( N - 2 ) ) e. F ) )
8 fveq1 
 |-  ( w = W -> ( w ` ( N - 1 ) ) = ( W ` ( N - 1 ) ) )
9 8 eleq1d 
 |-  ( w = W -> ( ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) <-> ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) ) )
10 fveq1 
 |-  ( w = W -> ( w ` ( N - 2 ) ) = ( W ` ( N - 2 ) ) )
11 10 eqeq1d 
 |-  ( w = W -> ( ( w ` ( N - 2 ) ) = X <-> ( W ` ( N - 2 ) ) = X ) )
12 7 9 11 3anbi123d 
 |-  ( w = W -> ( ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) )
13 12 elrab 
 |-  ( W e. { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } <-> ( W e. ( N ClWWalksN G ) /\ ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) )
14 5 13 bitrdi 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> ( W e. ( N ClWWalksN G ) /\ ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) ) )