:: REALSET3 semantic presentation

theorem Th1: :: REALSET3:1

for F being Field holds (compf F) . (ndf F) = ndf F

proof end;

theorem Th2: :: REALSET3:2

for F being Field holds (revf F) . (nmf F) = nmf F

proof end;

theorem Th3: :: REALSET3:3

for F being Field
for a, b being Element of suppf F holds (compf F) . ((odf F) . [a,((compf F) . b)]) = (odf F) . [b,((compf F) . a)]

proof end;

theorem Th4: :: REALSET3:4

for F being Field
for a, b being Element of (suppf F) \ {(ndf F)} holds (revf F) . ((omf F) . [a,((revf F) . b)]) = (omf F) . [b,((revf F) . a)]

proof end;

theorem Th5: :: REALSET3:5

for F being Field
for a, b being Element of suppf F holds (compf F) . ((odf F) . [a,b]) = (odf F) . ((compf F) . a),((compf F) . b)

proof end;

theorem Th6: :: REALSET3:6

for F being Field
for a, b being Element of (suppf F) \ {(ndf 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 suppf F holds
( (odf F) . a,((compf F) . b) = (odf F) . [c,((compf F) . d)] iff (odf F) . [a,d] = (odf F) . [b,c] )

proof end;

theorem Th8: :: REALSET3:8

for F being Field
for a, c being Element of suppf F
for b, d being Element of (suppf F) \ {(ndf 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

for F being Field
for a, b being Element of suppf F holds
( (omf F) . [a,b] = ndf F iff ( a = ndf F or b = ndf F ) )

proof end;

theorem :: REALSET3:10

for F being Field
for a, b being Element of suppf F
for c, d being Element of (suppf F) \ {(ndf 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 suppf F
for c, d being Element of (suppf F) \ {(ndf F)} holds (odf F) . [((omf F) . [a,((revf F) . c)]),((omf F) . [b,((revf F) . d)])] = (omf F) . [((odf 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 suppf F means :Def1: :: REALSET3:def 1
for x, y being Element of suppf F holds it . [x,y] = (odf F) . [x,((compf F) . y)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines osf REALSET3:def 1 :

theorem :: REALSET3:12

canceled;

theorem :: REALSET3:13

canceled;

theorem :: REALSET3:14

for F being Field
for x being Element of suppf F holds (osf F) . [x,x] = ndf F

proof end;

theorem Th15: :: REALSET3:15

for F being Field
for a, b, c being Element of suppf F holds (omf F) . [a,((osf F) . [b,c])] = (osf F) . [((omf F) . [a,b]),((omf F) . [a,c])]

proof end;

theorem Th16: :: REALSET3:16

for F being Field
for a, b being Element of suppf F holds (osf F) . [a,b] is Element of suppf F

proof end;

theorem :: REALSET3:17

for F being Field
for a, b, c being Element of suppf 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 suppf F holds (osf F) . [a,b] = (compf F) . ((osf F) . [b,a])

proof end;

theorem :: REALSET3:19

for F being Field
for a, b being Element of suppf F holds (osf F) . [((compf F) . a),b] = (compf F) . ((odf F) . a,b)

proof end;

theorem Th20: :: REALSET3:20

for F being Field
for a, b, c, d being Element of suppf F holds
( (osf F) . [a,b] = (osf F) . [c,d] iff (odf F) . [a,d] = (odf F) . [b,c] )

proof end;

theorem :: REALSET3:21

for F being Field
for a being Element of suppf F holds (osf F) . [(ndf F),a] = (compf F) . a

proof end;

theorem Th22: :: REALSET3:22

for F being Field
for a being Element of suppf F holds (osf F) . [a,(ndf F)] = a

proof end;

theorem :: REALSET3:23

for F being Field
for a, b, c being Element of suppf F holds
( (odf F) . [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 suppf F holds
( (odf F) . [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 suppf F holds (osf F) . [a,((osf F) . [b,c])] = (odf F) . [((osf F) . [a,b]),c]

proof end;

theorem :: REALSET3:26

for F being Field
for a, b, c being Element of suppf F holds (osf F) . [a,((odf F) . [b,c])] = (osf F) . [((osf F) . [a,b]),c]

proof end;

definition

let F be Field;
func ovf F -> Function of [:(suppf F),((suppf F) \ {(ndf F)}):], suppf F means :Def2: :: REALSET3:def 2
for x being Element of suppf F
for y being Element of (suppf F) \ {(ndf F)} holds it . [x,y] = (omf F) . [x,((revf F) . y)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ovf REALSET3:def 2 :

theorem :: REALSET3:27

canceled;

theorem :: REALSET3:28

canceled;

theorem Th29: :: REALSET3:29

for F being Field
for x being Element of (suppf F) \ {(ndf F)} holds (ovf F) . [x,x] = nmf F

proof end;

theorem Th30: :: REALSET3:30

for F being Field
for a being Element of suppf F
for b being Element of (suppf F) \ {(ndf F)} holds (ovf F) . [a,b] is Element of suppf F

proof end;

theorem Th31: :: REALSET3:31

for F being Field
for a, b being Element of suppf F
for c being Element of (suppf F) \ {(ndf 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 (suppf F) \ {(ndf F)} holds
( (omf F) . [a,((ovf F) . [(nmf F),a])] = nmf F & (omf F) . [((ovf F) . [(nmf F),a]),a] = nmf F )

proof end;

theorem :: REALSET3:33

canceled;

theorem :: REALSET3:34

canceled;

theorem :: REALSET3:35

for F being Field
for a, b being Element of (suppf F) \ {(ndf 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 (suppf F) \ {(ndf 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 suppf F
for b, d being Element of (suppf F) \ {(ndf 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 (suppf F) \ {(ndf F)} holds (ovf F) . [(nmf F),a] = (revf F) . a

proof end;

theorem Th39: :: REALSET3:39

for F being Field
for a being Element of suppf F holds (ovf F) . [a,(nmf F)] = a

proof end;

theorem :: REALSET3:40

for F being Field
for a being Element of (suppf F) \ {(ndf F)}
for b, c being Element of suppf 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 suppf F
for b being Element of (suppf F) \ {(ndf 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 suppf F
for b, c being Element of (suppf F) \ {(ndf 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 suppf F
for b, c being Element of (suppf F) \ {(ndf F)} holds (ovf F) . [a,((omf F) . [b,c])] = (ovf F) . [((ovf F) . [a,b]),c]

proof end;