Metamath Proof Explorer

Theorem gpgiedgdmellem

Description: Lemma for gpgiedgdmel and gpgedgel . (Contributed by AV, 2-Nov-2025)

Ref Expression
Hypotheses gpgvtxel.i 
|- I = ( 0 ..^ N )
gpgvtxel.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 gpgvtxel.i 
 |-  I = ( 0 ..^ N )
2 gpgvtxel.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
3 prex 
 |-  { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. _V
4 3 a1i 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. _V )
5 0elpr01 
 |-  0 e. { 0 , 1 }
6 5 a1i 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> 0 e. { 0 , 1 } )
7 simpr 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> x e. I )
8 6 7 opelxpd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> <. 0 , x >. e. ( { 0 , 1 } X. I ) )
9 elfzoelz 
 |-  ( x e. ( 0 ..^ N ) -> x e. ZZ )
10 9 1 eleq2s 
 |-  ( x e. I -> x e. ZZ )
11 10 adantl 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> x e. ZZ )
12 11 peano2zd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( x + 1 ) e. ZZ )
13 simpll 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> N e. NN )
14 zmodfzo 
 |-  ( ( ( x + 1 ) e. ZZ /\ N e. NN ) -> ( ( x + 1 ) mod N ) e. ( 0 ..^ N ) )
15 12 13 14 syl2anc 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( ( x + 1 ) mod N ) e. ( 0 ..^ N ) )
16 15 1 eleqtrrdi 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( ( x + 1 ) mod N ) e. I )
17 6 16 opelxpd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> <. 0 , ( ( x + 1 ) mod N ) >. e. ( { 0 , 1 } X. I ) )
18 8 17 prssd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } C_ ( { 0 , 1 } X. I ) )
19 4 18 elpwd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) )
20 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 ) ) )
21 19 20 syl5ibrcom 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( Y = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
22 prex 
 |-  { <. 0 , x >. , <. 1 , x >. } e. _V
23 22 a1i 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } e. _V )
24 1elpr01 
 |-  1 e. { 0 , 1 }
25 24 a1i 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> 1 e. { 0 , 1 } )
26 25 7 opelxpd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> <. 1 , x >. e. ( { 0 , 1 } X. I ) )
27 8 26 prssd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } C_ ( { 0 , 1 } X. I ) )
28 23 27 elpwd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 0 , x >. , <. 1 , x >. } e. ~P ( { 0 , 1 } X. I ) )
29 eleq1 
 |-  ( Y = { <. 0 , x >. , <. 1 , x >. } -> ( Y e. ~P ( { 0 , 1 } X. I ) <-> { <. 0 , x >. , <. 1 , x >. } e. ~P ( { 0 , 1 } X. I ) ) )
30 28 29 syl5ibrcom 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( Y = { <. 0 , x >. , <. 1 , x >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
31 prex 
 |-  { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. _V
32 31 a1i 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. _V )
33 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
34 33 2 eleq2s 
 |-  ( K e. J -> K e. ZZ )
35 34 ad2antlr 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> K e. ZZ )
36 11 35 zaddcld 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( x + K ) e. ZZ )
37 zmodfzo 
 |-  ( ( ( x + K ) e. ZZ /\ N e. NN ) -> ( ( x + K ) mod N ) e. ( 0 ..^ N ) )
38 36 13 37 syl2anc 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( ( x + K ) mod N ) e. ( 0 ..^ N ) )
39 38 1 eleqtrrdi 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( ( x + K ) mod N ) e. I )
40 25 39 opelxpd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> <. 1 , ( ( x + K ) mod N ) >. e. ( { 0 , 1 } X. I ) )
41 26 40 prssd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } C_ ( { 0 , 1 } X. I ) )
42 32 41 elpwd 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } e. ~P ( { 0 , 1 } X. I ) )
43 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 ) ) )
44 42 43 syl5ibrcom 
 |-  ( ( ( N e. NN /\ K e. J ) /\ x e. I ) -> ( Y = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } -> Y e. ~P ( { 0 , 1 } X. I ) ) )
45 21 30 44 3jaod 
 |-  ( ( ( N e. NN /\ 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 ) ) )
46 45 rexlimdva 
 |-  ( ( 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 ) ) )