Metamath Proof Explorer

Theorem gpgedgel

Description: An edge in a generalized Petersen graph G . (Contributed by AV, 29-Aug-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 prex 
 |-  { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. _V
20 19 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. _V )
21 c0ex 
 |-  0 e. _V
22 21 prid1 
 |-  0 e. { 0 , 1 }
23 22 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> 0 e. { 0 , 1 } )
24 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> x e. I )
25 23 24 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> <. 0 , x >. e. ( { 0 , 1 } X. I ) )
26 elfzoelz 
 |-  ( x e. ( 0 ..^ N ) -> x e. ZZ )
27 26 1 eleq2s 
 |-  ( x e. I -> x e. ZZ )
28 27 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> x e. ZZ )
29 28 peano2zd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( x + 1 ) e. ZZ )
30 8 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. NN )
31 30 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> N e. NN )
32 zmodfzo 
 |-  ( ( ( x + 1 ) e. ZZ /\ N e. NN ) -> ( ( x + 1 ) mod N ) e. ( 0 ..^ N ) )
33 29 31 32 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( ( x + 1 ) mod N ) e. ( 0 ..^ N ) )
34 33 1 eleqtrrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( ( x + 1 ) mod N ) e. I )
35 23 34 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> <. 0 , ( ( x + 1 ) mod N ) >. e. ( { 0 , 1 } X. I ) )
36 25 35 prssd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } C_ ( { 0 , 1 } X. I ) )
37 20 36 elpwd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) )
38 eleq1 
 |-  ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } -> ( Y e. ~P ( { 0 , 1 } X. I ) <-> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) ) )
39 37 38 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
40 prex 
 |-  { <. 0 , x >. , <. 1 , x >. } e. _V
41 40 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } e. _V )
42 1ex 
 |-  1 e. _V
43 42 prid2 
 |-  1 e. { 0 , 1 }
44 43 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> 1 e. { 0 , 1 } )
45 44 24 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> <. 1 , x >. e. ( { 0 , 1 } X. I ) )
46 25 45 prssd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } C_ ( { 0 , 1 } X. I ) )
47 41 46 elpwd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } e. ~P ( { 0 , 1 } X. I ) )
48 eleq1 
 |-  ( Y = { <. 0 , x >. , <. 1 , x >. } -> ( Y e. ~P ( { 0 , 1 } X. I ) <-> { <. 0 , x >. , <. 1 , x >. } e. ~P ( { 0 , 1 } X. I ) ) )
49 47 48 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( Y = { <. 0 , x >. , <. 1 , x >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
50 prex 
 |-  { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. _V
51 50 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. _V )
52 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
53 52 2 eleq2s 
 |-  ( K e. J -> K e. ZZ )
54 53 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. ZZ )
55 54 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> K e. ZZ )
56 28 55 zaddcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( x + K ) e. ZZ )
57 zmodfzo 
 |-  ( ( ( x + K ) e. ZZ /\ N e. NN ) -> ( ( x + K ) mod N ) e. ( 0 ..^ N ) )
58 56 31 57 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( ( x + K ) mod N ) e. ( 0 ..^ N ) )
59 58 1 eleqtrrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( ( x + K ) mod N ) e. I )
60 44 59 opelxpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> <. 1 , ( ( x + K ) mod N ) >. e. ( { 0 , 1 } X. I ) )
61 45 60 prssd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } C_ ( { 0 , 1 } X. I ) )
62 51 61 elpwd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) )
63 eleq1 
 |-  ( Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } -> ( Y e. ~P ( { 0 , 1 } X. I ) <-> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) ) )
64 62 63 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ x e. I ) -> ( Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
65 39 49 64 3jaod 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ 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 ) ) )
66 65 rexlimdva 
 |-  ( ( 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 ) ) )
67 66 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 ) >. } ) ) ) )
68 18 67 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 ) >. } ) ) )
69 12 68 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 ) >. } ) ) )