:: Midpoint algebras
:: by Micha{\l} Muzalewski
::
:: Received November 26, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines @ MIDSP_1:def 1 :
:: deftheorem MIDSP_1:def 2 :
canceled;
:: deftheorem defines Example MIDSP_1:def 3 :
theorem :: MIDSP_1:1
canceled;
theorem :: MIDSP_1:2
canceled;
theorem :: MIDSP_1:3
canceled;
theorem :: MIDSP_1:4
canceled;
theorem :: MIDSP_1:5
theorem :: MIDSP_1:6
theorem :: MIDSP_1:7
canceled;
theorem :: MIDSP_1:8
theorem :: MIDSP_1:9
canceled;
theorem Th10: :: MIDSP_1:10
:: deftheorem Def4 defines MidSp-like MIDSP_1:def 4 :
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
theorem Th16: :: MIDSP_1:16
theorem Th17: :: MIDSP_1:17
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'
theorem :: MIDSP_1:19
:: deftheorem Def5 defines @@ MIDSP_1:def 5 :
for
M being
MidSp for
a,
b,
c,
d being
Element of
M holds
(
a,
b @@ c,
d iff
a @ d = b @ c );
theorem :: MIDSP_1:20
canceled;
theorem Th21: :: MIDSP_1:21
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
theorem Th23: :: MIDSP_1:23
theorem Th24: :: MIDSP_1:24
theorem Th25: :: MIDSP_1:25
theorem Th26: :: MIDSP_1:26
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'
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
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'
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
for p being Element of [:the carrier of M,the carrier of M:] holds p `1 ,p `2 @@ p `1 ,p `2
by Th25;
symmetry
for p, q being Element of [:the carrier of M,the carrier of M:] st p `1 ,p `2 @@ q `1 ,q `2 holds
q `1 ,q `2 @@ p `1 ,p `2
by Th22;
end;
:: deftheorem Def6 defines ## MIDSP_1:def 6 :
theorem :: MIDSP_1:30
canceled;
theorem Th31: :: MIDSP_1:31
theorem Th32: :: MIDSP_1:32
theorem :: MIDSP_1:33
canceled;
theorem :: MIDSP_1:34
canceled;
theorem Th35: :: MIDSP_1:35
theorem :: MIDSP_1:36
theorem :: MIDSP_1:37
theorem :: MIDSP_1:38
theorem Th39: :: MIDSP_1:39
:: deftheorem defines ~ MIDSP_1:def 7 :
theorem :: MIDSP_1:40
canceled;
theorem Th41: :: MIDSP_1:41
theorem Th42: :: MIDSP_1:42
theorem Th43: :: MIDSP_1:43
theorem Th44: :: MIDSP_1:44
theorem :: MIDSP_1:45
:: deftheorem Def8 defines Vector MIDSP_1:def 8 :
theorem :: MIDSP_1:46
canceled;
theorem :: MIDSP_1:47
canceled;
theorem Th48: :: MIDSP_1:48
:: deftheorem defines ID MIDSP_1:def 9 :
theorem :: MIDSP_1:49
canceled;
theorem Th50: :: MIDSP_1:50
theorem Th51: :: MIDSP_1:51
theorem Th52: :: MIDSP_1:52
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
ex b1 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 & b1 = [(p `1 ),(q `2 )] ~ )
by Th51;
uniqueness
for b1, b2 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 & b1 = [(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 & b2 = [(p `1 ),(q `2 )] ~ ) holds
b1 = b2
by Th52;
end;
:: deftheorem Def10 defines + MIDSP_1:def 10 :
theorem Th53: :: MIDSP_1:53
:: deftheorem defines vect MIDSP_1:def 11 :
theorem :: MIDSP_1:54
canceled;
theorem Th55: :: MIDSP_1:55
theorem :: MIDSP_1:56
theorem :: MIDSP_1:57
theorem :: MIDSP_1:58
theorem :: MIDSP_1:59
theorem Th60: :: MIDSP_1:60
theorem Th61: :: MIDSP_1:61
theorem :: MIDSP_1:62
theorem Th63: :: MIDSP_1:63
theorem Th64: :: MIDSP_1:64
theorem Th65: :: MIDSP_1:65
theorem Th66: :: MIDSP_1:66
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
:: deftheorem defines - MIDSP_1:def 12 :
:: 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
:: deftheorem Def14 defines + MIDSP_1:def 14 :
theorem :: MIDSP_1:72
canceled;
theorem :: MIDSP_1:73
canceled;
theorem Th74: :: MIDSP_1:74
theorem Th75: :: MIDSP_1:75
:: deftheorem Def15 defines addvect MIDSP_1:def 15 :
theorem :: MIDSP_1:76
canceled;
theorem Th77: :: MIDSP_1:77
theorem Th78: :: MIDSP_1:78
:: deftheorem Def16 defines complvect MIDSP_1:def 16 :
:: deftheorem defines zerovect MIDSP_1:def 17 :
:: deftheorem defines vectgroup MIDSP_1:def 18 :
theorem :: MIDSP_1:79
canceled;
theorem :: MIDSP_1:80
canceled;
theorem :: MIDSP_1:81
canceled;
theorem :: MIDSP_1:82
theorem :: MIDSP_1:83
theorem :: MIDSP_1:84
canceled;
theorem :: MIDSP_1:85
theorem :: MIDSP_1:86