let p be Prime; :: thesis: for a, b being Element of (GF p)
for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) holds
Q in EC_SetProjCo (a,b,p)
let a, b be Element of (GF p); :: thesis: for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) holds
Q in EC_SetProjCo (a,b,p)
let P, Q be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; :: thesis: for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) holds
Q in EC_SetProjCo (a,b,p)
let d be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) implies Q in EC_SetProjCo (a,b,p) )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) ) ; :: thesis: Q in EC_SetProjCo (a,b,p)
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
consider PP being Element of ProjCo (GF p) such that
P1: ( P = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) by AS;
P2: (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;
P4: (EC_WEqProjCo (a,b,p)) . Q = (((d * (P `2)) |^ 2) * (d * (P `3))) - ((((d * (P `1)) |^ 3) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by AS, ECDefEQ
.= (((d |^ 2) * ((P `2) |^ 2)) * (d * (P `3))) - ((((d * (P `1)) |^ 3) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by EX9
.= ((((d |^ 2) * ((P `2) |^ 2)) * d) * (P `3)) - ((((d * (P `1)) |^ 3) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= ((((d |^ 2) * d) * ((P `2) |^ 2)) * (P `3)) - ((((d * (P `1)) |^ 3) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= (((d |^ (2 + 1)) * ((P `2) |^ 2)) * (P `3)) - ((((d * (P `1)) |^ 3) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by EX5
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + ((a * (d * (P `1))) * ((d * (P `3)) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by EX9
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + ((a * (d * (P `1))) * ((d |^ 2) * ((P `3) |^ 2)))) + (b * ((d * (P `3)) |^ 3))) by EX9
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + (((a * (d * (P `1))) * (d |^ 2)) * ((P `3) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + ((a * ((d * (P `1)) * (d |^ 2))) * ((P `3) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + ((a * (((d |^ 2) * d) * (P `1))) * ((P `3) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + ((a * ((d |^ (2 + 1)) * (P `1))) * ((P `3) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by EX5
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + (((d |^ 3) * (a * (P `1))) * ((P `3) |^ 2))) + (b * ((d * (P `3)) |^ 3))) by GROUP_1:def 3
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + (((d |^ 3) * (a * (P `1))) * ((P `3) |^ 2))) + (b * ((d |^ 3) * ((P `3) |^ 3)))) by EX9
.= (((d |^ 3) * ((P `2) |^ 2)) * (P `3)) - ((((d |^ 3) * ((P `1) |^ 3)) + (((d |^ 3) * (a * (P `1))) * ((P `3) |^ 2))) + (((d |^ 3) * b) * ((P `3) |^ 3))) by GROUP_1:def 3
.= ((d |^ 3) * (((P `2) |^ 2) * (P `3))) - ((((d |^ 3) * ((P `1) |^ 3)) + (((d |^ 3) * (a * (P `1))) * ((P `3) |^ 2))) + (((d |^ 3) * b) * ((P `3) |^ 3))) by GROUP_1:def 3
.= ((d |^ 3) * (((P `2) |^ 2) * (P `3))) - ((((d |^ 3) * ((P `1) |^ 3)) + ((d |^ 3) * ((a * (P `1)) * ((P `3) |^ 2)))) + (((d |^ 3) * b) * ((P `3) |^ 3))) by GROUP_1:def 3
.= ((d |^ 3) * (((P `2) |^ 2) * (P `3))) - ((((d |^ 3) * ((P `1) |^ 3)) + ((d |^ 3) * ((a * (P `1)) * ((P `3) |^ 2)))) + ((d |^ 3) * (b * ((P `3) |^ 3)))) by GROUP_1:def 3
.= ((d |^ 3) * (((P `2) |^ 2) * (P `3))) - (((d |^ 3) * (((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2)))) + ((d |^ 3) * (b * ((P `3) |^ 3)))) by VECTSP_1:4
.= ((d |^ 3) * (((P `2) |^ 2) * (P `3))) - ((d |^ 3) * ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))) by VECTSP_1:4
.= (d |^ 3) * ((((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))) by VECTSP_1:11
.= 0. (GF p) by P1, P2, VECTSP_1:12 ;
PP in ProjCo (GF p) ;
then PP in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by GFProjCo;
then P5: not P in {[0,0,0]} by P1, XBOOLE_0:def 5;
P6: Q = [(Q `1),(Q `2),(Q `3)] by MCART_1:44;
( P `1 <> 0 or P `2 <> 0 or P `3 <> 0 )

proof

assume ( not P `1 <> 0 & not P `2 <> 0 & not P `3 <> 0 ) ; :: thesis: contradiction
then P = [0,0,0] by MCART_1:44;
hence contradiction by P5, TARSKI:def 1; :: thesis: verum

end;

then ( P `1 <> 0. (GF p) or P `2 <> 0. (GF p) or P `3 <> 0. (GF p) ) by XLm2;
then ( d * (P `1) <> 0. (GF p) or d * (P `2) <> 0. (GF p) or d * (P `3) <> 0. (GF p) ) by AS, VECTSP_1:12;
then ( Q `1 <> 0 or Q `2 <> 0 or Q `3 <> 0 ) by AS, XLm2;
then [(Q `1),(Q `2),(Q `3)] <> [0,0,0] by MCART_1:25;
then not Q in {[0,0,0]} by P6, TARSKI:def 1;
then Q in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by XBOOLE_0:def 5;
then Q in ProjCo (GF p) by GFProjCo;
hence Q in EC_SetProjCo (a,b,p) by P4; :: thesis: verum