Theorem gpgedgel

Description: An edge in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025) (Proof shortened by AV, 8-Nov-2025)

	Ref	Expression
Hypotheses	gpgvtxel.i	$$⊢I=\left(0..^N\right)$$
	gpgvtxel.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgvtxel.g	No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
	gpgedgel.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	gpgedgel	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(Y\in E\leftrightarrow \exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	$$⊢I=\left(0..^N\right)$$
2		gpgvtxel.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
3		gpgvtxel.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
4		gpgedgel.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
5	3	fveq2i	Could not format ( Edg ` G ) = ( Edg ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Edg ` G ) = ( Edg ` ( N gPetersenGr K ) ) with typecode |-
6	4 5	eqtri	Could not format E = ( Edg ` ( N gPetersenGr K ) ) : No typesetting found for |- E = ( Edg ` ( N gPetersenGr K ) ) with typecode |-
7	6	eleq2i	Could not format ( Y e. E <-> Y e. ( Edg ` ( N gPetersenGr K ) ) ) : No typesetting found for |- ( Y e. E <-> Y e. ( Edg ` ( N gPetersenGr K ) ) ) with typecode |-
8		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
9	2 1	gpgedg	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 |-
10	8 9	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ 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. ( ZZ>= ` 3 ) /\ 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 |-
11	10	eleq2d	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. ( Edg ` ( N gPetersenGr K ) ) <-> Y e. { 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. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. ( Edg ` ( N gPetersenGr K ) ) <-> Y e. { 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 |-
12	7 11	bitrid	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(Y\in E\leftrightarrow Y\in \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)$$
13		eqeq1	$$⊢e=Y\to \left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
14		eqeq1	$$⊢e=Y\to \left(e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
15		eqeq1	$$⊢e=Y\to \left(e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\leftrightarrow Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)$$
16	13 14 15	3orbi123d	$$⊢e=Y\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(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
17	16	rexbidv	$$⊢e=Y\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(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
18	17	elrab	$$⊢Y\in \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\}\leftrightarrow \left(Y\in 𝒫\left(\left\{0,1\right\}\times I\right)\wedge \exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
19	8	anim1i	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(N\in \mathbb{N}\wedge K\in J\right)$$
20	1 2	gpgiedgdmellem	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(\exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\to Y\in 𝒫\left(\left\{0,1\right\}\times I\right)\right)$$
21	19 20	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(\exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\to Y\in 𝒫\left(\left\{0,1\right\}\times I\right)\right)$$
22	21	pm4.71rd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(\exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(Y\in 𝒫\left(\left\{0,1\right\}\times I\right)\wedge \exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
23	18 22	bitr4id	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(Y\in \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\}\leftrightarrow \exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
24	12 23	bitrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(Y\in E\leftrightarrow \exists x\in I\left(Y=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee Y=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee Y=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$