Metamath Proof Explorer

Theorem gpgnbgrvtx0

Description: The (open) neighborhood of an outside vertex in a generalized Petersen graph G . (Contributed by AV, 28-Aug-2025)

Ref Expression
Hypotheses gpgnbgr.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgnbgr.g 
|- G = ( N gPetersenGr K )
gpgnbgr.v 
|- V = ( Vtx ` G )
gpgnbgr.u 
|- U = ( G NeighbVtx X )
Assertion gpgnbgrvtx0 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> U = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } )

Proof

Step Hyp Ref Expression
1 gpgnbgr.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgnbgr.g 
 |-  G = ( N gPetersenGr K )
3 gpgnbgr.v 
 |-  V = ( Vtx ` G )
4 gpgnbgr.u 
 |-  U = ( G NeighbVtx X )
5 4 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> U = ( G NeighbVtx X ) )
6 1 eleq2i 
 |-  ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
7 gpgusgra 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )
8 6 7 sylan2b 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( N gPetersenGr K ) e. USGraph )
9 2 8 eqeltrid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> G e. USGraph )
10 simpl 
 |-  ( ( X e. V /\ ( 1st ` X ) = 0 ) -> X e. V )
11 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
12 3 11 nbusgrvtx 
 |-  ( ( G e. USGraph /\ X e. V ) -> ( G NeighbVtx X ) = { y e. V | { X , y } e. ( Edg ` G ) } )
13 9 10 12 syl2an 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( G NeighbVtx X ) = { y e. V | { X , y } e. ( Edg ` G ) } )
14 simpl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
15 simpr 
 |-  ( ( X e. V /\ ( 1st ` X ) = 0 ) -> ( 1st ` X ) = 0 )
16 15 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 1st ` X ) = 0 )
17 simpr 
 |-  ( ( v e. V /\ { X , v } e. ( Edg ` G ) ) -> { X , v } e. ( Edg ` G ) )
18 1 2 3 11 gpgvtxedg0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ { X , v } e. ( Edg ` G ) ) -> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
19 14 16 17 18 syl2an3an 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ ( v e. V /\ { X , v } e. ( Edg ` G ) ) ) -> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
20 19 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( v e. V /\ { X , v } e. ( Edg ` G ) ) -> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
21 1 2 3 gpgvtx0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ <. 0 , ( 2nd ` X ) >. e. V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) )
22 21 simp1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V )
23 22 adantrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V )
24 1 2 3 11 gpgedgvtx0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. ( Edg ` G ) /\ { X , <. 1 , ( 2nd ` X ) >. } e. ( Edg ` G ) /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. ( Edg ` G ) ) )
25 24 simp1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. ( Edg ` G ) )
26 23 25 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. ( Edg ` G ) ) )
27 eleq1 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. -> ( v e. V <-> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V ) )
28 preq2 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. -> { X , v } = { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } )
29 28 eleq1d 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. -> ( { X , v } e. ( Edg ` G ) <-> { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. ( Edg ` G ) ) )
30 27 29 anbi12d 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. -> ( ( v e. V /\ { X , v } e. ( Edg ` G ) ) <-> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. V /\ { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. ( Edg ` G ) ) ) )
31 26 30 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. -> ( v e. V /\ { X , v } e. ( Edg ` G ) ) ) )
32 1 2 3 gpgvtx1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. e. V /\ <. 1 , ( 2nd ` X ) >. e. V /\ <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. e. V ) )
33 32 simp2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> <. 1 , ( 2nd ` X ) >. e. V )
34 33 adantrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 1 , ( 2nd ` X ) >. e. V )
35 24 simp2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> { X , <. 1 , ( 2nd ` X ) >. } e. ( Edg ` G ) )
36 34 35 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( <. 1 , ( 2nd ` X ) >. e. V /\ { X , <. 1 , ( 2nd ` X ) >. } e. ( Edg ` G ) ) )
37 eleq1 
 |-  ( v = <. 1 , ( 2nd ` X ) >. -> ( v e. V <-> <. 1 , ( 2nd ` X ) >. e. V ) )
38 preq2 
 |-  ( v = <. 1 , ( 2nd ` X ) >. -> { X , v } = { X , <. 1 , ( 2nd ` X ) >. } )
39 38 eleq1d 
 |-  ( v = <. 1 , ( 2nd ` X ) >. -> ( { X , v } e. ( Edg ` G ) <-> { X , <. 1 , ( 2nd ` X ) >. } e. ( Edg ` G ) ) )
40 37 39 anbi12d 
 |-  ( v = <. 1 , ( 2nd ` X ) >. -> ( ( v e. V /\ { X , v } e. ( Edg ` G ) ) <-> ( <. 1 , ( 2nd ` X ) >. e. V /\ { X , <. 1 , ( 2nd ` X ) >. } e. ( Edg ` G ) ) ) )
41 36 40 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( v = <. 1 , ( 2nd ` X ) >. -> ( v e. V /\ { X , v } e. ( Edg ` G ) ) ) )
42 21 simp3d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V )
43 42 adantrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V )
44 43 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V )
45 eleq1 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. -> ( v e. V <-> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) )
46 45 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> ( v e. V <-> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. V ) )
47 44 46 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> v e. V )
48 24 simp3d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. ( Edg ` G ) )
49 48 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. ( Edg ` G ) )
50 preq2 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. -> { X , v } = { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } )
51 50 eleq1d 
 |-  ( v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. -> ( { X , v } e. ( Edg ` G ) <-> { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. ( Edg ` G ) ) )
52 51 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> ( { X , v } e. ( Edg ` G ) <-> { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. ( Edg ` G ) ) )
53 49 52 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> { X , v } e. ( Edg ` G ) )
54 47 53 jca 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) /\ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> ( v e. V /\ { X , v } e. ( Edg ` G ) ) )
55 54 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. -> ( v e. V /\ { X , v } e. ( Edg ` G ) ) ) )
56 31 41 55 3jaod 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) -> ( v e. V /\ { X , v } e. ( Edg ` G ) ) ) )
57 20 56 impbid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( v e. V /\ { X , v } e. ( Edg ` G ) ) <-> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
58 preq2 
 |-  ( y = v -> { X , y } = { X , v } )
59 58 eleq1d 
 |-  ( y = v -> ( { X , y } e. ( Edg ` G ) <-> { X , v } e. ( Edg ` G ) ) )
60 59 elrab 
 |-  ( v e. { y e. V | { X , y } e. ( Edg ` G ) } <-> ( v e. V /\ { X , v } e. ( Edg ` G ) ) )
61 vex 
 |-  v e. _V
62 61 eltp 
 |-  ( v e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } <-> ( v = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ v = <. 1 , ( 2nd ` X ) >. \/ v = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
63 57 60 62 3bitr4g 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( v e. { y e. V | { X , y } e. ( Edg ` G ) } <-> v e. { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } ) )
64 63 eqrdv 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> { y e. V | { X , y } e. ( Edg ` G ) } = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } )
65 5 13 64 3eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> U = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } )