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 = ( 𝑛 ∈ ℕ , 𝑘 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) ↦ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgpg | ⊢ gPetersenGr | |
| 1 | vn | ⊢ 𝑛 | |
| 2 | cn | ⊢ ℕ | |
| 3 | vk | ⊢ 𝑘 | |
| 4 | c1 | ⊢ 1 | |
| 5 | cfzo | ⊢ ..^ | |
| 6 | cceil | ⊢ ⌈ | |
| 7 | 1 | cv | ⊢ 𝑛 |
| 8 | cdiv | ⊢ / | |
| 9 | c2 | ⊢ 2 | |
| 10 | 7 9 8 | co | ⊢ ( 𝑛 / 2 ) |
| 11 | 10 6 | cfv | ⊢ ( ⌈ ‘ ( 𝑛 / 2 ) ) |
| 12 | 4 11 5 | co | ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 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 ..^ 𝑛 ) |
| 19 | 17 18 | cxp | ⊢ ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) |
| 20 | 15 19 | cop | ⊢ ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ |
| 21 | cedgf | ⊢ .ef | |
| 22 | 14 21 | cfv | ⊢ ( .ef ‘ ndx ) |
| 23 | cid | ⊢ I | |
| 24 | ve | ⊢ 𝑒 | |
| 25 | 19 | cpw | ⊢ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) |
| 26 | vx | ⊢ 𝑥 | |
| 27 | 24 | cv | ⊢ 𝑒 |
| 28 | 26 | cv | ⊢ 𝑥 |
| 29 | 16 28 | cop | ⊢ ⟨ 0 , 𝑥 ⟩ |
| 30 | caddc | ⊢ + | |
| 31 | 28 4 30 | co | ⊢ ( 𝑥 + 1 ) |
| 32 | cmo | ⊢ mod | |
| 33 | 31 7 32 | co | ⊢ ( ( 𝑥 + 1 ) mod 𝑛 ) |
| 34 | 16 33 | cop | ⊢ ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ |
| 35 | 29 34 | cpr | ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } |
| 36 | 27 35 | wceq | ⊢ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } |
| 37 | 4 28 | cop | ⊢ ⟨ 1 , 𝑥 ⟩ |
| 38 | 29 37 | cpr | ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } |
| 39 | 27 38 | wceq | ⊢ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } |
| 40 | 3 | cv | ⊢ 𝑘 |
| 41 | 28 40 30 | co | ⊢ ( 𝑥 + 𝑘 ) |
| 42 | 41 7 32 | co | ⊢ ( ( 𝑥 + 𝑘 ) mod 𝑛 ) |
| 43 | 4 42 | cop | ⊢ ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ |
| 44 | 37 43 | cpr | ⊢ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } |
| 45 | 27 44 | wceq | ⊢ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } |
| 46 | 36 39 45 | w3o | ⊢ ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) |
| 47 | 46 26 18 | wrex | ⊢ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) |
| 48 | 47 24 25 | crab | ⊢ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } |
| 49 | 23 48 | cres | ⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) |
| 50 | 22 49 | cop | ⊢ ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ |
| 51 | 20 50 | cpr | ⊢ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } |
| 52 | 1 3 2 12 51 | cmpo | ⊢ ( 𝑛 ∈ ℕ , 𝑘 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) ↦ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } ) |
| 53 | 0 52 | wceq | ⊢ gPetersenGr = ( 𝑛 ∈ ℕ , 𝑘 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) ↦ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } ) |