Metamath Proof Explorer

Definition df-gpg

Description: Definition of generalized Petersen graphs according to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph : "In Watkins' notation, G ( n , k ) is a graph with vertex set { u_0, u_1, ... , u_n-1, v_0, v_1, ... , v_n-1 } and edge set { u_i u_i+1 , u_i v_i , v_i v_i+k | 0 <_ i <_ ( n - 1 ) } where subscripts are to be read modulo n and where k < ( n / 2 ) . Some authors use the notation GPG(n,k)."

Instead of n e. NN , we could restrict the first argument to n e. ( ZZ>=3 ) (i.e., 3 <_ n ), because for n <_ 2 , the definition is not meaningful (since then ( |^( n / 2 ) ) <_ 1 and therefore ( 1 ..^ ( |^( n / 2 ) ) ) = (/) , so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025)

Ref Expression
Assertion df-gpg 
|- gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgpg 
 |-  gPetersenGr
1 vn 
 |-  n
2 cn 
 |-  NN
3 vk 
 |-  k
4 c1 
 |-  1
5 cfzo 
 |-  ..^
6 cceil 
 |-  |^
7 1 cv 
 |-  n
8 cdiv 
 |-  /
9 c2 
 |-  2
10 7 9 8 co 
 |-  ( n / 2 )
11 10 6 cfv 
 |-  ( |^ ` ( n / 2 ) )
12 4 11 5 co 
 |-  ( 1 ..^ ( |^ ` ( n / 2 ) ) )
13 cbs 
 |-  Base
14 cnx 
 |-  ndx
15 14 13 cfv 
 |-  ( Base ` ndx )
16 cc0 
 |-  0
17 16 4 cpr 
 |-  { 0 , 1 }
18 16 7 5 co 
 |-  ( 0 ..^ n )
19 17 18 cxp 
 |-  ( { 0 , 1 } X. ( 0 ..^ n ) )
20 15 19 cop 
 |-  <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >.
21 cedgf 
 |-  .ef
22 14 21 cfv 
 |-  ( .ef ` ndx )
23 cid 
 |-  _I
24 ve 
 |-  e
25 19 cpw 
 |-  ~P ( { 0 , 1 } X. ( 0 ..^ n ) )
26 vx 
 |-  x
27 24 cv 
 |-  e
28 26 cv 
 |-  x
29 16 28 cop 
 |-  <. 0 , x >.
30 caddc 
 |-  +
31 28 4 30 co 
 |-  ( x + 1 )
32 cmo 
 |-  mod
33 31 7 32 co 
 |-  ( ( x + 1 ) mod n )
34 16 33 cop 
 |-  <. 0 , ( ( x + 1 ) mod n ) >.
35 29 34 cpr 
 |-  { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. }
36 27 35 wceq 
 |-  e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. }
37 4 28 cop 
 |-  <. 1 , x >.
38 29 37 cpr 
 |-  { <. 0 , x >. , <. 1 , x >. }
39 27 38 wceq 
 |-  e = { <. 0 , x >. , <. 1 , x >. }
40 3 cv 
 |-  k
41 28 40 30 co 
 |-  ( x + k )
42 41 7 32 co 
 |-  ( ( x + k ) mod n )
43 4 42 cop 
 |-  <. 1 , ( ( x + k ) mod n ) >.
44 37 43 cpr 
 |-  { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. }
45 27 44 wceq 
 |-  e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. }
46 36 39 45 w3o 
 |-  ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } )
47 46 26 18 wrex 
 |-  E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } )
48 47 24 25 crab 
 |-  { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) }
49 23 48 cres 
 |-  ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } )
50 22 49 cop 
 |-  <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >.
51 20 50 cpr 
 |-  { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. }
52 1 3 2 12 51 cmpo 
 |-  ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } )
53 0 52 wceq 
 |-  gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } )