Theorem gpgov

Description: The generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025)

	Ref	Expression
Hypotheses	gpgov.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgov.i	$$⊢I=\left(0..^N\right)$$
Assertion	gpgov	Could not format assertion : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gpgov.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
2		gpgov.i	$$⊢I=\left(0..^N\right)$$
3		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}\in \mathrm{V}$$
4		oveq2	$$⊢n=N\to \left(0..^n\right)=\left(0..^N\right)$$
5	4 2	eqtr4di	$$⊢n=N\to \left(0..^n\right)=I$$
6	5	xpeq2d	$$⊢n=N\to \left\{0,1\right\}\times \left(0..^n\right)=\left\{0,1\right\}\times I$$
7	6	opeq2d	$$⊢n=N\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩$$
8	7	adantr	$$⊢\left(n=N\wedge k=K\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩$$
9	6	pweqd	$$⊢n=N\to 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)=𝒫\left(\left\{0,1\right\}\times I\right)$$
10	9	adantr	$$⊢\left(n=N\wedge k=K\right)\to 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)=𝒫\left(\left\{0,1\right\}\times I\right)$$
11	5	rexeqdv	$$⊢n=N\to \left(\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\leftrightarrow \exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right)$$
12	11	adantr	$$⊢\left(n=N\wedge k=K\right)\to \left(\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\leftrightarrow \exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right)$$
13		oveq2	$$⊢n=N\to \left(x+1\right)\mathrm{mod}n=\left(x+1\right)\mathrm{mod}N$$
14	13	opeq2d	$$⊢n=N\to ⟨0,\left(x+1\right)\mathrm{mod}n⟩=⟨0,\left(x+1\right)\mathrm{mod}N⟩$$
15	14	preq2d	$$⊢n=N\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}$$
16	15	adantr	$$⊢\left(n=N\wedge k=K\right)\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}$$
17	16	eqeq2d	$$⊢\left(n=N\wedge k=K\right)\to \left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\leftrightarrow e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
18		biidd	$$⊢\left(n=N\wedge k=K\right)\to \left(e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
19		oveq2	$$⊢k=K\to x+k=x+K$$
20	19	adantl	$$⊢\left(n=N\wedge k=K\right)\to x+k=x+K$$
21		simpl	$$⊢\left(n=N\wedge k=K\right)\to n=N$$
22	20 21	oveq12d	$$⊢\left(n=N\wedge k=K\right)\to \left(x+k\right)\mathrm{mod}n=\left(x+K\right)\mathrm{mod}N$$
23	22	opeq2d	$$⊢\left(n=N\wedge k=K\right)\to ⟨1,\left(x+k\right)\mathrm{mod}n⟩=⟨1,\left(x+K\right)\mathrm{mod}N⟩$$
24	23	preq2d	$$⊢\left(n=N\wedge k=K\right)\to \left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}$$
25	24	eqeq2d	$$⊢\left(n=N\wedge k=K\right)\to \left(e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\leftrightarrow e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)$$
26	17 18 25	3orbi123d	$$⊢\left(n=N\wedge k=K\right)\to \left(\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\leftrightarrow \left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
27	26	rexbidv	$$⊢\left(n=N\wedge k=K\right)\to \left(\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\leftrightarrow \exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
28	12 27	bitrd	$$⊢\left(n=N\wedge k=K\right)\to \left(\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\leftrightarrow \exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
29	10 28	rabeqbidv	$$⊢\left(n=N\wedge k=K\right)\to \left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}=\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}$$
30	29	reseq2d	$$⊢\left(n=N\wedge k=K\right)\to {\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}={\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}$$
31	30	opeq2d	$$⊢\left(n=N\wedge k=K\right)\to ⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}⟩=⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩$$
32	8 31	preq12d	$$⊢\left(n=N\wedge k=K\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}$$
33		fvoveq1	$$⊢n=N\to ⌈\frac{n}{2}⌉=⌈\frac{N}{2}⌉$$
34	33	oveq2d	$$⊢n=N\to \left(1..^⌈\frac{n}{2}⌉\right)=\left(1..^⌈\frac{N}{2}⌉\right)$$
35	34 1	eqtr4di	$$⊢n=N\to \left(1..^⌈\frac{n}{2}⌉\right)=J$$
36		df-gpg	Could not format 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 ) >. } ) } ) >. } ) : No typesetting found for |- 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 ) >. } ) } ) >. } ) with typecode |-
37	32 35 36	ovmpox	Could not format ( ( N e. NN /\ K e. J /\ { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } e. _V ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) : No typesetting found for |- ( ( N e. NN /\ K e. J /\ { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } e. _V ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) with typecode |-
38	3 37	mp3an3	Could not format ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) with typecode |-