:: Several Properties of Fields. Field Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users


begin

theorem :: REALSET3:1
canceled;

theorem Th2: :: REALSET3:2
for F being Field holds (revf F) . (1. F) = 1. F
proof end;

theorem :: REALSET3:3
canceled;

theorem Th4: :: REALSET3:4
for F being Field
for a, b being Element of NonZero F holds (revf F) . ((omf F) . a,((revf F) . b)) = (omf F) . b,((revf F) . a)
proof end;

theorem :: REALSET3:5
canceled;

theorem Th6: :: REALSET3:6
for F being Field
for a, b being Element of NonZero F holds (revf F) . ((omf F) . a,b) = (omf F) . ((revf F) . a),((revf F) . b)
proof end;

theorem Th7: :: REALSET3:7
for F being Field
for a, b, c, d being Element of F holds
( a - b = c - d iff a + d = b + c )
proof end;

theorem Th8: :: REALSET3:8
for F being Field
for a, c being Element of F
for b, d being Element of NonZero F holds
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
proof end;

theorem :: REALSET3:9
canceled;

theorem :: REALSET3:10
for F being Field
for a, b being Element of F
for c, d being Element of NonZero F holds (omf F) . ((omf F) . a,((revf F) . c)),((omf F) . b,((revf F) . d)) = (omf F) . ((omf F) . a,b),((revf F) . ((omf F) . c,d))
proof end;

