Metamath Proof Explorer

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 = ( 0 ..^ N )
gpgvtxel.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgvtxel.g 
|- G = ( N gPetersenGr K )
gpgedgel.e 
|- E = ( Edg ` G )
Assertion gpgedgel 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. E <-> E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 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 gpgedgel.e 
 |-  E = ( Edg ` G )
5 3 fveq2i 
 |-  ( Edg ` G ) = ( Edg ` ( N gPetersenGr K ) )
6 4 5 eqtri 
 |-  E = ( Edg ` ( N gPetersenGr K ) )
7 6 eleq2i 
 |-  ( Y e. E <-> Y e. ( Edg ` ( N gPetersenGr K ) ) )
8 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
9 2 1 gpgedg 
 |-  ( ( 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 ) >. } ) } )
10 8 9 sylan 
 |-  ( ( 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 ) >. } ) } )
11 10 eleq2d 
 |-  ( ( 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 ) >. } ) } ) )
12 7 11 bitrid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. E <-> 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 ) >. } ) } ) )
13 eqeq1 
 |-  ( e = Y -> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
14 eqeq1 
 |-  ( e = Y -> ( e = { <. 0 , x >. , <. 1 , x >. } <-> Y = { <. 0 , x >. , <. 1 , x >. } ) )
15 eqeq1 
 |-  ( e = Y -> ( e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
16 13 14 15 3orbi123d 
 |-  ( e = Y -> ( ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
17 16 rexbidv 
 |-  ( e = Y -> ( 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 ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
18 17 elrab 
 |-  ( 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 ) >. } ) } <-> ( Y e. ~P ( { 0 , 1 } X. I ) /\ E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
19 8 anim1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( N e. NN /\ K e. J ) )
20 1 2 gpgiedgdmellem 
 |-  ( ( N e. NN /\ K e. J ) -> ( E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) -> Y e. ~P ( { 0 , 1 } X. I ) ) )
21 19 20 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) -> Y e. ~P ( { 0 , 1 } X. I ) ) )
22 21 pm4.71rd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( Y e. ~P ( { 0 , 1 } X. I ) /\ E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) ) )
23 18 22 bitr4id 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 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 ) >. } ) } <-> E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
24 12 23 bitrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. E <-> E. x e. I ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ Y = { <. 0 , x >. , <. 1 , x >. } \/ Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )