Theorem gpgiedgdmel

Description: An index of edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 2-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 |-
Assertion	gpgiedgdmel	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\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	3	fveq2i	Could not format ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr K ) ) : No typesetting found for |- ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr K ) ) with typecode |-
5	2 1	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 |-
6	4 5	eqtrid	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \mathrm{iEdg}\left(G\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\}}$$
7	6	dmeqd	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \mathrm{dom}\mathrm{iEdg}\left(G\right)=\mathrm{dom}\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)$$
8	7	eleq2d	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow X\in \mathrm{dom}\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)\right)$$
9		dmresi	$$⊢\mathrm{dom}\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\}$$
10	9	a1i	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \mathrm{dom}\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\}$$
11	10	eleq2d	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(X\in \mathrm{dom}\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)\leftrightarrow X\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)$$
12		eqeq1	$$⊢e=X\to \left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
13		eqeq1	$$⊢e=X\to \left(e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
14		eqeq1	$$⊢e=X\to \left(e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\leftrightarrow X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)$$
15	12 13 14	3orbi123d	$$⊢e=X\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(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
16	15	rexbidv	$$⊢e=X\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(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
17	16	elrab	$$⊢X\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(X\in 𝒫\left(\left\{0,1\right\}\times I\right)\wedge \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
18	1 2	gpgiedgdmellem	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(\exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\to X\in 𝒫\left(\left\{0,1\right\}\times I\right)\right)$$
19	18	pm4.71rd	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(\exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(X\in 𝒫\left(\left\{0,1\right\}\times I\right)\wedge \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
20	17 19	bitr4id	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(X\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(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$
21	8 11 20	3bitrd	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right)$$