set a = z `1 ;
set b = z `2 ;
defpred S1[ Element of EC_SetProjCo ((z `1),(z `2),p), Element of EC_SetProjCo ((z `1),(z `2),p), set ] means for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( $1 _EQ_ O implies $3 = $2 ) & ( $2 _EQ_ O & not $1 _EQ_ O implies $3 = $1 ) & ( not $1 _EQ_ O & not $2 _EQ_ O & not $1 _EQ_ $2 implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = (($2 `2_3) * ($1 `3_3)) - (($1 `2_3) * ($2 `3_3)) & gf2 = (($2 `1_3) * ($1 `3_3)) - (($1 `1_3) * ($2 `3_3)) & gf3 = ((((gf1 |^ 2) * ($1 `3_3)) * ($2 `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * ($1 `1_3)) * ($2 `3_3)) holds
$3 = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * ($1 `1_3)) * ($2 `3_3)) - gf3)) - (((gf2 |^ 3) * ($1 `2_3)) * ($2 `3_3))),(((gf2 |^ 3) * ($1 `3_3)) * ($2 `3_3))] ) & ( not $1 _EQ_ O & not $2 _EQ_ O & $1 _EQ_ $2 implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * (($1 `3_3) |^ 2)) + (g3 * (($1 `1_3) |^ 2)) & gf2 = ($1 `2_3) * ($1 `3_3) & gf3 = (($1 `1_3) * ($1 `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
$3 = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * (($1 `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) );
for o1, o2 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st ( for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o1 . (P,Q)] ) & ( for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o2 . (P,Q)] ) holds
o1 = o2
proof
let o1, o2 be Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)); :: thesis: ( ( for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o1 . (P,Q)] ) & ( for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o2 . (P,Q)] ) implies o1 = o2 )
assume that
A65: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o1 . (P,Q)] and
A66: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,o2 . (P,Q)] ; :: thesis: o1 = o2
set O = [0,1,0];
reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds o1 . (P,Q) = o2 . (P,Q)
proof
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: o1 . (P,Q) = o2 . (P,Q)
per cases ( P _EQ_ O or ( Q _EQ_ O & not P _EQ_ O ) or ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) or ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) ) ;
suppose A67: P _EQ_ O ; :: thesis: o1 . (P,Q) = o2 . (P,Q)
o1 . (P,Q) = Q by A65, A67;
hence o1 . (P,Q) = o2 . (P,Q) by A66, A67; :: thesis: verum
end;
suppose A68: ( Q _EQ_ O & not P _EQ_ O ) ; :: thesis: o1 . (P,Q) = o2 . (P,Q)
o1 . (P,Q) = P by A65, A68;
hence o1 . (P,Q) = o2 . (P,Q) by A66, A68; :: thesis: verum
end;
suppose A69: ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) ; :: thesis: o1 . (P,Q) = o2 . (P,Q)
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
set gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3));
set gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3));
set gf3 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3));
reconsider gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)), gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)), gf3 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3)) as Element of (GF p) ;
o1 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] by A65, A69;
hence o1 . (P,Q) = o2 . (P,Q) by A66, A69; :: thesis: verum
end;
suppose A70: ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) ; :: thesis: o1 . (P,Q) = o2 . (P,Q)
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g3 = 3 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g4 = 4 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g8 = 8 mod p as Element of (GF p) by EC_PF_1:14;
set gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2));
set gf2 = (P `2_3) * (P `3_3);
set gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3));
set gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))));
reconsider gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)), gf2 = (P `2_3) * (P `3_3), gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)), gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))) as Element of (GF p) ;
o1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] by A65, A70;
hence o1 . (P,Q) = o2 . (P,Q) by A66, A70; :: thesis: verum
end;
end;
end;
hence o1 = o2 by BINOP_1:2; :: thesis: verum
end;
hence for b1, b2 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b1 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b1 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b1 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) & ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b2 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b2 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b2 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b2 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) holds
b1 = b2 ; :: thesis: verum