:: EC_PF_1 semantic presentation
begin
definition
let K be Field;
mode Subfield of K -> Field means :Def1: :: EC_PF_1:def 1
( the carrier of it c= the carrier of K & the addF of it = the addF of K || the carrier of it & the multF of it = the multF of K || the carrier of it & 1. it = 1. K & 0. it = 0. K );
existence
ex b1 being Field st
( the carrier of b1 c= the carrier of K & the addF of b1 = the addF of K || the carrier of b1 & the multF of b1 = the multF of K || the carrier of b1 & 1. b1 = 1. K & 0. b1 = 0. K )
proof
take K ; ::_thesis: ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K )
thus ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K ) by RELSET_1:19; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Subfield EC_PF_1:def_1_:_
for K, b2 being Field holds
( b2 is Subfield of K iff ( the carrier of b2 c= the carrier of K & the addF of b2 = the addF of K || the carrier of b2 & the multF of b2 = the multF of K || the carrier of b2 & 1. b2 = 1. K & 0. b2 = 0. K ) );
theorem Th1: :: EC_PF_1:1
for K being Field holds K is Subfield of K
proof
let K be Field; ::_thesis: K is Subfield of K
A1: the addF of K = the addF of K || the carrier of K by RELSET_1:19;
A2: the multF of K = the multF of K || the carrier of K by RELSET_1:19;
( the carrier of K c= the carrier of K & 1. K = 1. K & 0. K = 0. K ) ;
hence K is Subfield of K by A1, A2, Def1; ::_thesis: verum
end;
theorem Th2: :: EC_PF_1:2
for K being Field
for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds
ST is Subfield of K
proof
let K be Field; ::_thesis: for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds
ST is Subfield of K
let ST be non empty doubleLoopStr ; ::_thesis: ( the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated implies ST is Subfield of K )
assume that
A1: the carrier of ST is Subset of the carrier of K and
A2: the addF of ST = the addF of K || the carrier of ST and
A3: the multF of ST = the multF of K || the carrier of ST and
A4: 1. ST = 1. K and
A5: 0. ST = 0. K and
A6: ( ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated ) ; ::_thesis: ST is Subfield of K
set C1 = the carrier of ST;
set AC = the addF of ST;
set MC = the multF of ST;
set d0 = 0. ST;
set d1 = 1. ST;
A7: now__::_thesis:_for_a,_x_being_Element_of_ST_holds_a_*_x_=_the_multF_of_K_._(a,x)
let a, x be Element of ST; ::_thesis: a * x = the multF of K . (a,x)
a * x = the multF of K . [a,x] by A3, FUNCT_1:49;
hence a * x = the multF of K . (a,x) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x,_y_being_Element_of_ST_holds_x_+_y_=_the_addF_of_K_._(x,y)
let x, y be Element of ST; ::_thesis: x + y = the addF of K . (x,y)
x + y = the addF of K . [x,y] by A2, FUNCT_1:49;
hence x + y = the addF of K . (x,y) ; ::_thesis: verum
end;
( ST is Abelian & ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
proof
set MK = the multF of K;
set AK = the addF of K;
hereby :: according to RLVECT_1:def_2 ::_thesis: ( ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
let x, y be Element of ST; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of K by A1, TARSKI:def_3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_3 ::_thesis: ( ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
let x, y, z be Element of ST; ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of K by A1, TARSKI:def_3;
x + (y + z) = the addF of K . (x1,(y + z)) by A8;
then A9: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of K . ((x + y),z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A9, RLVECT_1:def_3; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_4 ::_thesis: ( ST is associative & ST is well-unital & ST is distributive )
let x be Element of ST; ::_thesis: x + (0. ST) = x
reconsider y = x, z = 0. ST as Element of K by A1, TARSKI:def_3;
x + (0. ST) = y + (0. K) by A5, A8;
hence x + (0. ST) = x by RLVECT_1:4; ::_thesis: verum
end;
hereby :: according to GROUP_1:def_3 ::_thesis: ( ST is well-unital & ST is distributive )
let a, b, x be Element of ST; ::_thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of K by A1, TARSKI:def_3;
a * (b * x) = the multF of K . (a,(b * x)) by A7;
then A10: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A10, GROUP_1:def_3; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_6 ::_thesis: ST is distributive
let x be Element of ST; ::_thesis: ( x * (1. ST) = x & (1. ST) * x = x )
reconsider y = x as Element of K by A1, TARSKI:def_3;
( x * (1. ST) = y * (1. K) & (1. ST) * x = (1. K) * y ) by A4, A7;
hence ( x * (1. ST) = x & (1. ST) * x = x ) by VECTSP_1:def_6; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_7 ::_thesis: verum
let a, x, y be Element of ST; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )
reconsider x1 = x, y1 = y, a1 = a as Element of K by A1, TARSKI:def_3;
(x + y) * a = the multF of K . ((x + y),a) by A7;
then (x + y) * a = (x1 + y1) * a1 by A8;
then (x + y) * a = (x1 * a1) + (y1 * a1) by VECTSP_1:def_7;
then (x + y) * a = the addF of K . (( the multF of K . (x1,a1)),(y * a)) by A7;
then A11: (x + y) * a = the addF of K . ((x * a),(y * a)) by A7;
a * (x + y) = the multF of K . (a,(x + y)) by A7;
then a * (x + y) = a1 * (x1 + y1) by A8;
then a * (x + y) = (a1 * x1) + (a1 * y1) by VECTSP_1:def_7;
then a * (x + y) = the addF of K . (( the multF of K . (a,x1)),(a * y)) by A7;
then a * (x + y) = the addF of K . ((a * x),(a * y)) by A7;
hence ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) by A8, A11; ::_thesis: verum
end;
end;
hence ST is Subfield of K by A1, A2, A3, A4, A5, A6, Def1; ::_thesis: verum
end;
registration
let K be Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K;
existence
ex b1 being Subfield of K st b1 is strict
proof
set C1 = [#] K;
A1: ( the addF of K = the addF of K || ([#] K) & the multF of K = the multF of K || ([#] K) ) by RELSET_1:19;
set ST = doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #);
A2: ( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K ) ;
( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )
proof
thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable ::_thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )
proof
let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of K ;
consider v being Element of K such that
A3: x1 + v = 0. K by ALGSTR_0:def_11;
reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A3; ::_thesis: verum
end;
thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative ::_thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )
proof
let x, y be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
reconsider x1 = x, y1 = y as Element of K ;
( x * y = x1 * y1 & y * x = y1 * x1 ) ;
hence x * y = y * x ; ::_thesis: verum
end;
thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible ::_thesis: not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated
proof
let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to VECTSP_1:def_9 ::_thesis: ( x = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) or ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) )
assume A4: x <> 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; ::_thesis: ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
reconsider x1 = x as Element of K ;
x1 is left_invertible by A4, ALGSTR_0:def_39;
then consider v being Element of K such that
A5: v * x1 = 1. K by ALGSTR_0:def_27;
reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ;
take y ; ::_thesis: y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A5; ::_thesis: verum
end;
( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K & 0. K <> 1. K ) ;
hence not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated by STRUCT_0:def_8; ::_thesis: verum
end;
then doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is Subfield of K by A1, A2, Th2;
hence ex b1 being Subfield of K st b1 is strict ; ::_thesis: verum
end;
end;
theorem Th3: :: EC_PF_1:3
for K1, K2 being Field st K1 is Subfield of K2 holds
for x being set st x in K1 holds
x in K2
proof
let K1, K2 be Field; ::_thesis: ( K1 is Subfield of K2 implies for x being set st x in K1 holds
x in K2 )
assume K1 is Subfield of K2 ; ::_thesis: for x being set st x in K1 holds
x in K2
then A1: the carrier of K1 c= the carrier of K2 by Def1;
for x being set st x in K1 holds
x in K2
proof
let x be set ; ::_thesis: ( x in K1 implies x in K2 )
assume x in K1 ; ::_thesis: x in K2
then x in the carrier of K1 by STRUCT_0:def_5;
hence x in K2 by A1, STRUCT_0:def_5; ::_thesis: verum
end;
hence for x being set st x in K1 holds
x in K2 ; ::_thesis: verum
end;
theorem Th4: :: EC_PF_1:4
for K1, K2 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K1 holds
K1 = K2
proof
let K1, K2 be strict Field; ::_thesis: ( K1 is Subfield of K2 & K2 is Subfield of K1 implies K1 = K2 )
assume A1: ( K1 is Subfield of K2 & K2 is Subfield of K1 ) ; ::_thesis: K1 = K2
A2: ( the carrier of K1 c= the carrier of K2 & the carrier of K2 c= the carrier of K1 ) by A1, Def1;
then A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def_10;
A4: the addF of K2 = the addF of K2 || the carrier of K1 by A3, RELSET_1:19
.= the addF of K1 by A1, Def1 ;
A5: the multF of K2 = the multF of K2 || the carrier of K1 by A3, RELSET_1:19
.= the multF of K1 by A1, Def1 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1;
hence K1 = K2 by A4, A5, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: EC_PF_1:5
for K1, K2, K3 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K3 holds
K1 is Subfield of K3
proof
let K1, K2, K3 be strict Field; ::_thesis: ( K1 is Subfield of K2 & K2 is Subfield of K3 implies K1 is Subfield of K3 )
assume A1: ( K1 is Subfield of K2 & K2 is Subfield of K3 ) ; ::_thesis: K1 is Subfield of K3
set C1 = the carrier of K1;
set C2 = the carrier of K2;
set C = the carrier of K3;
set ADD = the addF of K3;
set MULT = the multF of K3;
A2: the carrier of K1 c= the carrier of K2 by A1, Def1;
then A3: [: the carrier of K1, the carrier of K1:] c= [: the carrier of K2, the carrier of K2:] by ZFMISC_1:96;
the carrier of K2 c= the carrier of K3 by A1, Def1;
then A4: the carrier of K1 c= the carrier of K3 by A2, XBOOLE_1:1;
A5: the addF of K2 = the addF of K3 || the carrier of K2 by A1, Def1;
A6: the addF of K1 = the addF of K2 || the carrier of K1 by A1, Def1
.= the addF of K3 || the carrier of K1 by A3, A5, FUNCT_1:51 ;
A7: the multF of K2 = the multF of K3 || the carrier of K2 by A1, Def1;
A8: the multF of K1 = the multF of K2 || the carrier of K1 by A1, Def1
.= the multF of K3 || the carrier of K1 by A3, A7, FUNCT_1:51 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1;
then ( 1. K1 = 1. K3 & 0. K1 = 0. K3 ) by A1, Def1;
hence K1 is Subfield of K3 by A4, A6, A8, Def1; ::_thesis: verum
end;
theorem Th6: :: EC_PF_1:6
for K being Field
for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 )
proof
let K be Field; ::_thesis: for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 )
let SK1, SK2 be Subfield of K; ::_thesis: ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 )
set C1 = the carrier of SK1;
set C2 = the carrier of SK2;
set ADD = the addF of K;
set MULT = the multF of K;
thus ( SK1 is Subfield of SK2 implies the carrier of SK1 c= the carrier of SK2 ) by Def1; ::_thesis: ( the carrier of SK1 c= the carrier of SK2 implies SK1 is Subfield of SK2 )
assume A1: the carrier of SK1 c= the carrier of SK2 ; ::_thesis: SK1 is Subfield of SK2
then A2: [: the carrier of SK1, the carrier of SK1:] c= [: the carrier of SK2, the carrier of SK2:] by ZFMISC_1:96;
the addF of SK2 = the addF of K || the carrier of SK2 by Def1;
then A3: the addF of SK2 || the carrier of SK1 = the addF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the addF of SK1 by Def1 ;
the multF of SK2 = the multF of K || the carrier of SK2 by Def1;
then A4: the multF of SK2 || the carrier of SK1 = the multF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the multF of SK1 by Def1 ;
( 1. SK1 = 1. K & 0. SK1 = 0. K ) by Def1;
then ( 1. SK1 = 1. SK2 & 0. SK1 = 0. SK2 ) by Def1;
hence SK1 is Subfield of SK2 by A1, A3, A4, Def1; ::_thesis: verum
end;
theorem Th7: :: EC_PF_1:7
for K being Field
for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds
x in SK2 )
proof
let K be Field; ::_thesis: for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds
x in SK2 )
let SK1, SK2 be Subfield of K; ::_thesis: ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds
x in SK2 )
thus ( SK1 is Subfield of SK2 implies for x being set st x in SK1 holds
x in SK2 ) by Th3; ::_thesis: ( ( for x being set st x in SK1 holds
x in SK2 ) implies SK1 is Subfield of SK2 )
assume A1: for x being set st x in SK1 holds
x in SK2 ; ::_thesis: SK1 is Subfield of SK2
the carrier of SK1 c= the carrier of SK2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of SK1 or x in the carrier of SK2 )
assume x in the carrier of SK1 ; ::_thesis: x in the carrier of SK2
then reconsider x = x as Element of SK1 ;
x in SK1 by STRUCT_0:def_5;
then x in SK2 by A1;
hence x in the carrier of SK2 by STRUCT_0:def_5; ::_thesis: verum
end;
hence SK1 is Subfield of SK2 by Th6; ::_thesis: verum
end;
theorem Th8: :: EC_PF_1:8
for K being Field
for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 )
proof
let K be Field; ::_thesis: for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 )
let SK1, SK2 be strict Subfield of K; ::_thesis: ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 )
thus ( SK1 = SK2 implies the carrier of SK1 = the carrier of SK2 ) ; ::_thesis: ( the carrier of SK1 = the carrier of SK2 implies SK1 = SK2 )
assume A1: the carrier of SK1 = the carrier of SK2 ; ::_thesis: SK1 = SK2
then A2: SK2 is strict Subfield of SK1 by Th6;
SK1 is strict Subfield of SK2 by A1, Th6;
hence SK1 = SK2 by A2, Th4; ::_thesis: verum
end;
theorem :: EC_PF_1:9
for K being Field
for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )
proof
let K be Field; ::_thesis: for SK1, SK2 being strict Subfield of K holds
( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )
let SK1, SK2 be strict Subfield of K; ::_thesis: ( SK1 = SK2 iff for x being set holds
( x in SK1 iff x in SK2 ) )
thus ( SK1 = SK2 implies for x being set holds
( x in SK1 iff x in SK2 ) ) ; ::_thesis: ( ( for x being set holds
( x in SK1 iff x in SK2 ) ) implies SK1 = SK2 )
assume for x being set holds
( x in SK1 iff x in SK2 ) ; ::_thesis: SK1 = SK2
then ( SK1 is strict Subfield of SK2 & SK2 is strict Subfield of SK1 ) by Th7;
hence SK1 = SK2 by Th4; ::_thesis: verum
end;
registration
let K be finite Field;
cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K;
existence
ex b1 being Subfield of K st b1 is finite
proof
reconsider L = K as Subfield of K by Th1;
take L ; ::_thesis: L is finite
thus L is finite ; ::_thesis: verum
end;
end;
definition
let K be finite Field;
:: original: card
redefine func card K -> Element of NAT ;
coherence
card K is Element of NAT
proof
card the carrier of K in NAT ;
hence card K is Element of NAT ; ::_thesis: verum
end;
end;
registration
cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being Field st
( b1 is strict & b1 is finite )
proof
Z_3 is finite by MOD_2:def_20;
hence ex b1 being Field st
( b1 is strict & b1 is finite ) by MOD_2:27; ::_thesis: verum
end;
end;
theorem :: EC_PF_1:10
for K being finite strict Field
for SK1 being strict Subfield of K st card K = card SK1 holds
SK1 = K
proof
let K be finite strict Field; ::_thesis: for SK1 being strict Subfield of K st card K = card SK1 holds
SK1 = K
let SK1 be strict Subfield of K; ::_thesis: ( card K = card SK1 implies SK1 = K )
assume A1: card K = card SK1 ; ::_thesis: SK1 = K
A2: the carrier of SK1 = the carrier of K
proof
assume A3: the carrier of SK1 <> the carrier of K ; ::_thesis: contradiction
A4: the carrier of SK1 c= the carrier of K by Def1;
then the carrier of SK1 c< the carrier of K by A3, XBOOLE_0:def_8;
hence contradiction by A1, A4, CARD_2:48; ::_thesis: verum
end;
K is Subfield of K by Th1;
hence SK1 = K by A2, Th8; ::_thesis: verum
end;
definition
let IT be Field;
attrIT is prime means :Def2: :: EC_PF_1:def 2
for K1 being Field st K1 is strict Subfield of IT holds
K1 = IT;
end;
:: deftheorem Def2 defines prime EC_PF_1:def_2_:_
for IT being Field holds
( IT is prime iff for K1 being Field st K1 is strict Subfield of IT holds
K1 = IT );
notation
let p be Prime;
synonym GF p for INT.Ring p;
end;
registration
let p be Prime;
cluster GF p -> finite ;
coherence
GF p is finite ;
end;
registration
let p be Prime;
cluster GF p -> prime ;
coherence
GF p is prime
proof
set K = GF p;
A1: p > 1 by INT_2:def_4;
now__::_thesis:_for_K1_being_strict_Subfield_of_GF_p_holds_K1_=_GF_p
let K1 be strict Subfield of GF p; ::_thesis: K1 = GF p
set C = the carrier of (GF p);
set C1 = the carrier of K1;
set n1 = p - 1;
reconsider n1 = p - 1 as Element of NAT by A1, NAT_1:20;
A2: for x being set st x in GF p holds
x in K1
proof
A3: for n being Element of NAT st n in Segm p holds
n in the carrier of K1
proof
defpred S1[ Nat] means p in the carrier of K1;
0 in Segm p by NAT_1:44;
then 0. (GF p) = 0 by FUNCT_7:def_1;
then 0. K1 = 0 by Def1;
then A4: S1[ 0 ] ;
A5: now__::_thesis:_for_n_being_Element_of_NAT_st_0_<=_n_&_n_<_n1_&_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( 0 <= n & n < n1 & S1[n] implies S1[n + 1] )
assume A6: ( 0 <= n & n < n1 ) ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
A8: 1. K1 = 1. (GF p) by Def1
.= 1 by A1, INT_3:14 ;
then A9: [1,n] in [: the carrier of K1, the carrier of K1:] by A7, ZFMISC_1:87;
A10: the addF of K1 = the addF of (GF p) || the carrier of K1 by Def1;
A11: 1 + n < n1 + 1 by A6, XREAL_1:6;
n < n1 + 1 by A6, NAT_1:13;
then A12: ( 1 in Segm p & n in Segm p ) by A1, NAT_1:44;
the addF of K1 . (1,n) = (addint p) . (1,n) by A9, A10, FUNCT_1:49
.= (1 + n) mod p by A12, GR_CY_1:def_4
.= 1 + n by A11, NAT_D:63 ;
hence S1[n + 1] by A7, A8, BINOP_1:17; ::_thesis: verum
end;
A13: for n being Element of NAT st 0 <= n & n <= n1 holds
S1[n] from INT_1:sch_7(A4, A5);
thus for n being Element of NAT st n in Segm p holds
S1[n] ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: ( n in Segm p implies S1[n] )
assume A14: n in Segm p ; ::_thesis: S1[n]
( 0 <= n & n < n1 + 1 ) by A14, ALGSEQ_1:1;
then ( 0 <= n & n <= n1 ) by NAT_1:13;
hence S1[n] by A13; ::_thesis: verum
end;
end;
thus for x being set st x in GF p holds
x in K1 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in GF p implies x in K1 )
assume A15: x in GF p ; ::_thesis: x in K1
x in the carrier of (GF p) by A15, STRUCT_0:def_5;
then x in the carrier of K1 by A3;
hence x in K1 by STRUCT_0:def_5; ::_thesis: verum
end;
end;
GF p is strict Subfield of GF p by Th1;
then GF p is strict Subfield of K1 by A2, Th7;
hence K1 = GF p by Th4; ::_thesis: verum
end;
then for K1 being Field st K1 is strict Subfield of GF p holds
K1 = GF p ;
hence GF p is prime by Def2; ::_thesis: verum
end;
end;
registration
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed prime for doubleLoopStr ;
existence
ex b1 being Field st b1 is prime
proof
take GF the Prime ; ::_thesis: GF the Prime is prime
thus GF the Prime is prime ; ::_thesis: verum
end;
end;
begin
Lm1: for M being non empty multMagma
for a being Element of M
for n being Nat holds (power M) . (a,n) is Element of M
proof
let M be non empty multMagma ; ::_thesis: for a being Element of M
for n being Nat holds (power M) . (a,n) is Element of M
let a be Element of M; ::_thesis: for n being Nat holds (power M) . (a,n) is Element of M
defpred S1[ Nat] means (power M) . (a,$1) is Element of M;
(power M) . (a,0) = 1_ M by GROUP_1:def_7;
then A1: S1[ 0 ] ;
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then reconsider b = (power M) . (a,n) as Element of M ;
n - 0 is Element of NAT by NAT_1:21;
then (power M) . (a,(n + 1)) = b * a by GROUP_1:def_7;
hence S1[n + 1] ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence for n being Nat holds (power M) . (a,n) is Element of M ; ::_thesis: verum
end;
theorem Th11: :: EC_PF_1:11
for p being Prime holds 0 = 0. (GF p)
proof
let p be Prime; ::_thesis: 0 = 0. (GF p)
0 in Segm p by NAT_1:44;
hence 0 = 0. (GF p) by FUNCT_7:def_1; ::_thesis: verum
end;
theorem Th12: :: EC_PF_1:12
for p being Prime holds 1 = 1. (GF p)
proof
let p be Prime; ::_thesis: 1 = 1. (GF p)
1 < p by INT_2:def_4;
then 1 in Segm p by NAT_1:44;
hence 1 = 1. (GF p) by FUNCT_7:def_1; ::_thesis: verum
end;
theorem Th13: :: EC_PF_1:13
for p being Prime
for a being Element of (GF p) ex n1 being Nat st a = n1 mod p
proof
let p be Prime; ::_thesis: for a being Element of (GF p) ex n1 being Nat st a = n1 mod p
let a be Element of (GF p); ::_thesis: ex n1 being Nat st a = n1 mod p
reconsider a = a as Element of Segm p ;
( 0 <= a & a < p ) by ALGSEQ_1:1;
then a = a mod p by NAT_D:63;
hence ex n1 being Nat st a = n1 mod p ; ::_thesis: verum
end;
theorem Th14: :: EC_PF_1:14
for i being Integer
for p being Prime holds i mod p is Element of (GF p)
proof
let i be Integer; ::_thesis: for p being Prime holds i mod p is Element of (GF p)
let p be Prime; ::_thesis: i mod p is Element of (GF p)
reconsider b = i mod p as Integer ;
b in NAT by INT_1:3, INT_1:57;
then reconsider b = b as Nat ;
b < p by INT_1:58;
then b in Segm p by ALGSEQ_1:1;
hence i mod p is Element of (GF p) ; ::_thesis: verum
end;
theorem Th15: :: EC_PF_1:15
for i, j being Integer
for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a + b = (i + j) mod p
proof
let i, j be Integer; ::_thesis: for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a + b = (i + j) mod p
let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a + b = (i + j) mod p
let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a + b = (i + j) mod p )
assume A1: ( a = i mod p & b = j mod p ) ; ::_thesis: a + b = (i + j) mod p
a + b = ((i mod p) + (j mod p)) mod p by A1, GR_CY_1:def_4;
hence a + b = (i + j) mod p by NAT_D:66; ::_thesis: verum
end;
theorem Th16: :: EC_PF_1:16
for i being Integer
for p being Prime
for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p
proof
let i be Integer; ::_thesis: for p being Prime
for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p
let p be Prime; ::_thesis: for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p
let a be Element of (GF p); ::_thesis: ( a = i mod p implies - a = (p - i) mod p )
assume A1: a = i mod p ; ::_thesis: - a = (p - i) mod p
reconsider b = (p - i) mod p as Element of (GF p) by Th14;
a + b = (i + (p - i)) mod p by A1, Th15
.= 0 by INT_1:50
.= 0. (GF p) by Th11 ;
hence - a = (p - i) mod p by VECTSP_1:16; ::_thesis: verum
end;
theorem :: EC_PF_1:17
for i, j being Integer
for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a - b = (i - j) mod p
proof
let i, j be Integer; ::_thesis: for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a - b = (i - j) mod p
let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a - b = (i - j) mod p
let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a - b = (i - j) mod p )
assume A1: ( a = i mod p & b = j mod p ) ; ::_thesis: a - b = (i - j) mod p
then A2: - b = (p - j) mod p by Th16;
a - b = (i + (p - j)) mod p by A1, A2, Th15
.= ((i - j) + (1 * p)) mod p ;
hence a - b = (i - j) mod p by NAT_D:61; ::_thesis: verum
end;
theorem Th18: :: EC_PF_1:18
for i, j being Integer
for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a * b = (i * j) mod p
proof
let i, j be Integer; ::_thesis: for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a * b = (i * j) mod p
let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a * b = (i * j) mod p
let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a * b = (i * j) mod p )
assume ( a = i mod p & b = j mod p ) ; ::_thesis: a * b = (i * j) mod p
then a * b = ((i mod p) * (j mod p)) mod p by INT_3:def_10;
hence a * b = (i * j) mod p by NAT_D:67; ::_thesis: verum
end;
theorem :: EC_PF_1:19
for i, j being Integer
for p being Prime
for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p
proof
let i, j be Integer; ::_thesis: for p being Prime
for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p
let p be Prime; ::_thesis: for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p
let a be Element of (GF p); ::_thesis: ( a = i mod p & (i * j) mod p = 1 implies a " = j mod p )
assume A1: ( a = i mod p & (i * j) mod p = 1 ) ; ::_thesis: a " = j mod p
reconsider b = j mod p as Element of (GF p) by Th14;
A2: p > 1 by INT_2:def_4;
A3: b * a = 1 by A1, Th18
.= 1. (GF p) by A2, INT_3:14 ;
then a <> 0. (GF p) by VECTSP_1:7;
hence a " = j mod p by A3, VECTSP_1:def_10; ::_thesis: verum
end;
theorem Th20: :: EC_PF_1:20
for p being Prime
for a, b being Element of (GF p) holds
( ( a = 0 or b = 0 ) iff a * b = 0 )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) holds
( ( a = 0 or b = 0 ) iff a * b = 0 )
let a, b be Element of (GF p); ::_thesis: ( ( a = 0 or b = 0 ) iff a * b = 0 )
( ( a = 0. (GF p) or b = 0. (GF p) ) iff a * b = 0. (GF p) ) by VECTSP_1:12;
hence ( ( a = 0 or b = 0 ) iff a * b = 0 ) by Th11; ::_thesis: verum
end;
theorem Th21: :: EC_PF_1:21
for p being Prime
for a being Element of (GF p) holds
( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )
proof
let p be Prime; ::_thesis: for a being Element of (GF p) holds
( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )
let a be Element of (GF p); ::_thesis: ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )
thus A1: a |^ 0 = 1_ (GF p) by BINOM:8; ::_thesis: a |^ 0 = 1
p > 1 by INT_2:def_4;
hence a |^ 0 = 1 by A1, INT_3:14; ::_thesis: verum
end;
Lm2: for p being Prime
for a being Element of (GF p) holds (power (GF p)) . (a,1) = a
by GROUP_1:50;
Lm3: for p being Prime
for a being Element of (GF p) holds (power (GF p)) . (a,2) = a * a
by GROUP_1:51;
theorem :: EC_PF_1:22
for p being Prime
for a being Element of (GF p) holds a |^ 2 = a * a by Lm3;
theorem Th23: :: EC_PF_1:23
for n1, n being Nat
for p being Prime
for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p
proof
let n1, n be Nat; ::_thesis: for p being Prime
for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p
let p be Prime; ::_thesis: for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p
let a be Element of (GF p); ::_thesis: ( a = n1 mod p implies a |^ n = (n1 |^ n) mod p )
A1: p > 1 by INT_2:def_4;
assume A2: a = n1 mod p ; ::_thesis: a |^ n = (n1 |^ n) mod p
defpred S1[ Nat] means (power (GF p)) . (a,$1) = (n1 |^ $1) mod p;
a |^ 0 = 1 by Th21;
then A3: a |^ 0 = 1 mod p by A1, NAT_D:63;
A4: S1[ 0 ] by A3, NEWTON:4;
A5: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; ::_thesis: S1[n + 1]
reconsider b = (power (GF p)) . (a,n) as Element of (GF p) by Lm1;
n - 0 is Element of NAT by NAT_1:21;
then (power (GF p)) . (a,(n + 1)) = b * a by GROUP_1:def_7
.= ((n1 |^ n) * n1) mod p by A2, A6, Th18
.= (n1 |^ (n + 1)) mod p by NEWTON:6 ;
hence S1[n + 1] ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5);
hence a |^ n = (n1 |^ n) mod p ; ::_thesis: verum
end;
theorem Th24: :: EC_PF_1:24
for K being non empty unital associative multMagma
for a being Element of K
for n being Nat holds a |^ (n + 1) = (a |^ n) * a
proof
let K be non empty unital associative multMagma ; ::_thesis: for a being Element of K
for n being Nat holds a |^ (n + 1) = (a |^ n) * a
let a be Element of K; ::_thesis: for n being Nat holds a |^ (n + 1) = (a |^ n) * a
let n be Nat; ::_thesis: a |^ (n + 1) = (a |^ n) * a
a |^ (n + 1) = (a |^ n) * (a |^ 1) by BINOM:10
.= (a |^ n) * a by BINOM:8 ;
hence a |^ (n + 1) = (a |^ n) * a ; ::_thesis: verum
end;
theorem Th25: :: EC_PF_1:25
for n being Nat
for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0
proof
let n be Nat; ::_thesis: for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0
let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0
let a be Element of (GF p); ::_thesis: ( a <> 0 implies a |^ n <> 0 )
assume A1: a <> 0 ; ::_thesis: a |^ n <> 0
consider n1 being Nat such that
A2: a = n1 mod p by Th13;
not p divides n1 by A1, A2, INT_1:62;
then not p divides n1 |^ n by NAT_3:5;
then (n1 |^ n) mod p <> 0 by INT_1:62;
hence a |^ n <> 0 by A2, Th23; ::_thesis: verum
end;
theorem Th26: :: EC_PF_1:26
for F being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, y being Element of F holds
( x * x = y * y iff ( x = y or x = - y ) )
proof
let F be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y being Element of F holds
( x * x = y * y iff ( x = y or x = - y ) )
let x, y be Element of F; ::_thesis: ( x * x = y * y iff ( x = y or x = - y ) )
A1: (x - y) * (x + y) = ((x - y) * x) + ((x - y) * y) by VECTSP_1:4
.= ((x * x) - (x * y)) + ((x - y) * y) by VECTSP_1:11
.= ((x * x) - (x * y)) + ((y * x) - (y * y)) by VECTSP_1:11
.= (((x * x) - (x * y)) + (y * x)) + (- (y * y)) by RLVECT_1:def_3
.= ((x * x) + ((- (x * y)) + (y * x))) + (- (y * y)) by RLVECT_1:def_3
.= ((x * x) + ((y * x) - (x * y))) + (- (y * y))
.= ((x * x) + ((x - x) * y)) + (- (y * y)) by VECTSP_1:11
.= ((x * x) + ((0. F) * y)) - (y * y) by RLVECT_1:5
.= ((x * x) + (0. F)) - (y * y) by VECTSP_1:7
.= (x * x) - (y * y) by RLVECT_1:def_4 ;
hereby ::_thesis: ( ( x = y or x = - y ) implies x * x = y * y )
assume A2: x * x = y * y ; ::_thesis: ( x = y or x = - y )
(x - y) * (x + y) = 0. F by A1, A2, RLVECT_1:5;
then ( x - y = 0. F or x + y = 0. F ) by VECTSP_1:12;
hence ( x = y or x = - y ) by RLVECT_1:6, RLVECT_1:21; ::_thesis: verum
end;
assume ( x = y or x = - y ) ; ::_thesis: x * x = y * y
then ( x - y = 0. F or x + y = 0. F ) by RLVECT_1:5;
hence x * x = y * y by A1, RLVECT_1:21, VECTSP_1:6; ::_thesis: verum
end;
theorem Th27: :: EC_PF_1:27
for p being Prime
for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds
x = 0. (GF p)
proof
let p be Prime; ::_thesis: for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds
x = 0. (GF p)
let x be Element of (GF p); ::_thesis: ( 2 < p & x + x = 0. (GF p) implies x = 0. (GF p) )
assume A1: ( 2 < p & x + x = 0. (GF p) ) ; ::_thesis: x = 0. (GF p)
x in Segm p ;
then reconsider Ix = x as Element of NAT ;
A2: 1 = 1. (GF p) by Th12;
A3: 1 + 1 < p by A1;
A4: (1. (GF p)) + (1. (GF p)) = 2 by A2, A3, INT_3:7;
set d = (1. (GF p)) + (1. (GF p));
A5: ((1. (GF p)) + (1. (GF p))) * x = (2 * Ix) mod p by A4, INT_3:def_10;
x + x = ((1. (GF p)) * x) + x by VECTSP_1:def_6
.= ((1. (GF p)) * x) + ((1. (GF p)) * x) by VECTSP_1:def_6
.= (2 * Ix) mod p by A5, VECTSP_1:def_7 ;
then (2 * Ix) mod p = 0 by A1, Th11;
then (2 * Ix) - (((2 * Ix) div p) * p) = 0 by INT_1:def_10;
then A6: p divides 2 * Ix by INT_1:def_3;
p divides Ix by A1, A6, EULER_1:13, INT_2:28, INT_2:30;
then Ix = p * (Ix div p) by NAT_D:3;
then Ix - ((Ix div p) * p) = 0 ;
then A7: Ix mod p = 0 by INT_1:def_10;
Ix < p by NAT_1:44;
then Ix = 0 by A7, NAT_D:63;
hence x = 0. (GF p) by Th11; ::_thesis: verum
end;
theorem Th28: :: EC_PF_1:28
for n being Nat
for p being Prime
for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "
proof
let n be Nat; ::_thesis: for p being Prime
for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "
let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "
let a be Element of (GF p); ::_thesis: ( a <> 0 implies (a ") |^ n = (a |^ n) " )
assume A1: a <> 0 ; ::_thesis: (a ") |^ n = (a |^ n) "
A2: p > 1 by INT_2:def_4;
consider n1 being Nat such that
A3: a = n1 mod p by Th13;
consider n2 being Nat such that
A4: a " = n2 mod p by Th13;
A5: a |^ n = (n1 |^ n) mod p by A3, Th23;
A6: (a ") |^ n = (n2 |^ n) mod p by A4, Th23;
A7: ((n1 * n2) |^ n) mod p = ((n1 |^ n) * (n2 |^ n)) mod p by NEWTON:7
.= (a |^ n) * ((a ") |^ n) by A5, A6, Th18 ;
a <> 0. (GF p) by A1, Th11;
then (a ") * a = 1. (GF p) by VECTSP_1:def_10
.= 1 by Th12 ;
then (n1 * n2) mod p = 1 by A3, A4, Th18;
then ((n1 * n2) |^ n) mod p = 1 by A2, PEPIN:35;
then A8: ((a ") |^ n) * (a |^ n) = 1. (GF p) by A2, A7, INT_3:14;
then a |^ n <> 0. (GF p) by VECTSP_1:7;
hence (a ") |^ n = (a |^ n) " by A8, VECTSP_1:def_10; ::_thesis: verum
end;
Lm4: for n1, n2 being Nat
for p being Prime
for a being Element of (GF p) holds (a |^ n1) * (a |^ n2) = a |^ (n1 + n2)
by BINOM:10;
Lm5: for n1, n2 being Nat
for p being Prime
for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2)
by BINOM:11;
registration
let p be Prime;
cluster MultGroup (GF p) -> cyclic ;
coherence
MultGroup (GF p) is cyclic
proof
MultGroup (GF p) is finite Subgroup of MultGroup (GF p) by GROUP_2:54;
hence MultGroup (GF p) is cyclic by GR_CY_3:38; ::_thesis: verum
end;
end;
theorem Th29: :: EC_PF_1:29
for p being Prime
for x being Element of (MultGroup (GF p))
for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n
proof
let p be Prime; ::_thesis: for x being Element of (MultGroup (GF p))
for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let x be Element of (MultGroup (GF p)); ::_thesis: for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let x1 be Element of (GF p); ::_thesis: for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let n be Nat; ::_thesis: ( x = x1 implies x |^ n = x1 |^ n )
assume A1: x = x1 ; ::_thesis: x |^ n = x1 |^ n
defpred S1[ Nat] means x |^ $1 = x1 |^ $1;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
A3: x |^ (n + 1) = (x |^ n) * x by GROUP_1:34;
A4: x1 |^ (n + 1) = (x1 |^ n) * x1 by Th24;
assume x |^ n = x1 |^ n ; ::_thesis: S1[n + 1]
hence S1[n + 1] by A1, A3, A4, UNIROOTS:16; ::_thesis: verum
end;
x |^ 0 = 1_ (MultGroup (GF p)) by GROUP_1:25
.= 1_ (GF p) by UNIROOTS:17
.= x1 |^ 0 by Th21 ;
then A5: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2);
hence x |^ n = x1 |^ n ; ::_thesis: verum
end;
theorem Th30: :: EC_PF_1:30
for p being Prime ex g being Element of (GF p) st
for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n
proof
let p be Prime; ::_thesis: ex g being Element of (GF p) st
for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n
consider g being Element of (MultGroup (GF p)) such that
A1: for a being Element of (MultGroup (GF p)) ex n being Nat st a = g |^ n by GR_CY_1:18;
reconsider g0 = g as Element of (GF p) by UNIROOTS:19;
take g0 ; ::_thesis: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g0 |^ n
now__::_thesis:_for_a_being_Element_of_(GF_p)_st_a_<>_0._(GF_p)_holds_
ex_n_being_Nat_st_a_=_g0_|^_n
let a be Element of (GF p); ::_thesis: ( a <> 0. (GF p) implies ex n being Nat st a = g0 |^ n )
assume a <> 0. (GF p) ; ::_thesis: ex n being Nat st a = g0 |^ n
then A2: not a in {(0. (GF p))} by TARSKI:def_1;
the carrier of (GF p) = the carrier of (MultGroup (GF p)) \/ {(0. (GF p))} by UNIROOTS:15;
then reconsider a0 = a as Element of (MultGroup (GF p)) by A2, XBOOLE_0:def_3;
consider n being Nat such that
A3: a0 = g |^ n by A1;
take n = n; ::_thesis: a = g0 |^ n
thus a = g0 |^ n by A3, Th29; ::_thesis: verum
end;
hence for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g0 |^ n ; ::_thesis: verum
end;
begin
definition
let p be Prime;
let a be Element of (GF p);
attra is quadratic_residue means :Def3: :: EC_PF_1:def 3
( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a );
attra is not_quadratic_residue means :Def4: :: EC_PF_1:def 4
( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) );
end;
:: deftheorem Def3 defines quadratic_residue EC_PF_1:def_3_:_
for p being Prime
for a being Element of (GF p) holds
( a is quadratic_residue iff ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) );
:: deftheorem Def4 defines not_quadratic_residue EC_PF_1:def_4_:_
for p being Prime
for a being Element of (GF p) holds
( a is not_quadratic_residue iff ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) );
theorem Th31: :: EC_PF_1:31
for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ 2 is quadratic_residue
proof
let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds
a |^ 2 is quadratic_residue
let a be Element of (GF p); ::_thesis: ( a <> 0 implies a |^ 2 is quadratic_residue )
assume A1: a <> 0 ; ::_thesis: a |^ 2 is quadratic_residue
reconsider b = a |^ 2 as Element of (GF p) ;
b <> 0 by A1, Th25;
hence a |^ 2 is quadratic_residue by Def3; ::_thesis: verum
end;
registration
let p be Prime;
cluster 1. (GF p) -> quadratic_residue ;
correctness
coherence
1. (GF p) is quadratic_residue ;
proof
A1: p > 1 by INT_2:def_4;
reconsider a = 1. (GF p) as Element of (GF p) ;
A2: a = 1 by A1, INT_3:14;
a |^ 2 = (1. (GF p)) * (1. (GF p)) by Lm3
.= 1_ (GF p) by GROUP_1:def_4 ;
hence 1. (GF p) is quadratic_residue by A2, Th31; ::_thesis: verum
end;
end;
definition
let p be Prime;
let a be Element of (GF p);
func Lege_p a -> Integer equals :Def5: :: EC_PF_1:def 5
0 if a = 0
1 if a is quadratic_residue
otherwise - 1;
coherence
( ( a = 0 implies 0 is Integer ) & ( a is quadratic_residue implies 1 is Integer ) & ( not a = 0 & not a is quadratic_residue implies - 1 is Integer ) ) ;
consistency
for b1 being Integer st a = 0 & a is quadratic_residue holds
( b1 = 0 iff b1 = 1 ) by Def3;
end;
:: deftheorem Def5 defines Lege_p EC_PF_1:def_5_:_
for p being Prime
for a being Element of (GF p) holds
( ( a = 0 implies Lege_p a = 0 ) & ( a is quadratic_residue implies Lege_p a = 1 ) & ( not a = 0 & not a is quadratic_residue implies Lege_p a = - 1 ) );
theorem Th32: :: EC_PF_1:32
for p being Prime
for a being Element of (GF p) holds
( a is not_quadratic_residue iff Lege_p a = - 1 )
proof
let p be Prime; ::_thesis: for a being Element of (GF p) holds
( a is not_quadratic_residue iff Lege_p a = - 1 )
let a be Element of (GF p); ::_thesis: ( a is not_quadratic_residue iff Lege_p a = - 1 )
hereby ::_thesis: ( Lege_p a = - 1 implies a is not_quadratic_residue )
assume a is not_quadratic_residue ; ::_thesis: Lege_p a = - 1
then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by Def4;
then ( a <> 0 & not a is quadratic_residue ) by Def3;
hence Lege_p a = - 1 by Def5; ::_thesis: verum
end;
assume Lege_p a = - 1 ; ::_thesis: a is not_quadratic_residue
then ( a <> 0 & not a is quadratic_residue ) by Def5;
then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by Def3;
hence a is not_quadratic_residue by Def4; ::_thesis: verum
end;
theorem Th33: :: EC_PF_1:33
for p being Prime
for a being Element of (GF p) holds
( a is quadratic_residue iff Lege_p a = 1 )
proof
let p be Prime; ::_thesis: for a being Element of (GF p) holds
( a is quadratic_residue iff Lege_p a = 1 )
let a be Element of (GF p); ::_thesis: ( a is quadratic_residue iff Lege_p a = 1 )
thus ( a is quadratic_residue implies Lege_p a = 1 ) by Def5; ::_thesis: ( Lege_p a = 1 implies a is quadratic_residue )
assume Lege_p a = 1 ; ::_thesis: a is quadratic_residue
then ( a <> 0 & Lege_p a <> - 1 ) by Def5;
hence a is quadratic_residue by Def5; ::_thesis: verum
end;
theorem Th34: :: EC_PF_1:34
for p being Prime
for a being Element of (GF p) holds
( a = 0 iff Lege_p a = 0 )
proof
let p be Prime; ::_thesis: for a being Element of (GF p) holds
( a = 0 iff Lege_p a = 0 )
let a be Element of (GF p); ::_thesis: ( a = 0 iff Lege_p a = 0 )
thus ( a = 0 implies Lege_p a = 0 ) by Def5; ::_thesis: ( Lege_p a = 0 implies a = 0 )
assume Lege_p a = 0 ; ::_thesis: a = 0
then ( not a is quadratic_residue & Lege_p a <> - 1 ) by Def5;
hence a = 0 by Def5; ::_thesis: verum
end;
theorem :: EC_PF_1:35
for p being Prime
for a being Element of (GF p) st a <> 0 holds
Lege_p (a |^ 2) = 1
proof
let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds
Lege_p (a |^ 2) = 1
let a be Element of (GF p); ::_thesis: ( a <> 0 implies Lege_p (a |^ 2) = 1 )
assume a <> 0 ; ::_thesis: Lege_p (a |^ 2) = 1
then a |^ 2 is quadratic_residue by Th31;
hence Lege_p (a |^ 2) = 1 by Th33; ::_thesis: verum
end;
theorem Th36: :: EC_PF_1:36
for p being Prime
for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b)
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b)
let a, b be Element of (GF p); ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
percases ( a is quadratic_residue or not a is quadratic_residue ) ;
supposeA1: a is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A2: Lege_p a = 1 by Th33;
percases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ;
supposeA3: b is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A4: Lege_p b = 1 by Th33;
A5: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1, Def3;
( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A3, Def3;
then A6: a * b <> 0 by A5, Th20;
ex x being Element of (GF p) st x |^ 2 = a * b
proof
consider a1 being Element of (GF p) such that
A7: a1 |^ 2 = a by A1, Def3;
consider b1 being Element of (GF p) such that
A8: b1 |^ 2 = b by A3, Def3;
(a1 |^ 2) * (b1 |^ 2) = (a1 * b1) |^ 2 by BINOM:9;
hence ex x being Element of (GF p) st x |^ 2 = a * b by A7, A8; ::_thesis: verum
end;
then a * b is quadratic_residue by A6, Def3;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A4, Th33; ::_thesis: verum
end;
supposeA9: b = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then Lege_p b = 0 by Def5;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A9, Th20; ::_thesis: verum
end;
supposeA10: ( b <> 0 & not b is quadratic_residue ) ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A11: Lege_p b = - 1 by Def5;
A12: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1, Def3;
A13: a * b <> 0 by A10, A12, Th20;
for x being Element of (GF p) holds not x |^ 2 = a * b
proof
given xab being Element of (GF p) such that A14: xab |^ 2 = a * b ; ::_thesis: contradiction
consider xa being Element of (GF p) such that
A15: xa |^ 2 = a by A1, Def3;
A16: xa |^ 2 <> 0. (GF p) by A12, A15, Th11;
A17: xa <> 0
proof
assume xa = 0 ; ::_thesis: contradiction
then xa = 0. (GF p) by Th11;
then xa * xa = 0. (GF p) by VECTSP_1:12;
then xa |^ 2 = 0. (GF p) by Lm3;
hence contradiction by A15, A12, Th11; ::_thesis: verum
end;
((xa ") * xab) |^ 2 = ((xa ") |^ 2) * (a * b) by A14, BINOM:9
.= (((xa ") |^ 2) * (xa |^ 2)) * b by A15, GROUP_1:def_3
.= (((xa |^ 2) ") * (xa |^ 2)) * b by Th28, A17
.= (1. (GF p)) * b by A16, VECTSP_1:def_10
.= b by VECTSP_1:def_8 ;
hence contradiction by A10, Def3; ::_thesis: verum
end;
then a * b is not_quadratic_residue by A13, Def4;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A11, Th32; ::_thesis: verum
end;
end;
end;
supposeA18: not a is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
now__::_thesis:_Lege_p_(a_*_b)_=_(Lege_p_a)_*_(Lege_p_b)
percases ( a = 0 or a <> 0 ) ;
supposeA19: a = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then Lege_p a = 0 by Th34;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A19, Th20; ::_thesis: verum
end;
supposeA20: a <> 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A21: Lege_p a = - 1 by A18, Def5;
percases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ;
supposeA22: b is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A23: Lege_p b = 1 by Th33;
A24: ( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A22, Def3;
then A25: a * b <> 0 by A20, Th20;
for x being Element of (GF p) holds not x |^ 2 = a * b
proof
given xab being Element of (GF p) such that A26: xab |^ 2 = a * b ; ::_thesis: contradiction
consider xb being Element of (GF p) such that
A27: xb |^ 2 = b by A22, Def3;
A28: xb |^ 2 <> 0. (GF p) by A24, A27, Th11;
A29: xb <> 0
proof
assume xb = 0 ; ::_thesis: contradiction
then xb = 0. (GF p) by Th11;
then xb * xb = 0. (GF p) by VECTSP_1:12;
then xb |^ 2 = 0. (GF p) by Lm3;
hence contradiction by A27, A24, Th11; ::_thesis: verum
end;
(xab * (xb ")) |^ 2 = (a * b) * ((xb ") |^ 2) by A26, BINOM:9
.= a * ((xb |^ 2) * ((xb ") |^ 2)) by A27, GROUP_1:def_3
.= a * ((xb |^ 2) * ((xb |^ 2) ")) by Th28, A29
.= a * (1. (GF p)) by A28, VECTSP_1:def_10
.= a by VECTSP_1:def_8 ;
hence contradiction by A18, A20, Def3; ::_thesis: verum
end;
then a * b is not_quadratic_residue by A25, Def4;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A23, Th32; ::_thesis: verum
end;
supposeA30: b = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then Lege_p b = 0 by Th34;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A30, Th20; ::_thesis: verum
end;
supposeA31: ( b <> 0 & not b is quadratic_residue ) ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)
then A32: Lege_p b = - 1 by Def5;
A33: a * b <> 0 by A20, A31, Th20;
ex x being Element of (GF p) st x |^ 2 = a * b
proof
consider g being Element of (GF p) such that
A34: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n by Th30;
a <> 0. (GF p) by A20, Th11;
then consider na being Nat such that
A35: a = g |^ na by A34;
b <> 0. (GF p) by A31, Th11;
then consider nb being Nat such that
A36: b = g |^ nb by A34;
A37: na = ((na div 2) * 2) + (na mod 2) by NAT_D:2;
A38: nb = ((nb div 2) * 2) + (nb mod 2) by NAT_D:2;
na mod 2 <> 0
proof
assume A39: na mod 2 = 0 ; ::_thesis: contradiction
reconsider nn = na div 2 as Element of NAT ;
a = (g |^ nn) |^ 2 by A35, A37, A39, Lm5;
hence contradiction by A18, A20, Def3; ::_thesis: verum
end;
then A40: na mod 2 = 1 by NAT_D:12;
nb mod 2 <> 0
proof
assume A41: nb mod 2 = 0 ; ::_thesis: contradiction
reconsider nn = nb div 2 as Element of NAT ;
b = (g |^ nn) |^ 2 by A36, A38, A41, Lm5;
hence contradiction by A31, Def3; ::_thesis: verum
end;
then A42: nb mod 2 = 1 by NAT_D:12;
reconsider nc = ((na div 2) + (nb div 2)) + 1 as Nat ;
A43: na + nb = (((na div 2) * 2) + 1) + nb by A40, NAT_D:2
.= (((na div 2) * 2) + 1) + (((nb div 2) * 2) + 1) by A42, NAT_D:2
.= nc * 2 ;
a * b = g |^ (na + nb) by A35, A36, Lm4
.= (g |^ nc) |^ 2 by A43, Lm5 ;
hence ex x being Element of (GF p) st x |^ 2 = a * b ; ::_thesis: verum
end;
then a * b is quadratic_residue by A33, Def3;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A32, Th33; ::_thesis: verum
end;
end;
end;
end;
end;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) ; ::_thesis: verum
end;
end;
end;
theorem Th37: :: EC_PF_1:37
for n being Nat
for p being Prime
for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds
Lege_p (a |^ n) = 1
proof
let n be Nat; ::_thesis: for p being Prime
for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds
Lege_p (a |^ n) = 1
let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds
Lege_p (a |^ n) = 1
let a be Element of (GF p); ::_thesis: ( a <> 0 & n mod 2 = 0 implies Lege_p (a |^ n) = 1 )
assume A1: ( a <> 0 & n mod 2 = 0 ) ; ::_thesis: Lege_p (a |^ n) = 1
A2: n = ((n div 2) * 2) + (n mod 2) by INT_1:59
.= (n div 2) * 2 by A1 ;
reconsider n1 = n div 2 as Nat ;
(a |^ n1) |^ 2 is quadratic_residue by A1, Th31, Th25;
then a |^ n is quadratic_residue by A2, Lm5;
hence Lege_p (a |^ n) = 1 by Def5; ::_thesis: verum
end;
theorem :: EC_PF_1:38
for n being Nat
for p being Prime
for a being Element of (GF p) st n mod 2 = 1 holds
Lege_p (a |^ n) = Lege_p a
proof
let n be Nat; ::_thesis: for p being Prime
for a being Element of (GF p) st n mod 2 = 1 holds
Lege_p (a |^ n) = Lege_p a
let p be Prime; ::_thesis: for a being Element of (GF p) st n mod 2 = 1 holds
Lege_p (a |^ n) = Lege_p a
let a be Element of (GF p); ::_thesis: ( n mod 2 = 1 implies Lege_p (a |^ n) = Lege_p a )
assume A1: n mod 2 = 1 ; ::_thesis: Lege_p (a |^ n) = Lege_p a
A2: n = ((n div 2) * 2) + 1 by A1, INT_1:59;
reconsider n1 = n - 1 as Nat by A2;
a |^ (n1 + 1) = (a |^ n1) * a by Th24;
then A3: Lege_p (a |^ n) = (Lege_p (a |^ n1)) * (Lege_p a) by Th36;
percases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; ::_thesis: Lege_p (a |^ n) = Lege_p a
then Lege_p a = 0 by Def5;
hence Lege_p (a |^ n) = Lege_p a by A3; ::_thesis: verum
end;
supposeA4: a <> 0 ; ::_thesis: Lege_p (a |^ n) = Lege_p a
(n - 1) mod 2 = (0 + ((n div 2) * 2)) mod 2 by A2
.= 0 mod 2 by NAT_D:61
.= 0 by NAT_D:26 ;
then Lege_p (a |^ n1) = 1 by A4, Th37;
hence Lege_p (a |^ n) = Lege_p a by A3; ::_thesis: verum
end;
end;
end;
theorem Th39: :: EC_PF_1:39
for p being Prime
for a being Element of (GF p) st 2 < p holds
card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
proof
let p be Prime; ::_thesis: for a being Element of (GF p) st 2 < p holds
card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
let a be Element of (GF p); ::_thesis: ( 2 < p implies card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) )
assume A1: 2 < p ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
percases ( a is quadratic_residue or not a is quadratic_residue ) ;
supposeA2: a is quadratic_residue ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
then consider x being Element of (GF p) such that
A3: x |^ 2 = a by Def3;
A4: x in { b where b is Element of (GF p) : b |^ 2 = a } by A3;
(- x) |^ 2 = (- x) * (- x) by Lm3
.= x * x by VECTSP_1:10
.= a by A3, Lm3 ;
then - x in { b where b is Element of (GF p) : b |^ 2 = a } ;
then A5: {x,(- x)} c= { b where b is Element of (GF p) : b |^ 2 = a } by A4, ZFMISC_1:32;
A6: x <> - x
proof
assume x = - x ; ::_thesis: contradiction
then x + x = 0. (GF p) by VECTSP_1:16;
then A7: x = 0. (GF p) by A1, Th27;
x |^ 2 = (0. (GF p)) * (0. (GF p)) by A7, Lm3
.= 0. (GF p) by VECTSP_1:12
.= 0 by Th11 ;
hence contradiction by A3, A2, Def3; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__holds_
y_in_{x,(-_x)}
let y be set ; ::_thesis: ( y in { b where b is Element of (GF p) : b |^ 2 = a } implies y in {x,(- x)} )
assume y in { b where b is Element of (GF p) : b |^ 2 = a } ; ::_thesis: y in {x,(- x)}
then consider z being Element of (GF p) such that
A8: ( y = z & z |^ 2 = a ) ;
z * z = z |^ 2 by Lm3
.= x * x by A3, A8, Lm3 ;
then ( z = x or z = - x ) by Th26;
hence y in {x,(- x)} by A8, TARSKI:def_2; ::_thesis: verum
end;
then { b where b is Element of (GF p) : b |^ 2 = a } c= {x,(- x)} by TARSKI:def_3;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = card {x,(- x)} by A5, XBOOLE_0:def_10
.= 1 + 1 by A6, CARD_2:57
.= 1 + (Lege_p a) by A2, Def5 ;
::_thesis: verum
end;
supposeA9: not a is quadratic_residue ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
now__::_thesis:_card__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__=_1_+_(Lege_p_a)
percases ( a = 0 or a <> 0 ) ;
supposeA10: a = 0 ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ::_thesis: verum
proof
now__::_thesis:_for_x_being_set_st_x_in__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__holds_
x_in_{(0._(GF_p))}
let x be set ; ::_thesis: ( x in { b where b is Element of (GF p) : b |^ 2 = a } implies x in {(0. (GF p))} )
assume x in { b where b is Element of (GF p) : b |^ 2 = a } ; ::_thesis: x in {(0. (GF p))}
then consider b being Element of (GF p) such that
A11: ( x = b & b |^ 2 = 0 ) by A10;
b = 0 by Th25, A11
.= 0. (GF p) by Th11 ;
hence x in {(0. (GF p))} by A11, TARSKI:def_1; ::_thesis: verum
end;
then A12: { b where b is Element of (GF p) : b |^ 2 = a } c= {(0. (GF p))} by TARSKI:def_3;
(0. (GF p)) |^ 2 = (0. (GF p)) * (0. (GF p)) by Lm3
.= 0. (GF p) by VECTSP_1:12
.= 0 by Th11 ;
then 0. (GF p) in { b where b is Element of (GF p) : b |^ 2 = a } by A10;
then {(0. (GF p))} c= { b where b is Element of (GF p) : b |^ 2 = a } by ZFMISC_1:31;
then { b where b is Element of (GF p) : b |^ 2 = a } = {(0. (GF p))} by A12, XBOOLE_0:def_10;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + 0 by CARD_2:42
.= 1 + (Lege_p a) by A10, Def5 ;
::_thesis: verum
end;
end;
supposeA13: a <> 0 ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
A14: { b where b is Element of (GF p) : b |^ 2 = a } = {}
proof
assume { b where b is Element of (GF p) : b |^ 2 = a } <> {} ; ::_thesis: contradiction
then consider x being set such that
A15: x in { b where b is Element of (GF p) : b |^ 2 = a } by XBOOLE_0:def_1;
ex b being Element of (GF p) st
( x = b & b |^ 2 = a ) by A15;
hence contradiction by A9, Def3, A13; ::_thesis: verum
end;
thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (- 1) by A14
.= 1 + (Lege_p a) by A9, A13, Def5 ; ::_thesis: verum
end;
end;
end;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ; ::_thesis: verum
end;
end;
end;
begin
definition
let K be Field;
func ProjCo K -> non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] equals :: EC_PF_1:def 6
[: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]};
correctness
coherence
[: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:];
proof
[(1. K),(1. K),(1. K)] <> [(0. K),(0. K),(0. K)] by XTUPLE_0:3;
then not [(1. K),(1. K),(1. K)] in {[(0. K),(0. K),(0. K)]} by TARSKI:def_1;
hence [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
:: deftheorem defines ProjCo EC_PF_1:def_6_:_
for K being Field holds ProjCo K = [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]};
theorem Th40: :: EC_PF_1:40
for p being Prime holds ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
proof
let p be Prime; ::_thesis: ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
0. (GF p) = 0 by Th11;
hence ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} ; ::_thesis: verum
end;
definition
let p be Prime;
let a, b be Element of (GF p);
func Disc (a,b,p) -> Element of (GF p) means :: EC_PF_1:def 7
for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
it = (g4 * (a |^ 3)) + (g27 * (b |^ 2));
existence
ex b1 being Element of (GF p) st
for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2))
proof
reconsider g40 = 4 mod p as Element of (GF p) by Th14;
reconsider g270 = 27 mod p as Element of (GF p) by Th14;
reconsider d = (g40 * (a |^ 3)) + (g270 * (b |^ 2)) as Element of (GF p) ;
take d ; ::_thesis: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d = (g4 * (a |^ 3)) + (g27 * (b |^ 2))
thus for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of (GF p) st ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) holds
b1 = b2
proof
let d1, d2 be Element of (GF p); ::_thesis: ( ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) implies d1 = d2 )
assume A1: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: ( ex g4, g27 being Element of (GF p) st
( g4 = 4 mod p & g27 = 27 mod p & not d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) or d1 = d2 )
assume A2: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: d1 = d2
reconsider g4 = 4 mod p as Element of (GF p) by Th14;
reconsider g27 = 27 mod p as Element of (GF p) by Th14;
thus d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) by A1
.= d2 by A2 ; ::_thesis: verum
end;
end;
:: deftheorem defines Disc EC_PF_1:def_7_:_
for p being Prime
for a, b, b4 being Element of (GF p) holds
( b4 = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b4 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) );
definition
let p be Prime;
let a, b be Element of (GF p);
func EC_WEqProjCo (a,b,p) -> Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) means :Def8: :: EC_PF_1:def 8
for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds it . 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)));
existence
ex b1 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st
for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . 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)))
proof
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
deffunc H1( Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]) -> Element of the carrier of (GF p) = ((($1 `2_3) |^ 2) * ($1 `3_3)) - (((($1 `1_3) |^ 3) + ((a * ($1 `1_3)) * (($1 `3_3) |^ 2))) + (b * (($1 `3_3) |^ 3)));
consider f being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p) such that
A1: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . 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)))
thus for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . 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 A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . 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))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b2 . 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))) ) holds
b1 = b2
proof
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
deffunc H1( Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]) -> Element of the carrier of (GF p) = ((($1 `2_3) |^ 2) * ($1 `3_3)) - (((($1 `1_3) |^ 3) + ((a * ($1 `1_3)) * (($1 `3_3) |^ 2))) + (b * (($1 `3_3) |^ 3)));
let f, g be Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p); ::_thesis: ( ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . 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))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . 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))) ) implies f = g )
assume A2: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = H1(x) ; ::_thesis: ( ex P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st not g . 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))) or f = g )
assume A3: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . x = H1(x) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_[:_the_carrier_of_(GF_p),_the_carrier_of_(GF_p),_the_carrier_of_(GF_p):]_holds_f_._x_=_g_._x
let x be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; ::_thesis: f . x = g . x
thus f . x = H1(x) by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:def_8; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines EC_WEqProjCo EC_PF_1:def_8_:_
for p being Prime
for a, b being Element of (GF p)
for b4 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds
( b4 = EC_WEqProjCo (a,b,p) iff for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b4 . 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))) );
theorem Th41: :: EC_PF_1:41
for p being Prime
for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
proof
let p be Prime; ::_thesis: for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
let a, b be Element of (GF p); ::_thesis: for X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
let X, Y, Z be Element of (GF p); ::_thesis: (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
reconsider P = [X,Y,Z] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
( P `1_3 = X & P `2_3 = Y & P `3_3 = Z ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7;
hence (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) by Def8; ::_thesis: verum
end;
Lm6: for p being 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) )
proof
let p be Prime; ::_thesis: 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); ::_thesis: ( [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 ::_thesis: (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; ::_thesis: 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 ;
A3: P = [(0. (GF p)),1,0] by Th11
.= [(0. (GF p)),(1. (GF p)),0] by Th12
.= [(0. (GF p)),(1. (GF p)),(0. (GF p))] by Th11 ;
then A4: P `1_3 = 0. (GF p) by MCART_1:def_5;
A5: P `3_3 = 0. (GF p) by A3, MCART_1:def_7;
A6: (P `1_3) |^ 3 = (P `1_3) |^ (2 + 1)
.= ((P `1_3) |^ 2) * (P `1_3) by Th24
.= 0. (GF p) by A4, VECTSP_1:12 ;
A7: (P `3_3) |^ 3 = (P `3_3) |^ (2 + 1)
.= ((P `3_3) |^ 2) * (P `3_3) by Th24
.= 0. (GF p) by A5, VECTSP_1:12 ;
A8: (P `3_3) |^ 2 = (P `3_3) |^ (1 + 1)
.= ((P `3_3) |^ 1) * (P `3_3) by Th24
.= 0. (GF p) by A5, VECTSP_1:12 ;
(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))) by A5, VECTSP_1:12
.= - (((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))) by A8, VECTSP_1:12
.= - (b * ((P `3_3) |^ 3)) by RLVECT_1:4
.= - (0. (GF p)) by A7, VECTSP_1:12
.= (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; ::_thesis: verum
end;
definition
let p be Prime;
let a, b be Element of (GF p);
func EC_SetProjCo (a,b,p) -> non empty Subset of (ProjCo (GF p)) equals :: EC_PF_1:def 9
{ P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
correctness
coherence
{ P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p));
proof
A1: now__::_thesis:_for_x_being_set_st_x_in__{__P_where_P_is_Element_of_ProjCo_(GF_p)_:_(EC_WEqProjCo_(a,b,p))_._P_=_0._(GF_p)__}__holds_
x_in_ProjCo_(GF_p)
let x be set ; ::_thesis: ( x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } implies x in ProjCo (GF p) )
assume x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; ::_thesis: x in ProjCo (GF p)
then ex P being Element of ProjCo (GF p) st
( x = P & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ;
hence x in ProjCo (GF p) ; ::_thesis: verum
end;
reconsider D0 = [0,1,0] as Element of ProjCo (GF p) by Lm6;
(EC_WEqProjCo (a,b,p)) . D0 = 0. (GF p) by Lm6;
then D0 in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p)) by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines EC_SetProjCo EC_PF_1:def_9_:_
for p being Prime
for a, b being Element of (GF p) holds EC_SetProjCo (a,b,p) = { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
Lm7: for p being Prime
for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p)
proof
let p be Prime; ::_thesis: for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p)
let d, Y be Element of (GF p); ::_thesis: [d,Y,1] is Element of ProjCo (GF p)
set P = [d,Y,1];
[d,Y,1] <> [0,0,0] by XTUPLE_0:3;
then A1: not [d,Y,1] in {[0,0,0]} by TARSKI:def_1;
1. (GF p) in the carrier of (GF p) ;
then 1 in the carrier of (GF p) by Th12;
then [d,Y,1] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] by MCART_1:69;
then [d,Y,1] 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 [d,Y,1] is Element of ProjCo (GF p) by Th40; ::_thesis: verum
end;
theorem Th42: :: EC_PF_1:42
for p being Prime
for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)
let a, b be Element of (GF p); ::_thesis: [0,1,0] is Element of EC_SetProjCo (a,b,p)
( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) by Lm6;
then [0,1,0] in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence [0,1,0] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: verum
end;
theorem Th43: :: EC_PF_1:43
for p being Prime
for a, b, X, Y being Element of (GF p) holds
( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )
proof
let p be Prime; ::_thesis: for a, b, X, Y being Element of (GF p) holds
( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )
let a, b, X, Y be Element of (GF p); ::_thesis: ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )
A1: 1 = 1. (GF p) by Th12;
reconsider Q = [X,Y,1] as Element of ProjCo (GF p) by Lm7;
A2: Y |^ 2 = (Y |^ 2) * (1. (GF p)) by VECTSP_1:def_6;
A3: a * X = (a * X) * (1. (GF p)) by VECTSP_1:def_6
.= (a * X) * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def_6
.= (a * X) * ((1. (GF p)) |^ 2) by Lm3 ;
A4: b = b * (1. (GF p)) by VECTSP_1:def_6
.= b * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def_6
.= b * ((1. (GF p)) |^ 2) by Lm3
.= b * (((1. (GF p)) |^ 2) * (1. (GF p))) by VECTSP_1:def_6
.= b * ((1. (GF p)) |^ (2 + 1)) by Th24
.= b * ((1. (GF p)) |^ 3) ;
hereby ::_thesis: ( [X,Y,1] is Element of EC_SetProjCo (a,b,p) implies Y |^ 2 = ((X |^ 3) + (a * X)) + b )
assume A5: Y |^ 2 = ((X |^ 3) + (a * X)) + b ; ::_thesis: [X,Y,1] is Element of EC_SetProjCo (a,b,p)
(Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A5, VECTSP_1:19;
then (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) by A1, A2, A3, A4, Th41;
then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: verum
end;
assume [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: Y |^ 2 = ((X |^ 3) + (a * X)) + b
then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
then ex P being Element of ProjCo (GF p) st
( P = Q & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ;
then (Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A1, A2, A3, A4, Th41;
hence Y |^ 2 = ((X |^ 3) + (a * X)) + b by VECTSP_1:19; ::_thesis: verum
end;
definition
let p be Prime;
let P, Q be Element of ProjCo (GF p);
predP _EQ_ Q means :Def10: :: EC_PF_1:def 10
ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) );
reflexivity
for P being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) )
proof
for R being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) )
proof
let R be Element of ProjCo (GF p); ::_thesis: ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) )
reconsider a = 1. (GF p) as Element of (GF p) ;
( R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) by VECTSP_1:def_6;
hence ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) ; ::_thesis: verum
end;
hence for P being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) ) ; ::_thesis: verum
end;
symmetry
for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds
ex a being Element of (GF p) st
( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) )
proof
thus for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds
ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) ::_thesis: verum
proof
let P, Q be Element of ProjCo (GF p); ::_thesis: ( ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) implies ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) )
given a being Element of (GF p) such that A1: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ; ::_thesis: ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) )
take b = a " ; ::_thesis: ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) )
A2: b <> 0. (GF p)
proof
assume b = 0. (GF p) ; ::_thesis: contradiction
then b * a = 0. (GF p) by VECTSP_1:7;
then 1. (GF p) = 0. (GF p) by A1, VECTSP_1:def_10;
hence contradiction ; ::_thesis: verum
end;
A3: Q `1_3 = (1. (GF p)) * (Q `1_3) by VECTSP_1:def_6
.= (b * a) * (Q `1_3) by A1, VECTSP_1:def_10
.= b * (P `1_3) by A1, GROUP_1:def_3 ;
A4: Q `2_3 = (1. (GF p)) * (Q `2_3) by VECTSP_1:def_6
.= (b * a) * (Q `2_3) by A1, VECTSP_1:def_10
.= b * (P `2_3) by A1, GROUP_1:def_3 ;
Q `3_3 = (1. (GF p)) * (Q `3_3) by VECTSP_1:def_6
.= (b * a) * (Q `3_3) by A1, VECTSP_1:def_10
.= b * (P `3_3) by A1, GROUP_1:def_3 ;
hence ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) by A2, A3, A4; ::_thesis: verum
end;
end;
end;
:: deftheorem Def10 defines _EQ_ EC_PF_1:def_10_:_
for p being Prime
for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) );
theorem Th44: :: EC_PF_1:44
for p being Prime
for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds
P _EQ_ R
proof
let p be Prime; ::_thesis: for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds
P _EQ_ R
let P, Q, R be Element of ProjCo (GF p); ::_thesis: ( P _EQ_ Q & Q _EQ_ R implies P _EQ_ R )
assume A1: ( P _EQ_ Q & Q _EQ_ R ) ; ::_thesis: P _EQ_ R
then consider a being Element of (GF p) such that
A2: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) by Def10;
consider b being Element of (GF p) such that
A3: ( b <> 0. (GF p) & Q `1_3 = b * (R `1_3) & Q `2_3 = b * (R `2_3) & Q `3_3 = b * (R `3_3) ) by Def10, A1;
take d = a * b; :: according to EC_PF_1:def_10 ::_thesis: ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) )
thus ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) ) by A2, A3, GROUP_1:def_3, VECTSP_1:12; ::_thesis: verum
end;
theorem Th45: :: EC_PF_1:45
for p being Prime
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_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds
Q in EC_SetProjCo (a,b,p)
proof
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_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_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_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_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_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_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_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) implies Q in EC_SetProjCo (a,b,p) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_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
A2: ( P = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) by A1;
A3: (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;
A4: (EC_WEqProjCo (a,b,p)) . Q = (((d * (P `2_3)) |^ 2) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by A1, Def8
.= (((d |^ 2) * ((P `2_3) |^ 2)) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9
.= ((((d |^ 2) * ((P `2_3) |^ 2)) * d) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= ((((d |^ 2) * d) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= (((d |^ (2 + 1)) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by Th24
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d |^ 2) * ((P `3_3) |^ 2)))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((a * (d * (P `1_3))) * (d |^ 2)) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d * (P `1_3)) * (d |^ 2))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (((d |^ 2) * d) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d |^ (2 + 1)) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by Th24
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d |^ 3) * ((P `3_3) |^ 3)))) by BINOM:9
.= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3
.= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3
.= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3
.= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3)))) by GROUP_1:def_3
.= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - (((d |^ 3) * (((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3)))) by VECTSP_1:4
.= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((d |^ 3) * ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))) by VECTSP_1:4
.= (d |^ 3) * ((((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 VECTSP_1:11
.= 0. (GF p) by A2, A3, 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 Th40;
then A5: not P in {[0,0,0]} by A2, XBOOLE_0:def_5;
A6: Q = [(Q `1_3),(Q `2_3),(Q `3_3)] by MCART_1:44;
( P `1_3 <> 0 or P `2_3 <> 0 or P `3_3 <> 0 )
proof
assume ( not P `1_3 <> 0 & not P `2_3 <> 0 & not P `3_3 <> 0 ) ; ::_thesis: contradiction
then P = [0,0,0] by MCART_1:44;
hence contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
then ( P `1_3 <> 0. (GF p) or P `2_3 <> 0. (GF p) or P `3_3 <> 0. (GF p) ) by Th11;
then ( d * (P `1_3) <> 0. (GF p) or d * (P `2_3) <> 0. (GF p) or d * (P `3_3) <> 0. (GF p) ) by A1, VECTSP_1:12;
then ( Q `1_3 <> 0 or Q `2_3 <> 0 or Q `3_3 <> 0 ) by A1, Th11;
then [(Q `1_3),(Q `2_3),(Q `3_3)] <> [0,0,0] by XTUPLE_0:3;
then not Q in {[0,0,0]} by A6, 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 Th40;
hence Q in EC_SetProjCo (a,b,p) by A4; ::_thesis: verum
end;
definition
let p be Prime;
func R_ProjCo p -> Relation of (ProjCo (GF p)) equals :: EC_PF_1:def 11
{ [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;
correctness
coherence
{ [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p));
proof
set RX = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;
now__::_thesis:_for_x_being_set_st_x_in__{__[P,Q]_where_P,_Q_is_Element_of_ProjCo_(GF_p)_:_P__EQ__Q__}__holds_
x_in_[:(ProjCo_(GF_p)),(ProjCo_(GF_p)):]
let x be set ; ::_thesis: ( x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } implies x in [:(ProjCo (GF p)),(ProjCo (GF p)):] )
assume x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; ::_thesis: x in [:(ProjCo (GF p)),(ProjCo (GF p)):]
then consider P, Q being Element of ProjCo (GF p) such that
A1: ( x = [P,Q] & P _EQ_ Q ) ;
thus x in [:(ProjCo (GF p)),(ProjCo (GF p)):] by A1; ::_thesis: verum
end;
hence { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p)) by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines R_ProjCo EC_PF_1:def_11_:_
for p being Prime holds R_ProjCo p = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;
theorem Th46: :: EC_PF_1:46
for p being Prime
for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff [P,Q] in R_ProjCo p )
proof
let p be Prime; ::_thesis: for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff [P,Q] in R_ProjCo p )
let P, Q be Element of ProjCo (GF p); ::_thesis: ( P _EQ_ Q iff [P,Q] in R_ProjCo p )
thus ( P _EQ_ Q implies [P,Q] in R_ProjCo p ) ; ::_thesis: ( [P,Q] in R_ProjCo p implies P _EQ_ Q )
assume [P,Q] in R_ProjCo p ; ::_thesis: P _EQ_ Q
then consider X0, Y0 being Element of ProjCo (GF p) such that
A1: ( [P,Q] = [X0,Y0] & X0 _EQ_ Y0 ) ;
( P = X0 & Q = Y0 ) by A1, XTUPLE_0:1;
hence P _EQ_ Q by A1; ::_thesis: verum
end;
registration
let p be Prime;
cluster R_ProjCo p -> total symmetric transitive ;
coherence
( R_ProjCo p is total & R_ProjCo p is symmetric & R_ProjCo p is transitive )
proof
set R = R_ProjCo p;
for x being set holds
( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p )
proof
let x be set ; ::_thesis: ( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p )
hereby ::_thesis: ( ex y being set st [x,y] in R_ProjCo p implies x in ProjCo (GF p) )
assume x in ProjCo (GF p) ; ::_thesis: ex y being set st [x,y] in R_ProjCo p
then reconsider X = x as Element of ProjCo (GF p) ;
X _EQ_ X ;
then [x,x] in R_ProjCo p ;
hence ex y being set st [x,y] in R_ProjCo p ; ::_thesis: verum
end;
given y being set such that A1: [x,y] in R_ProjCo p ; ::_thesis: x in ProjCo (GF p)
consider X, Y being Element of ProjCo (GF p) such that
A2: ( [x,y] = [X,Y] & X _EQ_ Y ) by A1;
x = X by A2, XTUPLE_0:1;
hence x in ProjCo (GF p) ; ::_thesis: verum
end;
then dom (R_ProjCo p) = ProjCo (GF p) by XTUPLE_0:def_12;
hence R_ProjCo p is total by PARTFUN1:def_2; ::_thesis: ( R_ProjCo p is symmetric & R_ProjCo p is transitive )
for x, y being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p holds
[y,x] in R_ProjCo p
proof
let x, y be set ; ::_thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p implies [y,x] in R_ProjCo p )
assume ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p ) ; ::_thesis: [y,x] in R_ProjCo p
then consider X, Y being Element of ProjCo (GF p) such that
A3: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
( x = X & y = Y ) by A3, XTUPLE_0:1;
hence [y,x] in R_ProjCo p by A3; ::_thesis: verum
end;
then R_ProjCo p is_symmetric_in field (R_ProjCo p) by RELAT_2:def_3;
hence R_ProjCo p is symmetric by RELAT_2:def_11; ::_thesis: R_ProjCo p is transitive
for x, y, z being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p holds
[x,z] in R_ProjCo p
proof
let x, y, z be set ; ::_thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p implies [x,z] in R_ProjCo p )
assume A4: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p ) ; ::_thesis: [x,z] in R_ProjCo p
then consider X, Y being Element of ProjCo (GF p) such that
A5: ( [x,y] = [X,Y] & X _EQ_ Y ) ;
A6: ( x = X & y = Y ) by A5, XTUPLE_0:1;
consider Y1, Z being Element of ProjCo (GF p) such that
A7: ( [y,z] = [Y1,Z] & Y1 _EQ_ Z ) by A4;
( X _EQ_ Y & Y _EQ_ Z ) by A5, A6, A7, XTUPLE_0:1;
then A8: X _EQ_ Z by Th44;
[x,z] = [X,Z] by A6, A7, XTUPLE_0:1;
hence [x,z] in R_ProjCo p by A8; ::_thesis: verum
end;
then R_ProjCo p is_transitive_in field (R_ProjCo p) by RELAT_2:def_8;
hence R_ProjCo p is transitive by RELAT_2:def_16; ::_thesis: verum
end;
end;
definition
let p be Prime;
let a, b be Element of (GF p);
func R_EllCur (a,b,p) -> Equivalence_Relation of (EC_SetProjCo (a,b,p)) equals :: EC_PF_1:def 12
(R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p)));
correctness
coherence
(R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p));
proof
set P = R_ProjCo p;
set R = nabla (EC_SetProjCo (a,b,p));
reconsider PR = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) as Relation of (EC_SetProjCo (a,b,p)) ;
for x being set holds
( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR )
proof
let x be set ; ::_thesis: ( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR )
hereby ::_thesis: ( ex y being set st [x,y] in PR implies x in EC_SetProjCo (a,b,p) )
assume A1: x in EC_SetProjCo (a,b,p) ; ::_thesis: ex y being set st [x,y] in PR
then reconsider X = x as Element of ProjCo (GF p) ;
X _EQ_ X ;
then A2: [x,x] in R_ProjCo p ;
[x,x] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87;
then [x,x] in PR by A2, XBOOLE_0:def_4;
hence ex y being set st [x,y] in PR ; ::_thesis: verum
end;
thus ( ex y being set st [x,y] in PR implies x in EC_SetProjCo (a,b,p) ) by ZFMISC_1:87; ::_thesis: verum
end;
then dom PR = EC_SetProjCo (a,b,p) by XTUPLE_0:def_12;
hence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)) by PARTFUN1:def_2; ::_thesis: verum
end;
end;
:: deftheorem defines R_EllCur EC_PF_1:def_12_:_
for p being Prime
for a, b being Element of (GF p) holds R_EllCur (a,b,p) = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p)));
theorem Th47: :: EC_PF_1:47
for p being Prime
for a, b being Element of (GF p)
for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p)
for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
let a, b be Element of (GF p); ::_thesis: for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
let P, Q be Element of ProjCo (GF p); ::_thesis: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) implies ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) )
assume A1: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) ) ; ::_thesis: ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
hereby ::_thesis: ( [P,Q] in R_EllCur (a,b,p) implies P _EQ_ Q )
assume P _EQ_ Q ; ::_thesis: [P,Q] in R_EllCur (a,b,p)
then A2: [P,Q] in R_ProjCo p ;
[P,Q] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87;
hence [P,Q] in R_EllCur (a,b,p) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume [P,Q] in R_EllCur (a,b,p) ; ::_thesis: P _EQ_ Q
then [P,Q] in R_ProjCo p by XBOOLE_0:def_4;
hence P _EQ_ Q by Th46; ::_thesis: verum
end;
theorem Th48: :: EC_PF_1:48
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
let a, b be Element of (GF p); ::_thesis: for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
let P be Element of ProjCo (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 ) ; ::_thesis: ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
set d = (P `3_3) " ;
A2: P `3_3 <> 0. (GF p) by A1, Th11;
A3: (P `3_3) " <> 0. (GF p)
proof
assume A4: (P `3_3) " = 0. (GF p) ; ::_thesis: contradiction
A5: ((P `3_3) ") * (P `3_3) = 1_ (GF p) by A2, VECTSP_1:def_10
.= 1 by Th12 ;
((P `3_3) ") * (P `3_3) = 0. (GF p) by A4, VECTSP_1:12
.= 0 by Th11 ;
hence contradiction by A5; ::_thesis: verum
end;
reconsider Q = [(((P `3_3) ") * (P `1_3)),(((P `3_3) ") * (P `2_3)),(((P `3_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
A6: ( Q `1_3 = ((P `3_3) ") * (P `1_3) & Q `2_3 = ((P `3_3) ") * (P `2_3) & Q `3_3 = ((P `3_3) ") * (P `3_3) ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7;
then Q in EC_SetProjCo (a,b,p) by A1, A3, Th45;
then consider PP being Element of ProjCo (GF p) such that
A7: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ;
reconsider Q = Q as Element of ProjCo (GF p) by A7;
take Q ; ::_thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
thus Q in EC_SetProjCo (a,b,p) by A6, A1, A3, Th45; ::_thesis: ( Q _EQ_ P & Q `3_3 = 1 )
thus Q _EQ_ P by A6, A3, Def10; ::_thesis: Q `3_3 = 1
thus Q `3_3 = ((P `3_3) ") * (P `3_3) by MCART_1:def_7
.= 1_ (GF p) by A2, VECTSP_1:def_10
.= 1 by Th12 ; ::_thesis: verum
end;
theorem Th49: :: EC_PF_1:49
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
let a, b be Element of (GF p); ::_thesis: for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
let P be Element of ProjCo (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 ) ; ::_thesis: ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
A2: P `3_3 = 0. (GF p) by A1, Th11;
set d = (P `2_3) " ;
A3: ex X0 being Element of ProjCo (GF p) st
( P = X0 & (EC_WEqProjCo (a,b,p)) . X0 = 0. (GF p) ) by A1;
A4: (P `3_3) |^ 3 = (P `3_3) |^ (2 + 1)
.= ((P `3_3) |^ 2) * (P `3_3) by Th24
.= 0. (GF p) by A2, VECTSP_1:12 ;
A5: (P `3_3) |^ 2 = (P `3_3) |^ (1 + 1)
.= ((P `3_3) |^ 1) * (P `3_3) by Th24
.= 0. (GF p) by A2, VECTSP_1:12 ;
0. (GF 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 A3, Def8
.= (0. (GF p)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A2, VECTSP_1:12
.= (0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (b * ((P `3_3) |^ 3))) by A5, VECTSP_1:12
.= (0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (0. (GF p))) by A4, VECTSP_1:12
.= (0. (GF p)) - (((P `1_3) |^ 3) + (0. (GF p))) by RLVECT_1:4
.= (0. (GF p)) - ((P `1_3) |^ 3) by RLVECT_1:4
.= - ((P `1_3) |^ 3) by RLVECT_1:14 ;
then A6: (P `1_3) |^ 3 = ((P `1_3) |^ 3) + (- ((P `1_3) |^ 3)) by RLVECT_1:4;
A7: P `1_3 = 0. (GF p)
proof
assume A8: P `1_3 <> 0. (GF p) ; ::_thesis: contradiction
then (P `1_3) * (P `1_3) <> 0. (GF p) by VECTSP_1:12;
then ((P `1_3) |^ 1) * (P `1_3) <> 0. (GF p) by Lm2;
then (P `1_3) |^ (1 + 1) <> 0. (GF p) by Th24;
then ((P `1_3) |^ 2) * (P `1_3) <> 0. (GF p) by A8, VECTSP_1:12;
then (P `1_3) |^ (2 + 1) <> 0. (GF p) by Th24;
hence contradiction by A6, RLVECT_1:5; ::_thesis: verum
end;
A9: P `2_3 <> 0. (GF p)
proof
assume P `2_3 = 0. (GF p) ; ::_thesis: contradiction
then P `2_3 = 0 by Th11;
then [(P `1_3),(P `2_3),(P `3_3)] = [0,0,0] by A1, A7, Th11;
then P = [0,0,0] by MCART_1:44;
then P in {[0,0,0]} by TARSKI:def_1;
then not P 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 not P in ProjCo (GF p) by Th40;
hence contradiction ; ::_thesis: verum
end;
A10: (P `2_3) " <> 0. (GF p)
proof
assume A11: (P `2_3) " = 0. (GF p) ; ::_thesis: contradiction
A12: ((P `2_3) ") * (P `2_3) = 1_ (GF p) by A9, VECTSP_1:def_10
.= 1 by Th12 ;
((P `2_3) ") * (P `2_3) = 0. (GF p) by A11, VECTSP_1:12
.= 0 by Th11 ;
hence contradiction by A12; ::_thesis: verum
end;
reconsider Q = [(((P `2_3) ") * (P `1_3)),(((P `2_3) ") * (P `2_3)),(((P `2_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
A13: ( Q `1_3 = ((P `2_3) ") * (P `1_3) & Q `2_3 = ((P `2_3) ") * (P `2_3) & Q `3_3 = ((P `2_3) ") * (P `3_3) ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7;
then Q in EC_SetProjCo (a,b,p) by A1, A10, Th45;
then consider PP being Element of ProjCo (GF p) such that
A14: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ;
reconsider Q = Q as Element of ProjCo (GF p) by A14;
take Q ; ::_thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus Q in EC_SetProjCo (a,b,p) by A13, A1, A10, Th45; ::_thesis: ( Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus Q _EQ_ P by A13, A10, Def10; ::_thesis: ( Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus Q `1_3 = ((P `2_3) ") * (P `1_3) by MCART_1:def_5
.= 0. (GF p) by A7, VECTSP_1:12
.= 0 by Th11 ; ::_thesis: ( Q `2_3 = 1 & Q `3_3 = 0 )
thus Q `2_3 = ((P `2_3) ") * (P `2_3) by MCART_1:def_6
.= 1_ (GF p) by A9, VECTSP_1:def_10
.= 1 by Th12 ; ::_thesis: Q `3_3 = 0
thus Q `3_3 = ((P `2_3) ") * (P `3_3) by MCART_1:def_7
.= 0. (GF p) by A2, VECTSP_1:12
.= 0 by Th11 ; ::_thesis: verum
end;
theorem Th50: :: EC_PF_1:50
for p being Prime
for a, b being Element of (GF p)
for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p)
for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let a, b be Element of (GF p); ::_thesis: for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let x be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) implies ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) ) ; ::_thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y0 being Element of EC_SetProjCo (a,b,p) such that
A2: x = Class ((R_EllCur (a,b,p)),y0) by EQREL_1:36;
reconsider w = y0 as Element of ProjCo (GF p) ;
percases ( w `3_3 = 0 or w `3_3 <> 0 ) ;
suppose w `3_3 = 0 ; ::_thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y being Element of ProjCo (GF p) such that
A3: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `1_3 = 0 & y `2_3 = 1 & y `3_3 = 0 ) by A1, Th49;
[y,w] in R_EllCur (a,b,p) by A1, Th47, A3;
then x = Class ((R_EllCur (a,b,p)),y) by A2, A3, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A3, MCART_1:44; ::_thesis: verum
end;
suppose w `3_3 <> 0 ; ::_thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y being Element of ProjCo (GF p) such that
A4: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `3_3 = 1 ) by A1, Th48;
set e = y `1_3 ;
set f = y `2_3 ;
A5: y = [(y `1_3),(y `2_3),1] by A4, MCART_1:44;
[y,w] in R_EllCur (a,b,p) by A1, Th47, A4;
then x = Class ((R_EllCur (a,b,p)),y) by A2, A4, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A5, A4; ::_thesis: verum
end;
end;
end;
theorem Th51: :: EC_PF_1:51
for p being Prime
for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
set A = Class (R_EllCur (a,b,p));
set B = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ;
reconsider d0 = [0,1,0] as Element of EC_SetProjCo (a,b,p) by Th42;
for x being set holds
( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
proof
let x be set ; ::_thesis: ( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
hereby ::_thesis: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in Class (R_EllCur (a,b,p)) )
assume x in Class (R_EllCur (a,b,p)) ; ::_thesis: x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
then ( ex y being Element of ProjCo (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [0,1,0] & x = Class ((R_EllCur (a,b,p)),y) ) or ex y being Element of ProjCo (GF p) ex e, f being Element of (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [e,f,1] & x = Class ((R_EllCur (a,b,p)),y) ) ) by A1, Th50;
then ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by TARSKI:def_1;
hence x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by XBOOLE_0:def_3; ::_thesis: verum
end;
assume x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; ::_thesis: x in Class (R_EllCur (a,b,p))
then A2: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by XBOOLE_0:def_3;
now__::_thesis:_x_in_Class_(R_EllCur_(a,b,p))
percases ( x = Class ((R_EllCur (a,b,p)),[0,1,0]) or ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ) by A2, TARSKI:def_1;
supposeA3: x = Class ((R_EllCur (a,b,p)),[0,1,0]) ; ::_thesis: x in Class (R_EllCur (a,b,p))
EqClass ((R_EllCur (a,b,p)),d0) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by A3; ::_thesis: verum
end;
suppose ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ; ::_thesis: x in Class (R_EllCur (a,b,p))
then consider y being Element of ProjCo (GF p) such that
A4: ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ;
reconsider y = y as Element of EC_SetProjCo (a,b,p) by A4;
EqClass ((R_EllCur (a,b,p)),y) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by A4; ::_thesis: verum
end;
end;
end;
hence x in Class (R_EllCur (a,b,p)) ; ::_thesis: verum
end;
hence Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:1; ::_thesis: verum
end;
theorem Th52: :: EC_PF_1:52
for p being 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 ) )
proof
let p be Prime; ::_thesis: 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); ::_thesis: ( 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 A1: ( 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) ) ; ::_thesis: ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) )
hereby ::_thesis: ( 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]) ; ::_thesis: ( d2 = d1 & Y2 = Y1 )
then [d2,Y2,1] in Class ((R_EllCur (a,b,p)),[d1,Y1,1]) by A1, EQREL_1:23;
then A2: [[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 A1;
P _EQ_ Q by Th47, A1, A2;
then consider a being Element of (GF p) such that
A3: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10;
A4: p > 1 by INT_2:def_4;
A5: 1. (GF p) = 1 by A4, INT_3:14
.= P `3_3 by MCART_1:def_7 ;
A6: 1. (GF p) = 1 by A4, INT_3:14
.= a * (P `3_3) by A3, MCART_1:def_7
.= a by A5, VECTSP_1:def_8 ;
thus d2 = a * (P `1_3) by A3, MCART_1:def_5
.= P `1_3 by A6, VECTSP_1:def_8
.= d1 by MCART_1:def_5 ; ::_thesis: Y2 = Y1
thus Y2 = a * (P `2_3) by A3, MCART_1:def_6
.= P `2_3 by A6, VECTSP_1:def_8
.= Y1 by MCART_1:def_6 ; ::_thesis: verum
end;
assume ( d1 = d2 & Y1 = Y2 ) ; ::_thesis: 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]) ; ::_thesis: verum
end;
theorem Th53: :: EC_PF_1:53
for p being Prime
for a, b being Element of (GF p)
for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds
F1 misses F2
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p)
for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds
F1 misses F2
let a, b be Element of (GF p); ::_thesis: for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds
F1 misses F2
let F1, F2 be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies F1 misses F2 )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) ; ::_thesis: F1 misses F2
assume F1 meets F2 ; ::_thesis: contradiction
then F1 /\ F2 <> {} by XBOOLE_0:def_7;
then consider z being set such that
A2: z in F1 /\ F2 by XBOOLE_0:def_1;
A3: ( z in F1 & z in F2 ) by A2, XBOOLE_0:def_4;
consider P being Element of ProjCo (GF p) such that
A4: ( z = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) by A1, A3;
consider X1, Y1 being Element of (GF p) such that
A5: P = [X1,Y1,1] by A4;
A6: z = Class ((R_EllCur (a,b,p)),[0,1,0]) by A1, A3, TARSKI:def_1;
reconsider Q = [0,1,0] as Element of ProjCo (GF p) by Lm6;
A7: Q is Element of EC_SetProjCo (a,b,p) by Th42;
Q in Class ((R_EllCur (a,b,p)),P) by A4, A6, EQREL_1:23;
then [P,Q] in R_EllCur (a,b,p) by EQREL_1:18;
then P _EQ_ Q by Th47, A1, A7, A4;
then consider a being Element of (GF p) such that
A8: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10;
A9: p > 1 by INT_2:def_4;
A10: 1. (GF p) = 1 by A9, INT_3:14
.= P `3_3 by A5, MCART_1:def_7 ;
0. (GF p) = 0 by Th11
.= a * (P `3_3) by A8, MCART_1:def_7
.= a by A10, VECTSP_1:def_8 ;
hence contradiction by A8; ::_thesis: verum
end;
theorem Th54: :: EC_PF_1:54
for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b2 -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X
proof
let X be non empty finite set ; ::_thesis: for R being Equivalence_Relation of X
for S being Class b1 -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X
let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X
let S be Class R -valued Function; ::_thesis: for i being set st i in dom S holds
S . i is finite Subset of X
let i be set ; ::_thesis: ( i in dom S implies S . i is finite Subset of X )
assume i in dom S ; ::_thesis: S . i is finite Subset of X
then S . i in Class R by FUNCT_1:102;
hence S . i is finite Subset of X ; ::_thesis: verum
end;
theorem Th55: :: EC_PF_1:55
for X being non empty set
for R being Equivalence_Relation of X
for S being Class b2 -valued Function st S is one-to-one holds
S is disjoint_valued
proof
let X be non empty set ; ::_thesis: for R being Equivalence_Relation of X
for S being Class b1 -valued Function st S is one-to-one holds
S is disjoint_valued
let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function st S is one-to-one holds
S is disjoint_valued
let S be Class R -valued Function; ::_thesis: ( S is one-to-one implies S is disjoint_valued )
assume A1: S is one-to-one ; ::_thesis: S is disjoint_valued
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
S_._x_misses_S_._y
let x, y be set ; ::_thesis: ( x <> y implies S . b1 misses S . b2 )
assume A2: x <> y ; ::_thesis: S . b1 misses S . b2
percases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ;
supposeA3: ( x in dom S & y in dom S ) ; ::_thesis: S . b1 misses S . b2
then A4: S . x <> S . y by A1, A2, FUNCT_1:def_4;
( S . x in Class R & S . y in Class R ) by A3, FUNCT_1:102;
hence S . x misses S . y by A4, EQREL_1:def_4; ::_thesis: verum
end;
suppose ( not x in dom S or not y in dom S ) ; ::_thesis: S . b1 misses S . b2
then ( S . x = {} or S . y = {} ) by FUNCT_1:def_2;
hence S . x misses S . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence S is disjoint_valued by PROB_2:def_2; ::_thesis: verum
end;
theorem Th56: :: EC_PF_1:56
for X being non empty set
for R being Equivalence_Relation of X
for S being Class b2 -valued Function st S is onto holds
Union S = X
proof
let X be non empty set ; ::_thesis: for R being Equivalence_Relation of X
for S being Class b1 -valued Function st S is onto holds
Union S = X
let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function st S is onto holds
Union S = X
let S be Class R -valued Function; ::_thesis: ( S is onto implies Union S = X )
assume A1: S is onto ; ::_thesis: Union S = X
union (Class R) = X by EQREL_1:def_4;
hence Union S = X by A1, FUNCT_2:def_3; ::_thesis: verum
end;
theorem :: EC_PF_1:57
for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b2 -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
proof
let X be non empty finite set ; ::_thesis: for R being Equivalence_Relation of X
for S being Class b1 -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function
for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let S be Class R -valued Function; ::_thesis: for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) holds
card X = Sum L
let L be FinSequence of NAT ; ::_thesis: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) implies card X = Sum L )
assume A1: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds
L . i = card (S . i) ) ) ; ::_thesis: card X = Sum L
A2: S is disjoint_valued by A1, Th55;
A3: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by A1, Th54;
Union S = X by Th56, A1;
hence card X = Sum L by A1, A2, A3, DIST_1:17; ::_thesis: verum
end;
theorem Th58: :: EC_PF_1:58
for p being Prime
for a, b, d being Element of (GF p)
for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds
ex I being Function of F,G st
( I is onto & I is one-to-one )
proof
let p be Prime; ::_thesis: for a, b, d being Element of (GF p)
for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds
ex I being Function of F,G st
( I is onto & I is one-to-one )
let a, b, d be Element of (GF p); ::_thesis: for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds
ex I being Function of F,G st
( I is onto & I is one-to-one )
let F, G be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } implies ex I being Function of F,G st
( I is onto & I is one-to-one ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,P,1])) where P is Element of (GF p) : [d,P,1] in EC_SetProjCo (a,b,p) } ) ; ::_thesis: ex I being Function of F,G st
( I is onto & I is one-to-one )
consider z being set such that
A2: z in F by A1, XBOOLE_0:def_1;
consider W being Element of (GF p) such that
A3: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A2;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by A3, Th43;
then A4: Class ((R_EllCur (a,b,p)),[d,W,1]) in G by A1;
deffunc H1( set ) -> Element of bool (EC_SetProjCo (a,b,p)) = Class ((R_EllCur (a,b,p)),[d,$1,1]);
A5: for x being set st x in F holds
H1(x) in G
proof
let x be set ; ::_thesis: ( x in F implies H1(x) in G )
assume x in F ; ::_thesis: H1(x) in G
then consider Y being Element of (GF p) such that
A6: ( x = Y & Y |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1;
[d,Y,1] is Element of EC_SetProjCo (a,b,p) by A6, Th43;
hence H1(x) in G by A1, A6; ::_thesis: verum
end;
consider I being Function of F,G such that
A7: for x being set st x in F holds
I . x = H1(x) from FUNCT_2:sch_2(A5);
take I ; ::_thesis: ( I is onto & I is one-to-one )
now__::_thesis:_for_y_being_set_st_y_in_G_holds_
y_in_rng_I
let y be set ; ::_thesis: ( y in G implies y in rng I )
assume y in G ; ::_thesis: y in rng I
then consider P being Element of (GF p) such that
A8: ( y = Class ((R_EllCur (a,b,p)),[d,P,1]) & [d,P,1] in EC_SetProjCo (a,b,p) ) by A1;
P |^ 2 = ((d |^ 3) + (a * d)) + b by A8, Th43;
then A9: P in F by A1;
then y = I . P by A7, A8;
hence y in rng I by A9, A4, FUNCT_2:112; ::_thesis: verum
end;
then G c= rng I by TARSKI:def_3;
then G = rng I by XBOOLE_0:def_10;
hence I is onto by FUNCT_2:def_3; ::_thesis: I is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_I_&_x2_in_dom_I_&_I_._x1_=_I_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 implies x1 = x2 )
assume A10: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 ) ; ::_thesis: x1 = x2
A11: ( x1 in F & x2 in F ) by A10;
then consider Y1 being Element of (GF p) such that
A12: ( x1 = Y1 & Y1 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1;
consider Y2 being Element of (GF p) such that
A13: ( x2 = Y2 & Y2 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A11;
A14: I . x1 = Class ((R_EllCur (a,b,p)),[d,x1,1]) by A10, A7;
A15: Class ((R_EllCur (a,b,p)),[d,x1,1]) = Class ((R_EllCur (a,b,p)),[d,x2,1]) by A10, A7, A14;
A16: [d,Y2,1] is Element of EC_SetProjCo (a,b,p) by Th43, A13;
[d,Y1,1] is Element of EC_SetProjCo (a,b,p) by Th43, A12;
hence x1 = x2 by A1, A12, A13, A15, A16, Th52; ::_thesis: verum
end;
hence I is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th59: :: EC_PF_1:59
for p being Prime
for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
proof
let p be Prime; ::_thesis: for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
let a, b, d be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
set F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
set G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ;
percases ( { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} or { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ) ;
supposeA2: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
A3: { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = {}
proof
assume { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } <> {} ; ::_thesis: contradiction
then consider z being set such that
A4: z in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by XBOOLE_0:def_1;
consider Y being Element of (GF p) such that
A5: ( z = Class ((R_EllCur (a,b,p)),[d,Y,1]) & [d,Y,1] in EC_SetProjCo (a,b,p) ) by A4;
Y |^ 2 = ((d |^ 3) + (a * d)) + b by A5, Th43;
then Y in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
hence contradiction by A2; ::_thesis: verum
end;
2 < p by A1, XXREAL_0:2;
hence card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by A3, A2, Th39; ::_thesis: verum
end;
supposeA6: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
then consider z being set such that
A7: z in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by XBOOLE_0:def_1;
consider W being Element of (GF p) such that
A8: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A7;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by A8, Th43;
then A9: Class ((R_EllCur (a,b,p)),[d,W,1]) in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ;
consider I being Function of { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } , { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } such that
A10: ( I is onto & I is one-to-one ) by A1, A6, Th58;
A11: dom I = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A9, FUNCT_2:def_1;
A12: rng I = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A10, FUNCT_2:def_3;
then A13: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } c= card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A10, A11, CARD_1:10;
reconsider h = I " as Function of { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } , { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A10, A12, FUNCT_2:25;
( (I ") * I = id { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & I * (I ") = id { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ) by A10, A12, A9, FUNCT_2:29;
then A14: ( h is onto & h is one-to-one ) by FUNCT_2:23;
then A15: rng h = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by FUNCT_2:def_3;
dom h = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A6, FUNCT_2:def_1;
then card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } c= card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A14, A15, CARD_1:10;
then A16: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A13, XBOOLE_0:def_10;
2 < p by A1, XXREAL_0:2;
hence card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by A16, Th39; ::_thesis: verum
end;
end;
end;
Lm8: for p being Prime
for n being Nat st n in Seg p holds
n - 1 is Element of (GF p)
proof
let p be Prime; ::_thesis: for n being Nat st n in Seg p holds
n - 1 is Element of (GF p)
let n be Nat; ::_thesis: ( n in Seg p implies n - 1 is Element of (GF p) )
assume n in Seg p ; ::_thesis: n - 1 is Element of (GF p)
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A1: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A2: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A1, XXREAL_0:2;
hence n - 1 is Element of (GF p) by A2, NAT_1:44; ::_thesis: verum
end;
Lm9: for p being Prime
for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex S being Function st
( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
proof
let p be Prime; ::_thesis: for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex S being Function st
( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
let a, b, c, d be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex S being Function st
( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex S being Function st
( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
deffunc H1( Nat) -> set = { (Class ((R_EllCur (a,b,p)),[($1 - 1),Y,1])) where Y is Element of (GF p) : [($1 - 1),Y,1] in EC_SetProjCo (a,b,p) } ;
consider S being FinSequence such that
A2: ( len S = p & ( for i being Nat st i in dom S holds
S . i = H1(i) ) ) from FINSEQ_1:sch_2();
take S ; ::_thesis: ( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
thus A3: dom S = Seg p by A2, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
thus for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2; ::_thesis: ( S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
S_._x_misses_S_._y
let x, y be set ; ::_thesis: ( x <> y implies S . b1 misses S . b2 )
assume A4: x <> y ; ::_thesis: S . b1 misses S . b2
percases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ;
supposeA5: ( x in dom S & y in dom S ) ; ::_thesis: S . b1 misses S . b2
then reconsider n = x, m = y as Nat ;
( x in Seg p & y in Seg p ) by A5, A2, FINSEQ_1:def_3;
then A6: ( n - 1 is Element of (GF p) & m - 1 is Element of (GF p) ) by Lm8;
A7: S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A5, A2;
A8: S . m = { (Class ((R_EllCur (a,b,p)),[(m - 1),Y,1])) where Y is Element of (GF p) : [(m - 1),Y,1] in EC_SetProjCo (a,b,p) } by A5, A2;
thus S . x misses S . y ::_thesis: verum
proof
assume S . x meets S . y ; ::_thesis: contradiction
then consider z being set such that
A9: ( z in S . x & z in S . y ) by XBOOLE_0:3;
consider Yx being Element of (GF p) such that
A10: ( z = Class ((R_EllCur (a,b,p)),[(n - 1),Yx,1]) & [(n - 1),Yx,1] in EC_SetProjCo (a,b,p) ) by A7, A9;
consider Yy being Element of (GF p) such that
A11: ( z = Class ((R_EllCur (a,b,p)),[(m - 1),Yy,1]) & [(m - 1),Yy,1] in EC_SetProjCo (a,b,p) ) by A8, A9;
n - 1 = m - 1 by Th52, A1, A10, A11, A6;
hence contradiction by A4; ::_thesis: verum
end;
end;
suppose ( not x in dom S or not y in dom S ) ; ::_thesis: S . b1 misses S . b2
then ( S . x = {} or S . y = {} ) by FUNCT_1:def_2;
hence S . x misses S . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence S is disjoint_valued by PROB_2:def_2; ::_thesis: ( ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
thus for n being Nat st n in dom S holds
S . n is finite ::_thesis: Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
proof
let n be Nat; ::_thesis: ( n in dom S implies S . n is finite )
assume A12: n in dom S ; ::_thesis: S . n is finite
then A13: S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2;
( 1 <= n & n <= p ) by A12, A3, FINSEQ_1:1;
then A14: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A15: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A14, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A15, NAT_1:44;
A16: card (S . n) = card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A13
.= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by Th59, A1 ;
0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
proof
percases ( ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) or ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ;
suppose ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
then Lege_p (((d |^ 3) + (a * d)) + b) = - 1 by Def5;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum
end;
supposeA17: ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
now__::_thesis:_0_<=_1_+_(Lege_p_(((d_|^_3)_+_(a_*_d))_+_b))
percases ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) by A17;
suppose ((d |^ 3) + (a * d)) + b = 0 ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
then Lege_p (((d |^ 3) + (a * d)) + b) = 0 by Def5;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum
end;
suppose ((d |^ 3) + (a * d)) + b is quadratic_residue ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
then Lege_p (((d |^ 3) + (a * d)) + b) = 1 by Def5;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum
end;
end;
end;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum
end;
end;
end;
then card (S . n) in NAT by A16, INT_1:3;
hence S . n is finite ; ::_thesis: verum
end;
set B = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ;
for x being set holds
( x in union (rng S) iff x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
proof
let x be set ; ::_thesis: ( x in union (rng S) iff x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
hereby ::_thesis: ( x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in union (rng S) )
assume x in union (rng S) ; ::_thesis: x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
then consider Z being set such that
A18: ( x in Z & Z in rng S ) by TARSKI:def_4;
consider n being set such that
A19: ( n in dom S & Z = S . n ) by A18, FUNCT_1:def_3;
reconsider n = n as Nat by A19;
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A19, A2;
then consider Y being Element of (GF p) such that
A20: ( x = Class ((R_EllCur (a,b,p)),[(n - 1),Y,1]) & [(n - 1),Y,1] in EC_SetProjCo (a,b,p) ) by A18, A19;
n - 1 is Element of (GF p) by A3, A19, Lm8;
hence x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by A20; ::_thesis: verum
end;
assume x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; ::_thesis: x in union (rng S)
then consider P being Element of ProjCo (GF p) such that
A21: ( x = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) ;
consider X, Y being Element of (GF p) such that
A22: P = [X,Y,1] by A21;
reconsider n1 = X as Nat ;
A23: ( 0 <= n1 & n1 < p ) by NAT_1:44;
A24: 0 + 1 <= n1 + 1 by XREAL_1:6;
A25: n1 + 1 <= p by A23, NAT_1:13;
set n = n1 + 1;
A26: ( n1 + 1 in Seg p & (n1 + 1) - 1 = X ) by A24, A25;
x in { (Class ((R_EllCur (a,b,p)),[((n1 + 1) - 1),Q,1])) where Q is Element of (GF p) : [((n1 + 1) - 1),Q,1] in EC_SetProjCo (a,b,p) } by A21, A22;
then A27: x in S . (n1 + 1) by A26, A2, A3;
S . (n1 + 1) in rng S by A26, A3, FUNCT_1:3;
hence x in union (rng S) by A27, TARSKI:def_4; ::_thesis: verum
end;
hence Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:1; ::_thesis: verum
end;
theorem Th60: :: EC_PF_1:60
for p being Prime
for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F )
let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F )
then consider S being Function such that
A2: ( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) by Lm9;
defpred S1[ Nat, Nat] means $2 = card (S . $1);
A3: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_p_holds_
ex_x_being_Element_of_NAT_st_S1[i,x]
let i be Nat; ::_thesis: ( i in Seg p implies ex x being Element of NAT st S1[i,x] )
assume i in Seg p ; ::_thesis: ex x being Element of NAT st S1[i,x]
then S . i is finite by A2;
then reconsider x = card (S . i) as Element of NAT by ORDINAL1:def_12;
take x = x; ::_thesis: S1[i,x]
thus S1[i,x] ; ::_thesis: verum
end;
consider L being FinSequence of NAT such that
A4: ( dom L = Seg p & ( for i being Nat st i in Seg p holds
S1[i,L . i] ) ) from FINSEQ_1:sch_5(A3);
take L ; ::_thesis: ( len L = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L )
p is Element of NAT by ORDINAL1:def_12;
hence len L = p by A4, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L )
A5: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_p_holds_
ex_d_being_Element_of_(GF_p)_st_
(_d_=_n_-_1_&_L_._n_=_1_+_(Lege_p_(((d_|^_3)_+_(a_*_d))_+_b))_)
let n be Nat; ::_thesis: ( n in Seg p implies ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) )
assume A6: n in Seg p ; ::_thesis: ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A7: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A8: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A7, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A8, NAT_1:44;
take d = d; ::_thesis: ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
thus d = n - 1 ; ::_thesis: L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
thus L . n = card (S . n) by A4, A6
.= card { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2, A6
.= card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
.= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by Th59, A1 ; ::_thesis: verum
end;
for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by A2, A4;
hence ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) by A2, A4, A5, DIST_1:17; ::_thesis: verum
end;
theorem :: EC_PF_1:61
for p being Prime
for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of INT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
proof
let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of INT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex F being FinSequence of INT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex F being FinSequence of INT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
then consider L being FinSequence of NAT such that
A2: ( len L = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) by Th60;
A3: p is Element of NAT by ORDINAL1:def_12;
defpred S1[ Nat, set ] means ex d being Element of (GF p) st
( d = $1 - 1 & $2 = Lege_p (((d |^ 3) + (a * d)) + b) );
A4: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_p_holds_
ex_x_being_Element_of_INT_st_S1[n,x]
let n be Nat; ::_thesis: ( n in Seg p implies ex x being Element of INT st S1[n,x] )
assume n in Seg p ; ::_thesis: ex x being Element of INT st S1[n,x]
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A5: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A6: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A5, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A6, NAT_1:44;
reconsider x = Lege_p (((d |^ 3) + (a * d)) + b) as Element of INT by INT_1:def_2;
take x = x; ::_thesis: S1[n,x]
thus S1[n,x] ; ::_thesis: verum
end;
consider F being FinSequence of INT such that
A7: ( dom F = Seg p & ( for i being Nat st i in Seg p holds
S1[i,F . i] ) ) from FINSEQ_1:sch_5(A4);
take F ; ::_thesis: ( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
thus A8: len F = p by A7, A3, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
reconsider pp = p |-> 1 as Element of p -tuples_on REAL ;
F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:15;
then reconsider FF = F as Element of p -tuples_on REAL by A8, FINSEQ_2:92;
A9: now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_p_holds_
L_._n_=_(pp_+_FF)_._n
let n be Nat; ::_thesis: ( 1 <= n & n <= p implies L . n = (pp + FF) . n )
assume ( 1 <= n & n <= p ) ; ::_thesis: L . n = (pp + FF) . n
then A10: n in Seg p by FINSEQ_1:1;
then A11: ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) by A2;
ex f being Element of (GF p) st
( f = n - 1 & F . n = Lege_p (((f |^ 3) + (a * f)) + b) ) by A7, A10;
then L . n = ((p |-> 1) . n) + (F . n) by A11, A10, FUNCOP_1:7;
hence L . n = (pp + FF) . n by RVSUM_1:11; ::_thesis: verum
end;
len (pp + FF) = p by A3, FINSEQ_2:132;
then L = pp + FF by A2, A9, FINSEQ_1:14;
then Sum L = (Sum (p |-> 1)) + (Sum F) by RVSUM_1:89;
then A12: Sum L = (p * 1) + (Sum F) by RVSUM_1:80;
reconsider F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} as finite set ;
reconsider F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } as finite set by A2;
A13: card F1 = 1 by CARD_2:42;
card (Class (R_EllCur (a,b,p))) = card (F1 \/ F2) by A1, Th51
.= 1 + (p + (Sum F)) by A1, A13, A2, A12, Th53, CARD_2:40 ;
hence ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) by A7; ::_thesis: verum
end;