Metamath Proof Explorer

Theorem pgnbgreunbgrlem2

Description: Lemma 2 for pgnbgreunbgr . Impossible cases. (Contributed by AV, 18-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 pgnbgreunbgrlem2 
|- ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )

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 eqtr3 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) -> L = K )
6 eqneqall 
 |-  ( K = L -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
7 6 impd 
 |-  ( K = L -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
8 7 eqcoms 
 |-  ( L = K -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
9 5 8 syl 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
10 9 a1d 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
11 10 ex 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
12 1ex 
 |-  1 e. _V
13 vex 
 |-  y e. _V
14 12 13 op2ndd 
 |-  ( X = <. 1 , y >. -> ( 2nd ` X ) = y )
15 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) + 2 ) = ( y + 2 ) )
16 15 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) + 2 ) mod 5 ) = ( ( y + 2 ) mod 5 ) )
17 16 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. = <. 1 , ( ( y + 2 ) mod 5 ) >. )
18 17 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. <-> L = <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
19 opeq2 
 |-  ( ( 2nd ` X ) = y -> <. 0 , ( 2nd ` X ) >. = <. 0 , y >. )
20 19 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 0 , ( 2nd ` X ) >. <-> K = <. 0 , y >. ) )
21 18 20 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) <-> ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) ) )
22 14 21 syl 
 |-  ( X = <. 1 , y >. -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) <-> ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) ) )
23 1 2 3 4 pgnbgreunbgrlem2lem1 
 |-  ( ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )
24 23 pm2.21d 
 |-  ( ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> ( { <. 0 , b >. , L } e. E -> X = <. 0 , b >. ) )
25 24 expimpd 
 |-  ( ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
26 25 ex 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
27 26 adantld 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
28 22 27 biimtrdi 
 |-  ( X = <. 1 , y >. -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
29 28 adantr 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
30 29 expdcom 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( K = <. 0 , ( 2nd ` X ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
31 oveq1 
 |-  ( ( 2nd ` X ) = y -> ( ( 2nd ` X ) - 2 ) = ( y - 2 ) )
32 31 oveq1d 
 |-  ( ( 2nd ` X ) = y -> ( ( ( 2nd ` X ) - 2 ) mod 5 ) = ( ( y - 2 ) mod 5 ) )
33 32 opeq2d 
 |-  ( ( 2nd ` X ) = y -> <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. = <. 1 , ( ( y - 2 ) mod 5 ) >. )
34 33 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. <-> K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) )
35 18 34 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
36 14 35 syl 
 |-  ( X = <. 1 , y >. -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
37 1 2 3 4 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 )
38 37 pm2.21d 
 |-  ( ( ( ( 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 -> X = <. 0 , b >. ) )
39 38 expimpd 
 |-  ( ( ( 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 ) -> X = <. 0 , b >. ) )
40 39 ex 
 |-  ( ( 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 ) -> X = <. 0 , b >. ) ) )
41 40 adantld 
 |-  ( ( L = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
42 36 41 biimtrdi 
 |-  ( X = <. 1 , y >. -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
43 42 adantr 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
44 43 expdcom 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
45 11 30 44 3jaod 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
46 14 adantr 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( 2nd ` X ) = y )
47 19 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 0 , ( 2nd ` X ) >. <-> L = <. 0 , y >. ) )
48 17 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. <-> K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) )
49 47 48 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) <-> ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) ) )
50 46 49 syl 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) <-> ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) ) )
51 prcom 
 |-  { <. 0 , b >. , L } = { L , <. 0 , b >. }
52 51 eleq1i 
 |-  ( { <. 0 , b >. , L } e. E <-> { L , <. 0 , b >. } e. E )
53 1 2 3 4 pgnbgreunbgrlem2lem1 
 |-  ( ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , K } e. E )
54 prcom 
 |-  { K , <. 0 , b >. } = { <. 0 , b >. , K }
55 54 eleq1i 
 |-  ( { K , <. 0 , b >. } e. E <-> { <. 0 , b >. , K } e. E )
56 pm2.21 
 |-  ( -. { <. 0 , b >. , K } e. E -> ( { <. 0 , b >. , K } e. E -> X = <. 0 , b >. ) )
57 55 56 biimtrid 
 |-  ( -. { <. 0 , b >. , K } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) )
