:: Several Properties of Fields. Field Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: 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 b₁ being BinOp of the carrier of F st
for x, y being Element of F holds b₁ . (x,y) = the addF of F . (x,((comp F) . y))

proof end;

uniqueness
for b₁, b₂ being BinOp of the carrier of F st ( for x, y being Element of F holds b₁ . (x,y) = the addF of F . (x,((comp F) . y)) ) & ( for x, y being Element of F holds b₂ . (x,y) = the addF of F . (x,((comp F) . y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines osf REALSET3:def 1 :
for F being Field
for b₂ being BinOp of the carrier of F holds
( b₂ = osf F iff for x, y being Element of F holds b₂ . (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,(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 b₁ 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 b₁ . (x,y) = (omf F) . (x,((revf F) . y))

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (x,y) = (omf F) . (x,((revf F) . y)) ) & ( for x being Element of F
for y being Element of NonZero F holds b₂ . (x,y) = (omf F) . (x,((revf F) . y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ovf REALSET3:def 2 :
for F being Field
for b₂ being Function of [: the carrier of F,(NonZero F):], the carrier of F holds
( b₂ = ovf F iff for x being Element of F
for y being Element of NonZero F holds b₂ . (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;