:: Analytical Ordered Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 11, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines // ANALOAF:def 1 :
theorem :: ANALOAF:1
canceled;
theorem :: ANALOAF:2
canceled;
theorem :: ANALOAF:3
canceled;
theorem Th4: :: ANALOAF:4
theorem :: ANALOAF:5
canceled;
theorem :: ANALOAF:6
canceled;
theorem :: ANALOAF:7
canceled;
theorem :: ANALOAF:8
canceled;
theorem Th9: :: ANALOAF:9
theorem Th10: :: ANALOAF:10
theorem Th11: :: ANALOAF:11
theorem Th12: :: ANALOAF:12
theorem Th13: :: ANALOAF:13
theorem :: ANALOAF:14
canceled;
theorem :: ANALOAF:15
canceled;
theorem Th16: :: ANALOAF:16
theorem Th17: :: ANALOAF:17
theorem :: ANALOAF:18
theorem Th19: :: ANALOAF:19
theorem Th20: :: ANALOAF:20
for
V being
RealLinearSpace for
p,
q,
u,
v,
w,
y being
VECTOR of
V st
p <> q &
p,
q // u,
v &
p,
q // w,
y holds
u,
v // w,
y
theorem Th21: :: ANALOAF:21
theorem Th22: :: ANALOAF:22
theorem Th23: :: ANALOAF:23
theorem Th24: :: ANALOAF:24
theorem Th25: :: ANALOAF:25
theorem Th26: :: ANALOAF:26
theorem Th27: :: ANALOAF:27
theorem Th28: :: ANALOAF:28
theorem Th29: :: ANALOAF:29
Lm1:
for V being RealLinearSpace
for v, u, w, y being VECTOR of V
for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
theorem :: ANALOAF:30
canceled;
theorem Th31: :: ANALOAF:31
for
V being
RealLinearSpace st ex
p,
q being
VECTOR of
V st
for
w being
VECTOR of
V ex
a,
b being
Real st
(a * p) + (b * q) = w holds
for
u,
v,
w,
y being
VECTOR of
V st not
u,
v // w,
y & not
u,
v // y,
w holds
ex
z being
VECTOR of
V st
( (
u,
v // u,
z or
u,
v // z,
u ) & (
w,
y // w,
z or
w,
y // z,
w ) )
:: deftheorem Def2 defines // ANALOAF:def 2 :
definition
let V be
RealLinearSpace;
func DirPar V -> Relation of
[:the carrier of V,the carrier of V:] means :
Def3:
:: ANALOAF:def 3
for
x,
z being
set holds
(
[x,z] in it iff ex
u,
v,
w,
y being
VECTOR of
V st
(
x = [u,v] &
z = [w,y] &
u,
v // w,
y ) );
existence
ex b1 being Relation of [:the carrier of V,the carrier of V:] st
for x, z being set holds
( [x,z] in b1 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )
uniqueness
for b1, b2 being Relation of [:the carrier of V,the carrier of V:] st ( for x, z being set holds
( [x,z] in b1 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines DirPar ANALOAF:def 3 :
for
V being
RealLinearSpace for
b2 being
Relation of
[:the carrier of V,the carrier of V:] holds
(
b2 = DirPar V iff for
x,
z being
set holds
(
[x,z] in b2 iff ex
u,
v,
w,
y being
VECTOR of
V st
(
x = [u,v] &
z = [w,y] &
u,
v // w,
y ) ) );
theorem :: ANALOAF:32
canceled;
theorem Th33: :: ANALOAF:33
:: deftheorem defines OASpace ANALOAF:def 4 :
theorem :: ANALOAF:34
canceled;
theorem Th35: :: ANALOAF:35
for
V being
RealLinearSpace st ex
u,
v being
VECTOR of
V st
for
a,
b being
Real st
(a * u) + (b * v) = 0. V holds
(
a = 0 &
b = 0 ) holds
( ex
a,
b being
Element of
(OASpace V) st
a <> b & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
(OASpace V) holds
(
a,
b // c,
c & (
a,
b // b,
a implies
a = b ) & (
a <> b &
a,
b // p,
q &
a,
b // r,
s implies
p,
q // r,
s ) & (
a,
b // c,
d implies
b,
a // d,
c ) & (
a,
b // b,
c implies
a,
b // a,
c ) & ( not
a,
b // a,
c or
a,
b // b,
c or
a,
c // c,
b ) ) ) & ex
a,
b,
c,
d being
Element of
(OASpace V) st
( not
a,
b // c,
d & not
a,
b // d,
c ) & ( for
a,
b,
c being
Element of
(OASpace V) ex
d being
Element of
(OASpace V) st
(
a,
b // c,
d &
a,
c // b,
d &
b <> d ) ) & ( for
p,
a,
b,
c being
Element of
(OASpace V) st
p <> b &
b,
p // p,
c holds
ex
d being
Element of
(OASpace V) st
(
a,
p // p,
d &
a,
b // c,
d ) ) )
theorem Th36: :: ANALOAF:36
for
V being
RealLinearSpace st ex
p,
q being
VECTOR of
V st
for
w being
VECTOR of
V ex
a,
b being
Real st
(a * p) + (b * q) = w holds
for
a,
b,
c,
d being
Element of
(OASpace V) st not
a,
b // c,
d & not
a,
b // d,
c holds
ex
t being
Element of
(OASpace V) st
( (
a,
b // a,
t or
a,
b // t,
a ) & (
c,
d // c,
t or
c,
d // t,
c ) )
definition
let IT be non
empty AffinStruct ;
attr IT is
OAffinSpace-like means :
Def5:
:: ANALOAF:def 5
( ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
IT holds
(
a,
b // c,
c & (
a,
b // b,
a implies
a = b ) & (
a <> b &
a,
b // p,
q &
a,
b // r,
s implies
p,
q // r,
s ) & (
a,
b // c,
d implies
b,
a // d,
c ) & (
a,
b // b,
c implies
a,
b // a,
c ) & ( not
a,
b // a,
c or
a,
b // b,
c or
a,
c // c,
b ) ) ) & ex
a,
b,
c,
d being
Element of
IT st
( not
a,
b // c,
d & not
a,
b // d,
c ) & ( for
a,
b,
c being
Element of
IT ex
d being
Element of
IT st
(
a,
b // c,
d &
a,
c // b,
d &
b <> d ) ) & ( for
p,
a,
b,
c being
Element of
IT st
p <> b &
b,
p // p,
c holds
ex
d being
Element of
IT st
(
a,
p // p,
d &
a,
b // c,
d ) ) );
end;
:: deftheorem Def5 defines OAffinSpace-like ANALOAF:def 5 :
for
IT being non
empty AffinStruct holds
(
IT is
OAffinSpace-like iff ( ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
IT holds
(
a,
b // c,
c & (
a,
b // b,
a implies
a = b ) & (
a <> b &
a,
b // p,
q &
a,
b // r,
s implies
p,
q // r,
s ) & (
a,
b // c,
d implies
b,
a // d,
c ) & (
a,
b // b,
c implies
a,
b // a,
c ) & ( not
a,
b // a,
c or
a,
b // b,
c or
a,
c // c,
b ) ) ) & ex
a,
b,
c,
d being
Element of
IT st
( not
a,
b // c,
d & not
a,
b // d,
c ) & ( for
a,
b,
c being
Element of
IT ex
d being
Element of
IT st
(
a,
b // c,
d &
a,
c // b,
d &
b <> d ) ) & ( for
p,
a,
b,
c being
Element of
IT st
p <> b &
b,
p // p,
c holds
ex
d being
Element of
IT st
(
a,
p // p,
d &
a,
b // c,
d ) ) ) );
theorem :: ANALOAF:37
for
AS being non
empty AffinStruct holds
( ( ex
a,
b being
Element of
AS st
a <> b & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
AS holds
(
a,
b // c,
c & (
a,
b // b,
a implies
a = b ) & (
a <> b &
a,
b // p,
q &
a,
b // r,
s implies
p,
q // r,
s ) & (
a,
b // c,
d implies
b,
a // d,
c ) & (
a,
b // b,
c implies
a,
b // a,
c ) & ( not
a,
b // a,
c or
a,
b // b,
c or
a,
c // c,
b ) ) ) & ex
a,
b,
c,
d being
Element of
AS st
( not
a,
b // c,
d & not
a,
b // d,
c ) & ( for
a,
b,
c being
Element of
AS ex
d being
Element of
AS st
(
a,
b // c,
d &
a,
c // b,
d &
b <> d ) ) & ( for
p,
a,
b,
c being
Element of
AS st
p <> b &
b,
p // p,
c holds
ex
d being
Element of
AS st
(
a,
p // p,
d &
a,
b // c,
d ) ) ) iff
AS is
OAffinSpace )
by Def5, STRUCT_0:def 10;
theorem Th38: :: ANALOAF:38
definition
let IT be
OAffinSpace;
attr IT is
2-dimensional means :
Def6:
:: ANALOAF:def 6
for
a,
b,
c,
d being
Element of
IT st not
a,
b // c,
d & not
a,
b // d,
c holds
ex
p being
Element of
IT st
( (
a,
b // a,
p or
a,
b // p,
a ) & (
c,
d // c,
p or
c,
d // p,
c ) );
end;
:: deftheorem Def6 defines 2-dimensional ANALOAF:def 6 :
for
IT being
OAffinSpace holds
(
IT is
2-dimensional iff for
a,
b,
c,
d being
Element of
IT st not
a,
b // c,
d & not
a,
b // d,
c holds
ex
p being
Element of
IT st
( (
a,
b // a,
p or
a,
b // p,
a ) & (
c,
d // c,
p or
c,
d // p,
c ) ) );
theorem :: ANALOAF:39
canceled;
theorem :: ANALOAF:40
canceled;
theorem :: ANALOAF:41
canceled;
theorem :: ANALOAF:42
canceled;
theorem :: ANALOAF:43
canceled;
theorem :: ANALOAF:44
canceled;
theorem :: ANALOAF:45
canceled;
theorem :: ANALOAF:46
canceled;
theorem :: ANALOAF:47
canceled;
theorem :: ANALOAF:48
canceled;
theorem :: ANALOAF:49
canceled;
theorem :: ANALOAF:50
for
AS being non
empty AffinStruct holds
( ( ex
a,
b being
Element of
AS st
a <> b & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
AS holds
(
a,
b // c,
c & (
a,
b // b,
a implies
a = b ) & (
a <> b &
a,
b // p,
q &
a,
b // r,
s implies
p,
q // r,
s ) & (
a,
b // c,
d implies
b,
a // d,
c ) & (
a,
b // b,
c implies
a,
b // a,
c ) & ( not
a,
b // a,
c or
a,
b // b,
c or
a,
c // c,
b ) ) ) & ex
a,
b,
c,
d being
Element of
AS st
( not
a,
b // c,
d & not
a,
b // d,
c ) & ( for
a,
b,
c being
Element of
AS ex
d being
Element of
AS st
(
a,
b // c,
d &
a,
c // b,
d &
b <> d ) ) & ( for
p,
a,
b,
c being
Element of
AS st
p <> b &
b,
p // p,
c holds
ex
d being
Element of
AS st
(
a,
p // p,
d &
a,
b // c,
d ) ) & ( for
a,
b,
c,
d being
Element of
AS st not
a,
b // c,
d & not
a,
b // d,
c holds
ex
p being
Element of
AS st
( (
a,
b // a,
p or
a,
b // p,
a ) & (
c,
d // c,
p or
c,
d // p,
c ) ) ) ) iff
AS is
OAffinPlane )
by Def5, Def6, STRUCT_0:def 10;
theorem :: ANALOAF:51