58 53 57 syl 
 |-  ( ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) )
59 58 ex 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 0 , b >. } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
60 52 59 biimtrid 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , b >. , L } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
61 60 impcomd 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
62 61 ex 
 |-  ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
63 62 ancoms 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
64 63 adantld 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
65 50 64 biimtrdi 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
66 65 expdcom 
 |-  ( L = <. 0 , ( 2nd ` X ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
67 eqtr3 
 |-  ( ( K = <. 0 , ( 2nd ` X ) >. /\ L = <. 0 , ( 2nd ` X ) >. ) -> K = L )
68 67 ancoms 
 |-  ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> K = L )
69 68 6 syl 
 |-  ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( K =/= L -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
70 69 impd 
 |-  ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
71 70 a1d 
 |-  ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
72 71 ex 
 |-  ( L = <. 0 , ( 2nd ` X ) >. -> ( K = <. 0 , ( 2nd ` X ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
73 47 34 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
74 46 73 syl 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) <-> ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) ) )
75 1 2 3 4 pgnbgreunbgrlem2lem2 
 |-  ( ( ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , K } e. E )
76 75 57 syl 
 |-  ( ( ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) )
77 76 ex 
 |-  ( ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 0 , b >. } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
78 52 77 biimtrid 
 |-  ( ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , b >. , L } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
79 78 impcomd 
 |-  ( ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
80 79 ex 
 |-  ( ( K = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ L = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
81 80 ancoms 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
82 81 adantld 
 |-  ( ( L = <. 0 , y >. /\ K = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
83 74 82 biimtrdi 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 0 , ( 2nd ` X ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
84 83 expdcom 
 |-  ( L = <. 0 , ( 2nd ` X ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
85 66 72 84 3jaod 
 |-  ( L = <. 0 , ( 2nd ` X ) >. -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
86 33 eqeq2d 
 |-  ( ( 2nd ` X ) = y -> ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. <-> L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) )
87 86 48 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) <-> ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) ) )
88 46 87 syl 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) <-> ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) ) )
89 1 2 3 4 pgnbgreunbgrlem2lem3 
 |-  ( ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , K } e. E )
90 89 57 syl 
 |-  ( ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { L , <. 0 , b >. } e. E ) -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) )
91 90 ex 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { L , <. 0 , b >. } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
92 52 91 biimtrid 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , b >. , L } e. E -> ( { K , <. 0 , b >. } e. E -> X = <. 0 , b >. ) ) )
93 92 impcomd 
 |-  ( ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
94 93 ex 
 |-  ( ( K = <. 1 , ( ( y + 2 ) mod 5 ) >. /\ L = <. 1 , ( ( y - 2 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
95 94 ancoms 
 |-  ( ( 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 ) -> X = <. 0 , b >. ) ) )
96 95 adantld 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( y + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
97 88 96 biimtrdi 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
98 97 expdcom 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
99 86 20 anbi12d 
 |-  ( ( 2nd ` X ) = y -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) <-> ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) ) )
100 46 99 syl 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) <-> ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) ) )
101 1 2 3 4 pgnbgreunbgrlem2lem2 
 |-  ( ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )
102 101 pm2.21d 
 |-  ( ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> ( { <. 0 , b >. , L } e. E -> X = <. 0 , b >. ) )
103 102 expimpd 
 |-  ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
104 103 ex 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
105 104 adantld 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
106 100 105 biimtrdi 
 |-  ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 0 , ( 2nd ` X ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
107 106 expdcom 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( K = <. 0 , ( 2nd ` X ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
108 eqtr3 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> L = K )
109 108 eqcomd 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> K = L )
110 109 7 syl 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
111 110 a1d 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. /\ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) )
112 111 ex 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
113 98 107 112 3jaod 
 |-  ( L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )
114 45 85 113 3jaoi 
 |-  ( ( L = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ L = <. 0 , ( 2nd ` X ) >. \/ L = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( K = <. 1 , ( ( ( 2nd ` X ) + 2 ) mod 5 ) >. \/ K = <. 0 , ( 2nd ` X ) >. \/ K = <. 1 , ( ( ( 2nd ` X ) - 2 ) mod 5 ) >. ) -> ( ( X = <. 1 , y >. /\ X e. V ) -> ( ( K =/= L /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) ) ) )