:: by J\'ozef Bia{\l}as

::

:: Received September 27, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

:: Properties of fields

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))

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))

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 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) )

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))))

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))))

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;

ex b_{1} being BinOp of the carrier of F st

for x, y being Element of F holds b_{1} . (x,y) = the addF of F . (x,((comp F) . y))

for b_{1}, b_{2} being BinOp of the carrier of F st ( for x, y being Element of F holds b_{1} . (x,y) = the addF of F . (x,((comp F) . y)) ) & ( for x, y being Element of F holds b_{2} . (x,y) = the addF of F . (x,((comp F) . y)) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of F holds it . (x,y) = the addF of F . (x,((comp F) . y));

ex b

for x, y being Element of F holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines osf REALSET3:def 1 :

for F being Field

for b_{2} being BinOp of the carrier of F holds

( b_{2} = osf F iff for x, y being Element of F holds b_{2} . (x,y) = the addF of F . (x,((comp F) . y)) );

for F being Field

for b

( b

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)))

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)))

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: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))

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 )

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: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)

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)

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;

ex b_{1} 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_{1} . (x,y) = (omf F) . (x,((revf F) . y))

for b_{1}, b_{2} 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_{1} . (x,y) = (omf F) . (x,((revf F) . y)) ) & ( for x being Element of F

for y being Element of NonZero F holds b_{2} . (x,y) = (omf F) . (x,((revf F) . y)) ) holds

b_{1} = b_{2}

end;
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 for x being Element of F

for y being Element of NonZero F holds it . (x,y) = (omf F) . (x,((revf F) . y));

ex b

for x being Element of F

for y being Element of NonZero F holds b

proof end;

uniqueness for b

for y being Element of NonZero F holds b

for y being Element of NonZero F holds b

b

proof end;

:: deftheorem Def2 defines ovf REALSET3:def 2 :

for F being Field

for b_{2} being Function of [: the carrier of F,(NonZero F):], the carrier of F holds

( b_{2} = ovf F iff for x being Element of F

for y being Element of NonZero F holds b_{2} . (x,y) = (omf F) . (x,((revf F) . y)) );

for F being Field

for b

( b

for y being Element of NonZero F holds b

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)

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 )

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))

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))

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) )

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: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 )

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 )

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)

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)

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;