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