let p be Prime; for a, b being Element of (GF p) holds
( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) )
let a, b be Element of (GF p); ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) )
set P = [0,1,0];
hereby (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p)
[0,1,0] <> [0,0,0]
by MCART_1:25;
then P0:
not
[0,1,0] in {[0,0,0]}
by TARSKI:def 1;
P1:
0 in the
carrier of
(GF p)
by NAT_1:44;
1. (GF p) in the
carrier of
(GF p)
;
then
1
in the
carrier of
(GF p)
by XLm3;
then
[0,1,0] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
by P1, MCART_1:69;
then
[0,1,0] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
by P0, XBOOLE_0:def 5;
hence
[0,1,0] is
Element of
ProjCo (GF p)
by GFProjCo;
verum
end;
then reconsider P = [0,1,0] as Element of ProjCo (GF p) ;
set Px = P `1 ;
set Py = P `2 ;
set Pz = P `3 ;
P3: P =
[(0. (GF p)),1,0]
by XLm2
.=
[(0. (GF p)),(1. (GF p)),0]
by XLm3
.=
[(0. (GF p)),(1. (GF p)),(0. (GF p))]
by XLm2
;
then P4:
P `1 = 0. (GF p)
by MCART_1:43;
P6:
P `3 = 0. (GF p)
by P3, MCART_1:43;
P7: (P `1) |^ 3 =
(P `1) |^ (2 + 1)
.=
((P `1) |^ 2) * (P `1)
by EX5
.=
0. (GF p)
by P4, VECTSP_1:12
;
P8: (P `3) |^ 3 =
(P `3) |^ (2 + 1)
.=
((P `3) |^ 2) * (P `3)
by EX5
.=
0. (GF p)
by P6, VECTSP_1:12
;
P9: (P `3) |^ 2 =
(P `3) |^ (1 + 1)
.=
((P `3) |^ 1) * (P `3)
by EX5
.=
0. (GF p)
by P6, VECTSP_1:12
;
(EC_WEqProjCo (a,b,p)) . P =
(((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))
by ECDefEQ
.=
(0. (GF p)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))
by P6, VECTSP_1:12
.=
- (((0. (GF p)) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))
by P7, RLVECT_1:4
.=
- (((a * (P `1)) * ((P `3) |^ 2)) + (b * ((P `3) |^ 3)))
by RLVECT_1:4
.=
- ((0. (GF p)) + (b * ((P `3) |^ 3)))
by P9, VECTSP_1:12
.=
- (b * ((P `3) |^ 3))
by RLVECT_1:4
.=
- (0. (GF p))
by P8, VECTSP_1:12
.=
(0. (GF p)) - (0. (GF p))
by RLVECT_1:4
;
hence
(EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p)
by VECTSP_1:19; verum