Definition df-gpg 47890

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, 𝐺(𝑛, 𝑘) is a graph with vertex set { u₀, u₁, ... , u_n-1, v₀, v₁, ... , v_n-1 } and edge set { u_i u_i+1 , u_i v_i , v_i v_i+k | 0 ≤ 𝑖 ≤ (𝑛 − 1) } where subscripts are to be read modulo n and where 𝑘 < (𝑛 / 2). Some authors use the notation GPG(n,k)."

Instead of 𝑛 ∈ ℕ, we could restrict the first argument to 𝑛 ∈ (ℤ_≥‘3) (i.e., 3 ≤ 𝑛), because for 𝑛 ≤ 2, the definition is not meaningful (since then (⌈‘(𝑛 / 2)) ≤ 1 and therefore (1..^(⌈‘(𝑛 / 2))) = ∅, so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025.)

Assertion

Ref	Expression
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 𝑛)⟩})})⟩})

Distinct variable group:   𝑒,𝑘,𝑛,𝑥

Detailed syntax breakdown of Definition df-gpg

Step	Hyp	Ref	Expression
1		cgpg 47889	. 2 class gPetersenGr
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn 12298	. . 3 class ℕ
5		c1 11188	. . . 4 class 1
6	2	cv 1536	. . . . . 6 class 𝑛
7		c2 12353	. . . . . 6 class 2
8		cdiv 11952	. . . . . 6 class /
9	6, 7, 8	co 7451	. . . . 5 class (𝑛 / 2)
10		cceil 13858	. . . . 5 class ⌈
11	9, 10	cfv 6576	. . . 4 class (⌈‘(𝑛 / 2))
12		cfzo 13722	. . . 4 class ..^
13	5, 11, 12	co 7451	. . 3 class (1..^(⌈‘(𝑛 / 2)))
14		cnx 17260	. . . . . 6 class ndx
15		cbs 17278	. . . . . 6 class Base
16	14, 15	cfv 6576	. . . . 5 class (Base‘ndx)
17		cc0 11187	. . . . . . 7 class 0
18	17, 5	cpr 4650	. . . . . 6 class {0, 1}
19	17, 6, 12	co 7451	. . . . . 6 class (0..^𝑛)
20	18, 19	cxp 5699	. . . . 5 class ({0, 1} × (0..^𝑛))
21	16, 20	cop 4654	. . . 4 class ⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩
22		cedgf 29041	. . . . . 6 class .ef
23	14, 22	cfv 6576	. . . . 5 class (.ef‘ndx)
24		cid 5593	. . . . . 6 class I
25		ve	. . . . . . . . . . 11 setvar 𝑒
26	25	cv 1536	. . . . . . . . . 10 class 𝑒
27		vx	. . . . . . . . . . . . 13 setvar 𝑥
28	27	cv 1536	. . . . . . . . . . . 12 class 𝑥
29	17, 28	cop 4654	. . . . . . . . . . 11 class ⟨0, 𝑥⟩
30		caddc 11190	. . . . . . . . . . . . . 14 class +
31	28, 5, 30	co 7451	. . . . . . . . . . . . 13 class (𝑥 + 1)
32		cmo 13936	. . . . . . . . . . . . 13 class mod
33	31, 6, 32	co 7451	. . . . . . . . . . . 12 class ((𝑥 + 1) mod 𝑛)
34	17, 33	cop 4654	. . . . . . . . . . 11 class ⟨0, ((𝑥 + 1) mod 𝑛)⟩
35	29, 34	cpr 4650	. . . . . . . . . 10 class {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩}
36	26, 35	wceq 1537	. . . . . . . . 9 wff 𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩}
37	5, 28	cop 4654	. . . . . . . . . . 11 class ⟨1, 𝑥⟩
38	29, 37	cpr 4650	. . . . . . . . . 10 class {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}
39	26, 38	wceq 1537	. . . . . . . . 9 wff 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}
40	3	cv 1536	. . . . . . . . . . . . . 14 class 𝑘
41	28, 40, 30	co 7451	. . . . . . . . . . . . 13 class (𝑥 + 𝑘)
42	41, 6, 32	co 7451	. . . . . . . . . . . 12 class ((𝑥 + 𝑘) mod 𝑛)
43	5, 42	cop 4654	. . . . . . . . . . 11 class ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩
44	37, 43	cpr 4650	. . . . . . . . . 10 class {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩}
45	26, 44	wceq 1537	. . . . . . . . 9 wff 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩}
46	36, 39, 45	w3o 1086	. . . . . . . 8 wff (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})
47	46, 27, 19	wrex 3076	. . . . . . 7 wff ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})
48	20	cpw 4622	. . . . . . 7 class 𝒫 ({0, 1} × (0..^𝑛))
49	47, 25, 48	crab 3443	. . . . . 6 class {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})}
50	24, 49	cres 5703	. . . . 5 class ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})
51	23, 50	cop 4654	. . . 4 class ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩
52	21, 51	cpr 4650	. . 3 class {⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩}
53	2, 3, 4, 13, 52	cmpo 7453	. 2 class (𝑛 ∈ ℕ, 𝑘 ∈ (1..^(⌈‘(𝑛 / 2))) ↦ {⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩})
54	1, 53	wceq 1537	1 wff gPetersenGr = (𝑛 ∈ ℕ, 𝑘 ∈ (1..^(⌈‘(𝑛 / 2))) ↦ {⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩})

This definition is referenced by:  gpgov  47891