:: MIDSP_1 semantic presentation

definition

attr c₁ is strict;
struct MidStr -> 1-sorted ;
aggr MidStr(# carrier, MIDPOINT #) -> MidStr ;
sel MIDPOINT c₁ -> BinOp of the carrier of c₁;

end;

registration

cluster non empty MidStr ;
existence

proof end;

end;

definition

let MS be non empty MidStr ;
let a, b be Element of MS;
func a @ b -> Element of MS equals :: MIDSP_1:def 1
the MIDPOINT of MS . a,b;
coherence ;

end;

:: deftheorem defines @ MIDSP_1:def 1 :

definition

func op2 -> BinOp of {{} } means :: MIDSP_1:def 2
verum;
existence ;
uniqueness by FUNCT_2:66;

end;

:: deftheorem defines op2 MIDSP_1:def 2 :

definition

func Example -> MidStr equals :: MIDSP_1:def 3
MidStr(# {{} },op2 #);
correctness ;

end;

:: deftheorem defines Example MIDSP_1:def 3 :

registration

cluster Example -> non empty strict ;
coherence

proof end;

end;

theorem :: MIDSP_1:1

canceled;

theorem :: MIDSP_1:2

canceled;

theorem :: MIDSP_1:3

canceled;

theorem :: MIDSP_1:4

canceled;

theorem :: MIDSP_1:5

the carrier of Example = {{} } ;

theorem :: MIDSP_1:6

the MIDPOINT of Example = op2 ;

theorem :: MIDSP_1:7

for a being Element of Example holds a = {} by TARSKI:def 1;

theorem :: MIDSP_1:8

for a, b being Element of Example holds a @ b = op2 . a,b ;

theorem :: MIDSP_1:9

canceled;

theorem Th10: :: MIDSP_1:10

for a, b, c, d being Element of Example holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

proof end;

definition

let IT be non empty MidStr ;
attr IT is MidSp-like means :Def4: :: MIDSP_1:def 4
for a, b, c, d being Element of IT holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of IT st x @ a = b );

end;

:: deftheorem Def4 defines MidSp-like MIDSP_1:def 4 :

registration

cluster non empty strict MidSp-like MidStr ;
existence

proof end;

end;

definition

mode MidSp is non empty MidSp-like MidStr ;

end;

definition

let M be MidSp;
let a, b be Element of M;
:: original: @
redefine func a @ b -> Element of M;
commutativity by Def4;

end;

theorem :: MIDSP_1:11

canceled;

theorem :: MIDSP_1:12

canceled;

theorem :: MIDSP_1:13

canceled;

theorem :: MIDSP_1:14

canceled;

theorem Th15: :: MIDSP_1:15

for M being MidSp
for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)

proof end;

theorem Th16: :: MIDSP_1:16

for M being MidSp
for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)

proof end;

theorem Th17: :: MIDSP_1:17

for M being MidSp
for a, b being Element of M st a @ b = a holds
a = b

proof end;

theorem Th18: :: MIDSP_1:18

for M being MidSp
for x, a, x' being Element of M st x @ a = x' @ a holds
x = x'

proof end;

theorem :: MIDSP_1:19

for M being MidSp
for a, x, x' being Element of M st a @ x = a @ x' holds
x = x' by Th18;

definition

let M be MidSp;
let a, b, c, d be Element of M;
pred a,b @@ c,d means :Def5: :: MIDSP_1:def 5
a @ d = b @ c;

end;

:: deftheorem Def5 defines @@ MIDSP_1:def 5 :

theorem :: MIDSP_1:20

canceled;

theorem Th21: :: MIDSP_1:21

for M being MidSp
for a, b being Element of M holds a,a @@ b,b

proof end;

theorem Th22: :: MIDSP_1:22

for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b

proof end;

theorem Th23: :: MIDSP_1:23

for M being MidSp
for a, b, c being Element of M st a,a @@ b,c holds
b = c

proof end;

theorem Th24: :: MIDSP_1:24

for M being MidSp
for a, b, c being Element of M st a,b @@ c,c holds
a = b

proof end;

theorem Th25: :: MIDSP_1:25

for M being MidSp
for a, b being Element of M holds a,b @@ a,b

proof end;

theorem Th26: :: MIDSP_1:26

for M being MidSp
for a, b, c being Element of M ex d being Element of M st a,b @@ c,d

proof end;

theorem Th27: :: MIDSP_1:27

for M being MidSp
for a, b, c, d, d' being Element of M st a,b @@ c,d & a,b @@ c,d' holds
d = d'

proof end;

theorem Th28: :: MIDSP_1:28

for M being MidSp
for x, y, a, b, c, d being Element of M st x,y @@ a,b & x,y @@ c,d holds
a,b @@ c,d

proof end;

theorem Th29: :: MIDSP_1:29

