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

:: Properties of fields
theorem Th1: :: REALSET3:1
for F being Field holds (revf F) . (1. F) = 1. F
proof end;

theorem Th2: :: REALSET3:2
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 Th3: :: REALSET3:3
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 Th4: :: REALSET3:4
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 Th5: :: REALSET3:5
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:6
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:7
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:8
for F being Field
for x being Element of F holds (osf F) . (x,x) = 0. F
proof end;

theorem Th9: :: REALSET3:9
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:10
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:11
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:12
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 Th13: :: REALSET3:13
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:14
for F being Field
for a being Element of F holds (osf F) . ((0. F),a) = (comp F) . a
proof end;

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

theorem :: REALSET3:16
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:17
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:18
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:19
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,():], 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,():], 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,():], 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,():], 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 Th20: :: REALSET3:20
for F being Field
for x being Element of NonZero F holds (ovf F) . (x,x) = 1. F
proof end;

theorem Th21: :: REALSET3:21
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:22
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:23
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:24
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 Th25: :: REALSET3:25
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:26
for F being Field
for a being Element of NonZero F holds (ovf F) . ((1. F),a) = (revf F) . a
proof end;

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

theorem :: REALSET3:28
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:29
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:30
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:31
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;