begin
:: deftheorem Def1 defines // ANALOAF:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
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:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
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
canceled;
theorem Th31:
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:
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
canceled;
theorem Th33:
:: deftheorem defines OASpace ANALOAF:def 4 :
theorem
canceled;
theorem Th35:
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:
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;
theorem Th38:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
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;
theorem