let p be Prime; for a, b, d1, Y1, d2, Y2 being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) holds
( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) )
let a, b, d1, Y1, d2, Y2 be Element of (GF p); ( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) implies ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) )
assume AS:
( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) )
; ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) )
hereby ( d1 = d2 & Y1 = Y2 implies Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) )
assume
Class (
(R_EllCur (a,b,p)),
[d1,Y1,1])
= Class (
(R_EllCur (a,b,p)),
[d2,Y2,1])
;
( d2 = d1 & Y2 = Y1 )then
[d2,Y2,1] in Class (
(R_EllCur (a,b,p)),
[d1,Y1,1])
by AS, EQREL_1:23;
then P07:
[[d1,Y1,1],[d2,Y2,1]] in R_EllCur (
a,
b,
p)
by EQREL_1:18;
reconsider P =
[d1,Y1,1],
Q =
[d2,Y2,1] as
Element of
ProjCo (GF p) by AS;
P _EQ_ Q
by LmDefREQ0, AS, P07;
then consider a being
Element of
(GF p) such that P08:
(
a <> 0. (GF p) &
Q `1 = a * (P `1) &
Q `2 = a * (P `2) &
Q `3 = a * (P `3) )
by DefEQV;
PP1:
p > 1
by INT_2:def 4;
P09:
1. (GF p) =
1
by PP1, INT_3:14
.=
P `3
by MCART_1:43
;
P10:
1. (GF p) =
1
by PP1, INT_3:14
.=
a * (P `3)
by P08, MCART_1:43
.=
a
by P09, VECTSP_1:def 8
;
thus d2 =
a * (P `1)
by P08, MCART_1:43
.=
P `1
by P10, VECTSP_1:def 8
.=
d1
by MCART_1:43
;
Y2 = Y1thus Y2 =
a * (P `2)
by P08, MCART_1:43
.=
P `2
by P10, VECTSP_1:def 8
.=
Y1
by MCART_1:43
;
verum
end;
assume
( d1 = d2 & Y1 = Y2 )
; Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1])
hence
Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1])
; verum