begin
theorem Th11:
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
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 Th21:
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 ) )
definition
let V be
RealLinearSpace;
func DirPar V -> Relation of
[: the carrier of V, the carrier of V:] means :
Def3:
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 Th23:
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 Th24:
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:
( ( 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
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;
definition
let IT be
OAffinSpace;
attr IT is
2-dimensional means :
Def6:
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
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;