theorem :: REALSET3:11
for F being Field
for a, b being Element of F
for c, d being Element of NonZero 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))
proof end;

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 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 F holds b1 . x,y = the addF of F . x,((comp F) . y)
proof end;
uniqueness
for b1, b2 being BinOp of the carrier of F st ( for x, y being Element of F holds b1 . x,y = the addF of F . x,((comp F) . y) ) & ( for x, y being Element of F holds b2 . x,y = the addF of F . x,((comp F) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines osf REALSET3:def 1 :
for F being Field
for b2 being BinOp of the carrier of F holds
( b2 = osf F iff for x, y being Element of F holds b2 . x,y = the addF of F . x,((comp F) . y) );

theorem :: REALSET3:12
canceled;

theorem :: REALSET3:13
canceled;

theorem :: REALSET3:14
for F being Field
for x being Element of F holds (osf F) . x,x = 0. F
proof end;

theorem Th15: :: REALSET3:15
for F being Field
for a, b, c being Element of F holds (omf F) . a,((osf F) . b,c) = (osf F) . ((omf F) . a,b),((omf F) . a,c)
proof end;

theorem :: REALSET3:16
canceled;

theorem :: REALSET3:17
for F being Field
for a, b, c being Element of F holds (omf F) . ((osf F) . a,b),c = (osf F) . ((omf F) . a,c),((omf F) . b,c)
proof end;

theorem :: REALSET3:18
for F being Field
for a, b being Element of F holds (osf F) . a,b = (comp F) . ((osf F) . b,a)
proof end;

theorem :: REALSET3:19
for F being Field
for a, b being Element of F holds (osf F) . ((comp F) . a),b = (comp F) . (the addF of F . a,b)
proof end;

theorem Th20: :: REALSET3:20
for F being Field
for a, b, c, d being Element of F holds
( (osf F) . a,b = (osf F) . c,d iff a + d = b + c )
proof end;

theorem :: REALSET3:21
for F being Field
for a being Element of F holds (osf F) . (0. F),a = (comp F) . a
proof end;

theorem Th22: :: REALSET3:22
for F being Field
for a being Element of F holds (osf F) . a,(0. F) = a
proof end;

theorem :: REALSET3:23
for F being Field
for a, b, c being Element of F holds
( a + b = c iff (osf F) . c,a = b )
proof end;

theorem :: REALSET3:24
for F being Field
for a, b, c being Element of F holds
( a + b = c iff (osf F) . c,b = a )
proof end;

theorem :: REALSET3:25
for F being Field
for a, b, c being Element of F holds (osf F) . a,((osf F) . b,c) = the addF of F . ((osf F) . a,b),c
proof end;

theorem :: REALSET3:26
for F being Field
for a, b, c being Element of F holds (osf F) . a,(the addF of F . b,c) = (osf F) . ((osf F) . a,b),c
proof end;

definition
let F be Field;
func ovf F -> Function of [:the carrier of F,(NonZero F):],the carrier of F means :Def2: :: REALSET3:def 2
for x being Element of F
for y being Element of NonZero F holds it . x,y = (omf F) . x,((revf F) . y);
existence
ex b1 being Function of [:the carrier of F,(NonZero F):],the carrier of F st
for x being Element of F
for y being Element of NonZero F holds b1 . x,y = (omf F) . x,((revf F) . y)
proof end;
uniqueness
for b1, b2 being Function of [:the carrier of F,(NonZero F):],the carrier of F st ( for x being Element of F
for y being Element of NonZero F holds b1 . x,y = (omf F) . x,((revf F) . y) ) & ( for x being Element of F
for y being Element of NonZero F holds b2 . x,y = (omf F) . x,((revf F) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ovf REALSET3:def 2 :
for F being Field
for b2 being Function of [:the carrier of F,(NonZero F):],the carrier of F holds
( b2 = ovf F iff for x being Element of F
for y being Element of NonZero F holds b2 . x,y = (omf F) . x,((revf F) . y) );

theorem :: REALSET3:27
canceled;

theorem :: REALSET3:28
canceled;

theorem Th29: :: REALSET3:29
for F being Field
for x being Element of NonZero F holds (ovf F) . x,x = 1. F
proof end;

theorem :: REALSET3:30
canceled;

theorem Th31: :: REALSET3:31
for F being Field
for a, b being Element of F
for c being Element of NonZero F holds (omf F) . a,((ovf F) . b,c) = (ovf F) . ((omf F) . a,b),c
proof end;

theorem :: REALSET3:32
for F being Field
for a being Element of NonZero F holds
( (omf F) . a,((ovf F) . (1. F),a) = 1. F & (omf F) . ((ovf F) . (1. F),a),a = 1. F )
proof end;

theorem :: REALSET3:33
canceled;

theorem :: REALSET3:34
canceled;

theorem :: REALSET3:35
for F being Field
for a, b being Element of NonZero F holds (ovf F) . a,b = (revf F) . ((ovf F) . b,a)
proof end;

theorem :: REALSET3:36
for F being Field
for a, b being Element of NonZero F holds (ovf F) . ((revf F) . a),b = (revf F) . ((omf F) . a,b)
proof end;

theorem Th37: :: REALSET3:37
for F being Field
for a, c being Element of F
for b, d being Element of NonZero F holds
( (ovf F) . a,b = (ovf F) . c,d iff (omf F) . a,d = (omf F) . b,c )
proof end;

theorem :: REALSET3:38
for F being Field
for a being Element of NonZero F holds (ovf F) . (1. F),a = (revf F) . a
proof end;

theorem Th39: :: REALSET3:39
for F being Field
for a being Element of F holds (ovf F) . a,(1. F) = a
proof end;

theorem :: REALSET3:40
for F being Field
for a being Element of NonZero F
for b, c being Element of F holds
( (omf F) . a,b = c iff (ovf F) . c,a = b )
proof end;

theorem :: REALSET3:41
for F being Field
for a, c being Element of F
for b being Element of NonZero F holds
( (omf F) . a,b = c iff (ovf F) . c,b = a )
proof end;

theorem :: REALSET3:42
for F being Field
for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . a,((ovf F) . b,c) = (omf F) . ((ovf F) . a,b),c
proof end;

theorem :: REALSET3:43
for F being Field
for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . a,((omf F) . b,c) = (ovf F) . ((ovf F) . a,b),c
proof end;