let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p

for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds

( P `3_3 = 0 iff P _EQ_ O )

let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds

( P `3_3 = 0 iff P _EQ_ O )

let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( P `3_3 = 0 iff P _EQ_ O ) )

assume A2: O = [0,1,0] ; :: thesis: ( P `3_3 = 0 iff P _EQ_ O )

set a = z `1 ;

set b = z `2 ;

consider PP being Element of ProjCo (GF p) such that

A3: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;

then rep_pt P = rep_pt O by EC_PF_2:39

.= O by A2, ThRepPoint5 ;

then (rep_pt PP) `3_3 = 0 by A2, A3, MCART_1:def 7;

then PP `3_3 = 0 by EC_PF_2:37;

hence P `3_3 = 0 by A3, EC_PF_2:32; :: thesis: verum

for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds

( P `3_3 = 0 iff P _EQ_ O )

let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds

( P `3_3 = 0 iff P _EQ_ O )

let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( P `3_3 = 0 iff P _EQ_ O ) )

assume A2: O = [0,1,0] ; :: thesis: ( P `3_3 = 0 iff P _EQ_ O )

set a = z `1 ;

set b = z `2 ;

consider PP being Element of ProjCo (GF p) such that

A3: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;

hereby :: thesis: ( P _EQ_ O implies P `3_3 = 0 )

assume
P _EQ_ O
; :: thesis: P `3_3 = 0 assume
P `3_3 = 0
; :: thesis: P _EQ_ O

then PP `3_3 = 0 by A3, EC_PF_2:32;

then A5: rep_pt P = [0,1,0] by A3, EC_PF_2:def 7;

rep_pt O = [0,1,0] by A2, ThRepPoint5;

hence P _EQ_ O by A5, EC_PF_2:39; :: thesis: verum

end;then PP `3_3 = 0 by A3, EC_PF_2:32;

then A5: rep_pt P = [0,1,0] by A3, EC_PF_2:def 7;

rep_pt O = [0,1,0] by A2, ThRepPoint5;

hence P _EQ_ O by A5, EC_PF_2:39; :: thesis: verum

then rep_pt P = rep_pt O by EC_PF_2:39

.= O by A2, ThRepPoint5 ;

then (rep_pt PP) `3_3 = 0 by A2, A3, MCART_1:def 7;

then PP `3_3 = 0 by EC_PF_2:37;

hence P `3_3 = 0 by A3, EC_PF_2:32; :: thesis: verum