Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem3

Description: Lemma 3 for pgnbgreunbgrlem2 . (Contributed by AV, 17-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g 
|- G = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v 
|- V = ( Vtx ` G )
pgnbgreunbgr.e 
|- E = ( Edg ` G )
pgnbgreunbgr.n 
|- N = ( G NeighbVtx X )
Assertion pgnbgreunbgrlem2lem3 
|- ( ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v 
 |-  V = ( Vtx ` G )
3 pgnbgreunbgr.e 
 |-  E = ( Edg ` G )
4 pgnbgreunbgr.n 
 |-  N = ( G NeighbVtx X )
5 prcom 
 |-  { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } = { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. }
6 5 eleq1i 
 |-  ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E <-> { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
7 6 a1i 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E <-> { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
8 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
9 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
10 8 9 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
11 c0ex 
 |-  0 e. _V
12 vex 
 |-  b e. _V
13 11 12 op1st 
 |-  ( 1st ` <. 0 , b >. ) = 0
14 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
15 14 1 2 3 gpgvtxedg0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 0 , b >. ) = 0 /\ { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
16 10 13 15 mp3an12 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E -> ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
17 7 16 biimtrdi 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E -> ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) )
18 14 1 2 3 gpgvtxedg0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 0 , b >. ) = 0 /\ { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) -> ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
19 10 13 18 mp3an12 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E -> ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
20 1ex 
 |-  1 e. _V
21 ovex 
 |-  ( ( y + 2 ) mod 5 ) e. _V
22 20 21 opth 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y + 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) )
23 ax-1ne0 
 |-  1 =/= 0
24 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
25 23 24 mpi 
 |-  ( 1 = 0 -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
26 25 adantr 
 |-  ( ( 1 = 0 /\ ( ( y + 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
27 22 26 sylbi 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
28 20 21 opth 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. <-> ( 1 = 1 /\ ( ( y + 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) ) )
29 11 12 op2nd 
 |-  ( 2nd ` <. 0 , b >. ) = b
30 29 eqeq2i 
 |-  ( ( ( y + 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) <-> ( ( y + 2 ) mod 5 ) = b )
31 ovex 
 |-  ( ( y - 2 ) mod 5 ) e. _V
32 20 31 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) )
33 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) ) )
34 23 33 mpi 
 |-  ( 1 = 0 -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
35 34 adantr 
 |-  ( ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
36 32 35 sylbi 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
37 20 31 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. <-> ( 1 = 1 /\ ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) ) )
38 29 eqeq2i 
 |-  ( ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) <-> ( ( y - 2 ) mod 5 ) = b )
39 eqeq2 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( ( ( y + 2 ) mod 5 ) = b <-> ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
40 39 eqcoms 
 |-  ( ( ( y - 2 ) mod 5 ) = b -> ( ( ( y + 2 ) mod 5 ) = b <-> ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
41 40 adantl 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ ( ( y - 2 ) mod 5 ) = b ) -> ( ( ( y + 2 ) mod 5 ) = b <-> ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
42 elfzoelz 
 |-  ( y e. ( 0 ..^ 5 ) -> y e. ZZ )
43 2z 
 |-  2 e. ZZ
44 43 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> 2 e. ZZ )
45 42 44 zaddcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y + 2 ) e. ZZ )
46 42 44 zsubcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - 2 ) e. ZZ )
47 5nn 
 |-  5 e. NN
48 47 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> 5 e. NN )
49 difmod0 
 |-  ( ( ( y + 2 ) e. ZZ /\ ( y - 2 ) e. ZZ /\ 5 e. NN ) -> ( ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = 0 <-> ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
50 49 bicomd 
 |-  ( ( ( y + 2 ) e. ZZ /\ ( y - 2 ) e. ZZ /\ 5 e. NN ) -> ( ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = 0 ) )
51 45 46 48 50 syl3anc 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = 0 ) )
52 42 zcnd 
 |-  ( y e. ( 0 ..^ 5 ) -> y e. CC )
