:: Several Properties of Fields. Field Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: REALSET3:1
canceled;
theorem Th2: :: REALSET3:2
theorem :: REALSET3:3
canceled;
theorem Th4: :: REALSET3:4
theorem :: REALSET3:5
canceled;
theorem Th6: :: REALSET3:6
theorem Th7: :: REALSET3:7
theorem Th8: :: REALSET3:8
theorem :: REALSET3:9
canceled;
theorem :: REALSET3:10
theorem :: REALSET3:11
for
F being
Field for
a,
b being
Element of the
carrier of
F for
c,
d being
Element of the
carrier of
F \ {(0. F)} holds the
addF of
F . ((omf F) . a,((revf F) . c)),
((omf F) . b,((revf F) . d)) = (omf F) . (the addF of F . ((omf F) . a,d),((omf F) . b,c)),
((revf F) . ((omf F) . c,d))
definition
let F be
Field;
func osf F -> BinOp of the
carrier of
F means :
Def1:
:: REALSET3:def 1
for
x,
y being
Element of the
carrier of
F holds
it . x,
y = the
addF of
F . x,
((comp F) . y);
existence
ex b1 being BinOp of the carrier of F st
for x, y being Element of the carrier of F holds b1 . x,y = the addF of F . x,((comp F) . y)
uniqueness
for b1, b2 being BinOp of the carrier of F st ( for x, y being Element of the carrier of F holds b1 . x,y = the addF of F . x,((comp F) . y) ) & ( for x, y being Element of the carrier of F holds b2 . x,y = the addF of F . x,((comp F) . y) ) holds
b1 = b2
end;
:: deftheorem Def1 defines osf REALSET3:def 1 :
theorem :: REALSET3:12
canceled;
theorem :: REALSET3:13
canceled;
theorem :: REALSET3:14
theorem Th15: :: REALSET3:15
theorem :: REALSET3:16
canceled;
theorem :: REALSET3:17
theorem :: REALSET3:18
theorem :: REALSET3:19
theorem Th20: :: REALSET3:20
theorem :: REALSET3:21
theorem Th22: :: REALSET3:22
theorem :: REALSET3:23
theorem :: REALSET3:24
theorem :: REALSET3:25
theorem :: REALSET3:26
definition
let F be
Field;
func ovf F -> Function of
[:the carrier of F,(the carrier of F \ {(0. F)}):],the
carrier of
F means :
Def2:
:: REALSET3:def 2
for
x being
Element of the
carrier of
F for
y being
Element of the
carrier of
F \ {(0. F)} holds
it . x,
y = (omf F) . x,
((revf F) . y);
existence
ex b1 being Function of [:the carrier of F,(the carrier of F \ {(0. F)}):],the carrier of F st
for x being Element of the carrier of F
for y being Element of the carrier of F \ {(0. F)} holds b1 . x,y = (omf F) . x,((revf F) . y)
uniqueness
for b1, b2 being Function of [:the carrier of F,(the carrier of F \ {(0. F)}):],the carrier of F st ( for x being Element of the carrier of F
for y being Element of the carrier of F \ {(0. F)} holds b1 . x,y = (omf F) . x,((revf F) . y) ) & ( for x being Element of the carrier of F
for y being Element of the carrier of F \ {(0. F)} holds b2 . x,y = (omf F) . x,((revf F) . y) ) holds
b1 = b2
end;
:: deftheorem Def2 defines ovf REALSET3:def 2 :
theorem :: REALSET3:27
canceled;
theorem :: REALSET3:28
canceled;
theorem Th29: :: REALSET3:29
theorem :: REALSET3:30
canceled;
theorem Th31: :: REALSET3:31
theorem :: REALSET3:32
theorem :: REALSET3:33
canceled;
theorem :: REALSET3:34
canceled;
theorem :: REALSET3:35
theorem :: REALSET3:36
theorem Th37: :: REALSET3:37
theorem :: REALSET3:38
theorem Th39: :: REALSET3:39
theorem :: REALSET3:40
theorem :: REALSET3:41
theorem :: REALSET3:42
theorem :: REALSET3:43