Theorem gpgedg

Description: The edges of 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	gpgedg	Could not format assertion : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { 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		edgval	Could not format ( Edg ` ( N gPetersenGr K ) ) = ran ( iEdg ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Edg ` ( N gPetersenGr K ) ) = ran ( iEdg ` ( N gPetersenGr K ) ) with typecode |-
4	1 2	gpgiedg	Could not format ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _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 ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _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 |-
5	4	rneqd	Could not format ( ( N e. NN /\ K e. J ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = ran ( _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 ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = ran ( _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 |-
6		rnresi	$$⊢\mathrm{ran}\left({\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)=\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\}$$
7	5 6	eqtrdi	Could not format ( ( N e. NN /\ K e. J ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = { 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 ) -> ran ( iEdg ` ( N gPetersenGr K ) ) = { 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 |-
8	3 7	eqtrid	Could not format ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { 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 ) -> ( Edg ` ( N gPetersenGr K ) ) = { 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 |-