53 2cnd 
 |-  ( y e. ( 0 ..^ 5 ) -> 2 e. CC )
54 52 53 53 pnncand 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y + 2 ) - ( y - 2 ) ) = ( 2 + 2 ) )
55 2p2e4 
 |-  ( 2 + 2 ) = 4
56 54 55 eqtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y + 2 ) - ( y - 2 ) ) = 4 )
57 56 oveq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = ( 4 mod 5 ) )
58 57 eqeq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = 0 <-> ( 4 mod 5 ) = 0 ) )
59 4re 
 |-  4 e. RR
60 5rp 
 |-  5 e. RR+
61 0re 
 |-  0 e. RR
62 4pos 
 |-  0 < 4
63 61 59 62 ltleii 
 |-  0 <_ 4
64 4lt5 
 |-  4 < 5
65 modid 
 |-  ( ( ( 4 e. RR /\ 5 e. RR+ ) /\ ( 0 <_ 4 /\ 4 < 5 ) ) -> ( 4 mod 5 ) = 4 )
66 59 60 63 64 65 mp4an 
 |-  ( 4 mod 5 ) = 4
67 66 eqeq1i 
 |-  ( ( 4 mod 5 ) = 0 <-> 4 = 0 )
68 4ne0 
 |-  4 =/= 0
69 68 a1i 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E -> 4 =/= 0 )
70 69 necon2bi 
 |-  ( 4 = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
71 67 70 sylbi 
 |-  ( ( 4 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
72 58 71 biimtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y + 2 ) - ( y - 2 ) ) mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
73 51 72 sylbid 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
74 73 adantr 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ ( ( y - 2 ) mod 5 ) = b ) -> ( ( ( y + 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
75 41 74 sylbid 
 |-  ( ( y e. ( 0 ..^ 5 ) /\ ( ( y - 2 ) mod 5 ) = b ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
76 75 ex 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 2 ) mod 5 ) = b -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
77 76 adantl 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y - 2 ) mod 5 ) = b -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
78 77 com12 
 |-  ( ( ( y - 2 ) mod 5 ) = b -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
79 38 78 sylbi 
 |-  ( ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
80 37 79 simplbiim 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
81 20 31 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) )
82 34 adantr 
 |-  ( ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
83 81 82 sylbi 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
84 36 80 83 3jaoi 
 |-  ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( ( y + 2 ) mod 5 ) = b -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
85 84 com13 
 |-  ( ( ( y + 2 ) mod 5 ) = b -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
86 85 impd 
 |-  ( ( ( y + 2 ) mod 5 ) = b -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
87 30 86 sylbi 
 |-  ( ( ( y + 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
88 28 87 simplbiim 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
89 20 21 opth 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y + 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) )
90 25 adantr 
 |-  ( ( 1 = 0 /\ ( ( y + 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
91 89 90 sylbi 
 |-  ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
92 27 88 91 3jaoi 
 |-  ( ( <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y + 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
93 19 92 syl 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
94 ax-1 
 |-  ( -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
95 93 94 pm2.61i 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
96 95 ex 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
97 17 96 syld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
98 97 adantl 
 |-  ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
99 preq1 
 |-  ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> { K , <. 0 , b >. } = { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } )
100 99 eleq1d 
 |-  ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( { K , <. 0 , b >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E ) )
101 100 adantl 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( { K , <. 0 , b >. } e. E <-> { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E ) )
102 preq2 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } )
103 102 eleq1d 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
104 103 notbid 
 |-  ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. -> ( -. { <. 0 , b >. , L } e. E <-> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
105 104 adantr 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( -. { <. 0 , b >. , L } e. E <-> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
106 101 105 imbi12d 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
107 106 adantr 
 |-  ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) <-> ( { <. 1 , ( ( y - 2 ) mod 5 ) >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) ) )
108 98 107 mpbird 
 |-  ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) )
109 108 imp 
 |-  ( ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )