Metamath Proof Explorer

Theorem extwwlkfab

Description: The set ( X C N ) of double loops of length N on vertex X can be constructed 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). 3 <_ N is required since for N = 2 : F = ( X ( ClWWalksNOnG ) 0 ) = (/) (see clwwlk0on0 stating that a closed walk of length 0 is not represented as word), which would result in an empty set on the right hand side, but ( X C N ) needs not be empty, see 2clwwlk2 . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 29-May-2021) (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 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 ) } )

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 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
5 2 2clwwlk 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
6 4 5 sylan2 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
7 6 3adant1 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
8 clwwlknon 
 |-  ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }
9 8 rabeqi 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } = { w e. { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } | ( w ` ( N - 2 ) ) = X }
10 rabrab 
 |-  { w e. { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } | ( w ` ( N - 2 ) ) = X } = { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) }
11 simpll3 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> N e. ( ZZ>= ` 3 ) )
12 simplr 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> w e. ( N ClWWalksN G ) )
13 simpr 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> ( w ` ( N - 2 ) ) = X )
14 simpl 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> ( w ` 0 ) = X )
15 14 eqcomd 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> X = ( w ` 0 ) )
16 13 15 eqtrd 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> ( w ` ( N - 2 ) ) = ( w ` 0 ) )
17 16 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w ` ( N - 2 ) ) = ( w ` 0 ) )
18 clwwnrepclwwn 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ w e. ( N ClWWalksN G ) /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) -> ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) )
19 11 12 17 18 syl3anc 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) )
20 14 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w ` 0 ) = X )
21 19 20 jca 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) )
22 simp1 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> G e. USGraph )
23 22 anim1i 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( G e. USGraph /\ w e. ( N ClWWalksN G ) ) )
24 23 adantr 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( G e. USGraph /\ w e. ( N ClWWalksN G ) ) )
25 clwwlknlbonbgr1 
 |-  ( ( G e. USGraph /\ w e. ( N ClWWalksN G ) ) -> ( w ` ( N - 1 ) ) e. ( G NeighbVtx ( w ` 0 ) ) )
26 24 25 syl 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w ` ( N - 1 ) ) e. ( G NeighbVtx ( w ` 0 ) ) )
27 oveq2 
 |-  ( X = ( w ` 0 ) -> ( G NeighbVtx X ) = ( G NeighbVtx ( w ` 0 ) ) )
28 27 eqcoms 
 |-  ( ( w ` 0 ) = X -> ( G NeighbVtx X ) = ( G NeighbVtx ( w ` 0 ) ) )
29 28 adantr 
 |-  ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> ( G NeighbVtx X ) = ( G NeighbVtx ( w ` 0 ) ) )
30 29 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( G NeighbVtx X ) = ( G NeighbVtx ( w ` 0 ) ) )
31 26 30 eleqtrrd 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) )
32 13 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( w ` ( N - 2 ) ) = X )
33 21 31 32 3jca 
 |-  ( ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) ) -> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) )
34 33 ex 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) -> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) ) )
35 simpr 
 |-  ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X )
36 35 anim1i 
 |-  ( ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 2 ) ) = X ) -> ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) )
37 36 3adant2 
 |-  ( ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) -> ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) )
38 34 37 impbid1 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) ) )
39 2clwwlklem 
 |-  ( ( w e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( w prefix ( N - 2 ) ) ` 0 ) = ( w ` 0 ) )
40 39 3ad2antr3 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( w prefix ( N - 2 ) ) ` 0 ) = ( w ` 0 ) )
41 40 ancoms 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( w prefix ( N - 2 ) ) ` 0 ) = ( w ` 0 ) )
42 41 eqcomd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( w ` 0 ) = ( ( w prefix ( N - 2 ) ) ` 0 ) )
43 42 eqeq1d 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( w ` 0 ) = X <-> ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) )
44 43 anbi2d 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) <-> ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) ) )
45 44 3anbi1d 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( w ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) ) )
46 3 eleq2i 
 |-  ( ( w prefix ( N - 2 ) ) e. F <-> ( w prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
47 isclwwlknon 
 |-  ( ( w prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) )
48 47 a1i 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( w prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) ) )
49 46 48 syl5bb 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( w prefix ( N - 2 ) ) e. F <-> ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) ) )
50 49 3anbi1d 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) ) )
51 50 bicomd 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) /\ ( 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 ) ) )
52 51 adantr 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( ( w prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) /\ ( ( w prefix ( N - 2 ) ) ` 0 ) = X ) /\ ( 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 ) ) )
53 38 45 52 3bitrd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ w e. ( N ClWWalksN G ) ) -> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) ) )
54 53 rabbidva 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = 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 ) } )
55 10 54 syl5eq 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> { w e. { w e. ( N ClWWalksN G ) | ( w ` 0 ) = 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 ) } )
56 9 55 syl5eq 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( 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 ) } )
57 7 56 eqtrd 
 |-  ( ( 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 ) } )