Metamath Proof Explorer

Theorem numclwwlk1lem2foa

Description: Going forth and back from the end of a (closed) walk: W represents the closed walk p_0, ..., p_(n-2), p_0 = p_(n-2). With X = p_(n-2) = p_0 and Y = p_(n-1), ( ( W ++ <" X "> ) ++ <" Y "> ) represents the closed walk p_0, ..., p_(n-2), p_(n-1), p_n = p_0 which is a double loop of length N on vertex X . (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 5-Mar-2022) (Proof shortened by AV, 2-Nov-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 numclwwlk1lem2foa 
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W e. F /\ Y e. ( G NeighbVtx X ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X C N ) ) )

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 simpl2 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> X e. V )
5 1 nbgrisvtx 
 |-  ( Y e. ( G NeighbVtx X ) -> Y e. V )
6 5 ad2antll 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> Y e. V )
7 simpl3 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> N e. ( ZZ>= ` 3 ) )
8 nbgrsym 
 |-  ( Y e. ( G NeighbVtx X ) <-> X e. ( G NeighbVtx Y ) )
9 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
10 9 nbusgreledg 
 |-  ( G e. USGraph -> ( X e. ( G NeighbVtx Y ) <-> { X , Y } e. ( Edg ` G ) ) )
11 10 biimpd 
 |-  ( G e. USGraph -> ( X e. ( G NeighbVtx Y ) -> { X , Y } e. ( Edg ` G ) ) )
12 8 11 biimtrid 
 |-  ( G e. USGraph -> ( Y e. ( G NeighbVtx X ) -> { X , Y } e. ( Edg ` G ) ) )
13 12 adantld 
 |-  ( G e. USGraph -> ( ( W e. F /\ Y e. ( G NeighbVtx X ) ) -> { X , Y } e. ( Edg ` G ) ) )
14 13 3ad2ant1 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W e. F /\ Y e. ( G NeighbVtx X ) ) -> { X , Y } e. ( Edg ` G ) ) )
15 14 imp 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> { X , Y } e. ( Edg ` G ) )
16 simprl 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> W e. F )
17 16 3 eleqtrdi 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
18 1 9 clwwlknonex2 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. ( Edg ` G ) /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )
19 4 6 7 15 17 18 syl311anc 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )
20 3 eleq2i 
 |-  ( W e. F <-> W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
21 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
22 21 nnne0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) =/= 0 )
23 1 9 clwwlknonel 
 |-  ( ( N - 2 ) =/= 0 -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
24 22 23 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
25 24 3ad2ant3 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
26 20 25 bitrid 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. F <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
27 3simpa 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) )
28 27 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Y e. ( G NeighbVtx X ) ) -> ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) )
29 simp32 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
30 29 5 anim12i 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Y e. ( G NeighbVtx X ) ) -> ( X e. V /\ Y e. V ) )
31 simpl33 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Y e. ( G NeighbVtx X ) ) -> N e. ( ZZ>= ` 3 ) )
32 28 30 31 3jca 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Y e. ( G NeighbVtx X ) ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) )
33 32 3exp1 
 |-  ( W e. Word V -> ( ( # ` W ) = ( N - 2 ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) ) )
34 33 3ad2ant1 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( ( # ` W ) = ( N - 2 ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) ) )
35 34 imp 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) )
36 35 3adant3 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) )
37 36 com12 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) )
38 26 37 sylbid 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. F -> ( Y e. ( G NeighbVtx X ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) ) ) )
39 38 imp32 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) )
40 numclwwlk1lem2foalem 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )
41 39 40 syl 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )
42 eleq1a 
 |-  ( W e. F -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F ) )
43 16 42 syl 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F ) )
44 eleq1a 
 |-  ( Y e. ( G NeighbVtx X ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) ) )
45 44 ad2antll 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) ) )
46 idd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )
47 43 45 46 3anim123d 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) ) )
48 41 47 mpd 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )
49 1 2 3 extwwlkfabel 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X C N ) <-> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) /\ ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) ) ) )
50 49 adantr 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X C N ) <-> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) /\ ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) e. F /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) ) ) )
51 19 48 50 mpbir2and 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. F /\ Y e. ( G NeighbVtx X ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X C N ) )
52 51 ex 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W e. F /\ Y e. ( G NeighbVtx X ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X C N ) ) )