Metamath Proof Explorer

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 = ( 0 ..^ N )
gpgvtxel.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgvtxel.g 
|- G = ( N gPetersenGr K )
Assertion gpgiedgdmel 
|- ( ( N e. NN /\ K e. J ) -> ( X e. dom ( iEdg ` G ) <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 gpgvtxel.i 
 |-  I = ( 0 ..^ N )
2 gpgvtxel.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
3 gpgvtxel.g 
 |-  G = ( N gPetersenGr K )
4 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr K ) )
5 2 1 gpgiedg 
 |-  ( ( 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 ) >. } ) } ) )
6 4 5 eqtrid 
 |-  ( ( N e. NN /\ K e. J ) -> ( iEdg ` G ) = ( _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 ) >. } ) } ) )
7 6 dmeqd 
 |-  ( ( N e. NN /\ K e. J ) -> dom ( iEdg ` G ) = dom ( _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 ) >. } ) } ) )
8 7 eleq2d 
 |-  ( ( N e. NN /\ K e. J ) -> ( X e. dom ( iEdg ` G ) <-> X e. dom ( _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 ) >. } ) } ) ) )
9 dmresi 
 |-  dom ( _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 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 ) >. } ) }
10 9 a1i 
 |-  ( ( N e. NN /\ K e. J ) -> dom ( _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 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 ) >. } ) } )
11 10 eleq2d 
 |-  ( ( N e. NN /\ K e. J ) -> ( X e. dom ( _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 ) >. } ) } ) <-> X 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 ) >. } ) } ) )
12 eqeq1 
 |-  ( e = X -> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
13 eqeq1 
 |-  ( e = X -> ( e = { <. 0 , x >. , <. 1 , x >. } <-> X = { <. 0 , x >. , <. 1 , x >. } ) )
14 eqeq1 
 |-  ( e = X -> ( e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
15 12 13 14 3orbi123d 
 |-  ( e = X -> ( ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
16 15 rexbidv 
 |-  ( e = X -> ( 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. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
17 16 elrab 
 |-  ( X 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 ) >. } ) } <-> ( X e. ~P ( { 0 , 1 } X. I ) /\ E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
18 1 2 gpgiedgdmellem 
 |-  ( ( N e. NN /\ K e. J ) -> ( E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) -> X e. ~P ( { 0 , 1 } X. I ) ) )
19 18 pm4.71rd 
 |-  ( ( N e. NN /\ K e. J ) -> ( E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( X e. ~P ( { 0 , 1 } X. I ) /\ E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) ) )
20 17 19 bitr4id 
 |-  ( ( N e. NN /\ K e. J ) -> ( X 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 ) >. } ) } <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
21 8 11 20 3bitrd 
 |-  ( ( N e. NN /\ K e. J ) -> ( X e. dom ( iEdg ` G ) <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )