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 XTUPLE_0:3;
then A1:
not
[0,1,0] in {[0,0,0]}
by TARSKI:def 1;
A2:
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 Th12;
then
[0,1,0] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
by A2, 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 A1, XBOOLE_0:def 5;
hence
[0,1,0] is
Element of
ProjCo (GF p)
by Th40;
verum
end;
then reconsider P = [0,1,0] as Element of ProjCo (GF p) ;
set Px = P `1_3 ;
set Py = P `2_3 ;
set Pz = P `3_3 ;
A6: (P `1_3) |^ 3 =
(P `1_3) |^ (2 + 1)
.=
((P `1_3) |^ 2) * (P `1_3)
by Th24
.=
0. (GF p)
;
A7: (P `3_3) |^ 3 =
(P `3_3) |^ (2 + 1)
.=
((P `3_3) |^ 2) * (P `3_3)
by Th24
.=
0. (GF p)
;
(EC_WEqProjCo (a,b,p)) . P =
(((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))
by Def8
.=
(0. (GF p)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))
.=
- (((0. (GF p)) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))
by A6, RLVECT_1:4
.=
- (((a * (P `1_3)) * ((P `3_3) |^ 2)) + (b * ((P `3_3) |^ 3)))
by RLVECT_1:4
.=
- ((0. (GF p)) + (b * ((P `3_3) |^ 3)))
.=
- (b * ((P `3_3) |^ 3))
by RLVECT_1:4
.=
- (0. (GF p))
by A7
.=
(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