for M being MidSp
for a, b, a', b', c, c' being Element of M st a,b @@ a',b' & b,c @@ b',c' holds
a,c @@ a',c'

proof end;

definition

let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
:: original: `1
redefine func p `1 -> Element of M;
coherence by MCART_1:10;

end;

definition

let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
:: original: `2
redefine func p `2 -> Element of M;
coherence by MCART_1:10;

end;

definition

let M be MidSp;
let p, q be Element of [:the carrier of M,the carrier of M:];
pred p ## q means :Def6: :: MIDSP_1:def 6
p `1 ,p `2 @@ q `1 ,q `2 ;
reflexivity by Th25;
symmetry by Th22;

end;

:: deftheorem Def6 defines ## MIDSP_1:def 6 :

definition

let M be MidSp;
let a, b be Element of M;
:: original: [
redefine func [a,b] -> Element of [:the carrier of M,the carrier of M:];
coherence by ZFMISC_1:def 2;

end;

theorem :: MIDSP_1:30

canceled;

theorem Th31: :: MIDSP_1:31

for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
[a,b] ## [c,d]

proof end;

theorem Th32: :: MIDSP_1:32

for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d

proof end;

theorem :: MIDSP_1:33

canceled;

theorem :: MIDSP_1:34

canceled;

theorem Th35: :: MIDSP_1:35

for M being MidSp
for p, q, r being Element of [:the carrier of M,the carrier of M:] st p ## q & p ## r holds
q ## r

proof end;

theorem :: MIDSP_1:36

for M being MidSp
for p, r, q being Element of [:the carrier of M,the carrier of M:] st p ## r & q ## r holds
p ## q by Th35;

theorem :: MIDSP_1:37

for M being MidSp
for p, q, r being Element of [:the carrier of M,the carrier of M:] st p ## q & q ## r holds
p ## r by Th35;

theorem :: MIDSP_1:38

for M being MidSp
for p, q, r being Element of [:the carrier of M,the carrier of M:] st p ## q holds
( r ## p iff r ## q ) by Th35;

theorem Th39: :: MIDSP_1:39

for M being MidSp
for p being Element of [:the carrier of M,the carrier of M:] holds { q where q is Element of [:the carrier of M,the carrier of M:] : q ## p } is non empty Subset of [:the carrier of M,the carrier of M:]

proof end;

definition

let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
func p ~ -> Subset of [:the carrier of M,the carrier of M:] equals :: MIDSP_1:def 7
{ q where q is Element of [:the carrier of M,the carrier of M:] : q ## p } ;
coherence by Th39;

end;

:: deftheorem defines ~ MIDSP_1:def 7 :

registration

let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
cluster p ~ -> non empty ;
coherence by Th39;

end;

theorem :: MIDSP_1:40

canceled;

theorem Th41: :: MIDSP_1:41

for M being MidSp
for r, p being Element of [:the carrier of M,the carrier of M:] holds
( r in p ~ iff r ## p )

proof end;

theorem Th42: :: MIDSP_1:42

for M being MidSp
for p, q being Element of [:the carrier of M,the carrier of M:] st p ## q holds
p ~ = q ~

proof end;

theorem Th43: :: MIDSP_1:43

for M being MidSp
for p, q being Element of [:the carrier of M,the carrier of M:] st p ~ = q ~ holds
p ## q

proof end;

theorem Th44: :: MIDSP_1:44

for M being MidSp
for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c

proof end;

theorem :: MIDSP_1:45

for M being MidSp
for p being Element of [:the carrier of M,the carrier of M:] holds p in p ~ ;

definition

let M be MidSp;
mode Vector of M -> non empty Subset of [:the carrier of M,the carrier of M:] means :Def8: :: MIDSP_1:def 8
ex p being Element of [:the carrier of M,the carrier of M:] st it = p ~ ;
existence

proof end;

end;

:: deftheorem Def8 defines Vector MIDSP_1:def 8 :

definition

let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
:: original: ~
redefine func p ~ -> Vector of M;
coherence by Def8;

end;

theorem :: MIDSP_1:46

canceled;

theorem :: MIDSP_1:47

canceled;

theorem Th48: :: MIDSP_1:48

for M being MidSp ex u being Vector of M st
for p being Element of [:the carrier of M,the carrier of M:] holds
( p in u iff p `1 = p `2 )

proof end;

definition

let M be MidSp;
func ID M -> Vector of M equals :: MIDSP_1:def 9
{ p where p is Element of [:the carrier of M,the carrier of M:] : p `1 = p `2 } ;
coherence

proof end;

end;

:: deftheorem defines ID MIDSP_1:def 9 :

theorem :: MIDSP_1:49

canceled;

theorem Th50: :: MIDSP_1:50

for M being MidSp
for b being Element of M holds ID M = [b,b] ~

proof end;

theorem Th51: :: MIDSP_1:51

for M being MidSp
for u, v being Vector of M ex w being Vector of M ex p, q being Element of [:the carrier of M,the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1 ),(q `2 )] ~ )

proof end;

theorem Th52: :: MIDSP_1:52

for M being MidSp
for u, v, w, w' being Vector of M st ex p, q being Element of [:the carrier of M,the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1 ),(q `2 )] ~ ) & ex p, q being Element of [:the carrier of M,the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w' = [(p `1 ),(q `2 )] ~ ) holds
w = w'

proof end;

definition

let M be MidSp;
let u, v be Vector of M;
func u + v -> Vector of M means :Def10: :: MIDSP_1:def 10
ex p, q being Element of [:the carrier of M,the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & it = [(p `1 ),(q `2 )] ~ );
existence by Th51;
uniqueness by Th52;

end;

:: deftheorem Def10 defines + MIDSP_1:def 10 :

theorem Th53: :: MIDSP_1:53

for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = [a,b] ~

proof end;

definition

let M be MidSp;
let a, b be Element of M;
func vect a,b -> Vector of M equals :: MIDSP_1:def 11
[a,b] ~ ;
coherence ;

end;

:: deftheorem defines vect MIDSP_1:def 11 :

theorem :: MIDSP_1:54

canceled;

theorem Th55: :: MIDSP_1:55

for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = vect a,b

proof end;

theorem Th56: :: MIDSP_1:56

for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
vect a,b = vect c,d by Th42;

theorem Th57: :: MIDSP_1:57

for M being MidSp
for a, b, c, d being Element of M st vect a,b = vect c,d holds
a @ d = b @ c by Th44;

theorem Th58: :: MIDSP_1:58

for M being MidSp
for b being Element of M holds ID M = vect b,b by Th50;

theorem :: MIDSP_1:59

for M being MidSp
for a, b, c being Element of M st vect a,b = vect a,c holds
b = c

proof end;

theorem Th60: :: MIDSP_1:60

for M being MidSp
for a, b, c being Element of M holds (vect a,b) + (vect b,c) = vect a,c

proof end;

theorem Th61: :: MIDSP_1:61

for M being MidSp
for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]

proof end;

theorem :: MIDSP_1:62

for M being MidSp
for a, b being Element of M holds (vect a,(a @ b)) + (vect a,(a @ b)) = vect a,b

proof end;

theorem Th63: :: MIDSP_1:63

for M being MidSp
for u, v, w being Vector of M holds (u + v) + w = u + (v + w)

proof end;

theorem Th64: :: MIDSP_1:64

for M being MidSp
for u being Vector of M holds u + (ID M) = u

proof end;

theorem Th65: :: MIDSP_1:65

for M being MidSp
for u being Vector of M ex v being Vector of M st u + v = ID M

proof end;

theorem Th66: :: MIDSP_1:66

for M being MidSp
for u, v being Vector of M holds u + v = v + u

proof end;

theorem Th67: :: MIDSP_1:67

for M being MidSp
for u, v, w being Vector of M st u + v = u + w holds
v = w

proof end;

definition

let M be MidSp;
let u be Vector of M;
func - u -> Vector of M means :: MIDSP_1:def 12
u + it = ID M;
existence by Th65;
uniqueness by Th67;

end;

:: deftheorem defines - MIDSP_1:def 12 :

definition

let M be MidSp;
func setvect M -> set equals :: MIDSP_1:def 13
{ X where X is Subset of [:the carrier of M,the carrier of M:] : X is Vector of M } ;
coherence ;

end;

:: deftheorem defines setvect MIDSP_1:def 13 :

theorem :: MIDSP_1:68

canceled;

theorem :: MIDSP_1:69

canceled;

theorem :: MIDSP_1:70

canceled;

theorem Th71: :: MIDSP_1:71

for M being MidSp
for x being set holds
( x is Vector of M iff x in setvect M )

proof end;

registration

let M be MidSp;
cluster setvect M -> non empty ;
coherence

proof end;

end;

definition

let M be MidSp;
let u1, v1 be Element of setvect M;
func u1 + v1 -> Element of setvect M means :Def14: :: MIDSP_1:def 14
for u, v being Vector of M st u1 = u & v1 = v holds
it = u + v;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines + MIDSP_1:def 14 :

theorem :: MIDSP_1:72

canceled;

theorem :: MIDSP_1:73

canceled;

theorem Th74: :: MIDSP_1:74

for M being MidSp
for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1

proof end;

theorem Th75: :: MIDSP_1:75

for M being MidSp
for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)

proof end;

definition

let M be MidSp;
func addvect M -> BinOp of setvect M means :Def15: :: MIDSP_1:def 15
for u1, v1 being Element of setvect M holds it . u1,v1 = u1 + v1;
existence

proof end;