begin
Lm1:
for V being RealLinearSpace
for v1, w, y, v2 being VECTOR of
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
Lm2:
for V being RealLinearSpace
for w, y being VECTOR of holds (0 * w) + (0 * y) = 0. V
Lm3:
for V being RealLinearSpace
for v, w, y being VECTOR of
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
:: deftheorem Def1 defines Gen ANALMETR:def 1 :
:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def 2 :
Lm4:
for V being RealLinearSpace
for w, y being VECTOR of
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
Lm5:
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
( w <> 0. V & y <> 0. V )
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
for
V being
RealLinearSpace for
u,
v,
w,
y being
VECTOR of
for
a,
b being
Real st
u,
v are_Ort_wrt w,
y holds
(
a * u,
v are_Ort_wrt w,
y &
u,
b * v are_Ort_wrt w,
y )
theorem Th12:
theorem Th13:
for
V being
RealLinearSpace for
w,
y,
v,
u1,
u2 being
VECTOR of st
Gen w,
y &
v,
u1 are_Ort_wrt w,
y &
v,
u2 are_Ort_wrt w,
y &
v <> 0. V holds
ex
a,
b being
Real st
(
a * u1 = b * u2 & (
a <> 0 or
b <> 0 ) )
theorem Th14:
for
V being
RealLinearSpace for
w,
y,
u,
v1,
v2 being
VECTOR of st
Gen w,
y &
u,
v1 are_Ort_wrt w,
y &
u,
v2 are_Ort_wrt w,
y holds
(
u,
v1 + v2 are_Ort_wrt w,
y &
u,
v1 - v2 are_Ort_wrt w,
y )
theorem Th15:
theorem Th16:
for
V being
RealLinearSpace for
w,
y,
u,
u1,
u2 being
VECTOR of st
Gen w,
y &
u,
u1 - u2 are_Ort_wrt w,
y &
u1,
u2 - u are_Ort_wrt w,
y holds
u2,
u - u1 are_Ort_wrt w,
y
theorem Th17:
theorem Th18:
theorem Th19:
definition
let V be
RealLinearSpace;
let u,
u1,
v,
v1,
w,
y be
VECTOR of ;
pred u,
u1,
v,
v1 are_Ort_wrt w,
y means :
Def3:
u1 - u,
v1 - v are_Ort_wrt w,
y;
end;
:: deftheorem Def3 defines are_Ort_wrt ANALMETR:def 3 :
for
V being
RealLinearSpace for
u,
u1,
v,
v1,
w,
y being
VECTOR of holds
(
u,
u1,
v,
v1 are_Ort_wrt w,
y iff
u1 - u,
v1 - v are_Ort_wrt w,
y );
definition
let V be
RealLinearSpace;
let w,
y be
VECTOR of ;
func Orthogonality V,
w,
y -> Relation of
means :
Def4:
for
x,
z being
set holds
(
[x,z] in it iff ex
u,
u1,
v,
v1 being
VECTOR of st
(
x = [u,u1] &
z = [v,v1] &
u,
u1,
v,
v1 are_Ort_wrt w,
y ) );
existence
ex b1 being Relation of st
for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
uniqueness
for b1, b2 being Relation of st ( for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines Orthogonality ANALMETR:def 4 :
for
V being
RealLinearSpace for
w,
y being
VECTOR of
for
b4 being
Relation of holds
(
b4 = Orthogonality V,
w,
y iff for
x,
z being
set holds
(
[x,z] in b4 iff ex
u,
u1,
v,
v1 being
VECTOR of st
(
x = [u,u1] &
z = [v,v1] &
u,
u1,
v,
v1 are_Ort_wrt w,
y ) ) );
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
:: deftheorem ANALMETR:def 5 :
canceled;
:: deftheorem Def6 defines _|_ ANALMETR:def 6 :
definition
let V be
RealLinearSpace;
let w,
y be
VECTOR of ;
func AMSpace V,
w,
y -> strict ParOrtStr equals
ParOrtStr(# the
carrier of
V,
(lambda (DirPar V)),
(Orthogonality V,w,y) #);
correctness
coherence
ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality V,w,y) #) is strict ParOrtStr ;
;
end;
:: deftheorem defines AMSpace ANALMETR:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines Af ANALMETR:def 8 :
theorem
canceled;
theorem Th30:
theorem Th31:
for
V being
RealLinearSpace for
u,
u1,
v,
v1,
w,
y being
VECTOR of
for
p,
p1,
q,
q1 being
Element of st
p = u &
p1 = u1 &
q = v &
q1 = v1 holds
(
p,
q _|_ p1,
q1 iff
u,
v,
u1,
v1 are_Ort_wrt w,
y )
theorem Th32:
for
V being
RealLinearSpace for
w,
y,
u,
v,
u1,
v1 being
VECTOR of
for
p,
q,
p1,
q1 being
Element of st
p = u &
q = v &
p1 = u1 &
q1 = v1 holds
(
p,
q // p1,
q1 iff ex
a,
b being
Real st
(
a * (v - u) = b * (v1 - u1) & (
a <> 0 or
b <> 0 ) ) )
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
for
p,
p1,
q,
q1,
r,
r1 being
Element of st
p,
p1 _|_ q,
q1 &
p,
p1 // r,
r1 & not
p = p1 holds
q,
q1 _|_ r,
r1
theorem Th37:
theorem Th38:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
for
p,
p1,
q,
q1,
r,
r1 being
Element of st
Gen w,
y &
p,
p1 _|_ q,
q1 &
p,
p1 _|_ r,
r1 & not
p = p1 holds
q,
q1 // r,
r1
theorem Th39:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
for
p,
q,
r,
r1,
r2 being
Element of st
Gen w,
y &
p,
q _|_ r,
r1 &
p,
q _|_ r,
r2 holds
p,
q _|_ r1,
r2
theorem Th40:
theorem
for
V being
RealLinearSpace for
w,
y being
VECTOR of
for
p,
q,
p1,
p2 being
Element of st
Gen w,
y &
p,
q _|_ p1,
p2 &
p1,
q _|_ p2,
p holds
p2,
q _|_ p,
p1
theorem Th42:
consider V0 being RealLinearSpace such that
Lm6:
ex w, y being VECTOR of st Gen w,y
by Th7;
consider w0, y0 being VECTOR of such that
Lm7:
Gen w0,y0
by Lm6;
Lm8:
now
set X =
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #);
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #)
= Af (AMSpace V0,w0,y0)
;
then A1:
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #)
= Lambda (OASpace V0)
by Th30;
for
a,
b being
Real st
(a * w0) + (b * y0) = 0. V0 holds
(
a = 0 &
b = 0 )
by Def1, Lm7;
then
OASpace V0 is
OAffinSpace
by ANALOAF:38;
hence
(
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #) is
AffinSpace & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ p,
s implies
a,
b _|_ q,
s ) ) ) & ( for
a,
b,
c being
Element of st
a <> b holds
ex
x being
Element of st
(
a,
b // a,
x &
a,
b _|_ x,
c ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) )
by A1, Lm7, Th33, Th34, Th35, Th36, Th37, Th39, Th40, Th42, DIRAF:48;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfSp-like means :
Def9:
(
AffinStruct(# the
carrier of
IT,the
CONGR of
IT #) is
AffinSpace & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ p,
s implies
a,
b _|_ q,
s ) ) ) & ( for
a,
b,
c being
Element of st
a <> b holds
ex
x being
Element of st
(
a,
b // a,
x &
a,
b _|_ x,
c ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) );
end;
:: deftheorem Def9 defines OrtAfSp-like ANALMETR:def 9 :
for
IT being non
empty ParOrtStr holds
(
IT is
OrtAfSp-like iff (
AffinStruct(# the
carrier of
IT,the
CONGR of
IT #) is
AffinSpace & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ p,
s implies
a,
b _|_ q,
s ) ) ) & ( for
a,
b,
c being
Element of st
a <> b holds
ex
x being
Element of st
(
a,
b // a,
x &
a,
b _|_ x,
c ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) ) );
theorem
canceled;
theorem
consider V0 being RealLinearSpace such that
Lm9:
ex w, y being VECTOR of st Gen w,y
by Th7;
consider w0, y0 being VECTOR of such that
Lm10:
Gen w0,y0
by Lm9;
Lm11:
now
set X =
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #);
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #)
= Af (AMSpace V0,w0,y0)
;
then A1:
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #)
= Lambda (OASpace V0)
by Th30;
( ( for
a,
b being
Real st
(a * w0) + (b * y0) = 0. V0 holds
(
a = 0 &
b = 0 ) ) & ( for
w1 being
VECTOR of ex
a,
b being
Real st
w1 = (a * w0) + (b * y0) ) )
by Def1, Lm10;
then
OASpace V0 is
OAffinPlane
by ANALOAF:51;
hence
(
AffinStruct(# the
carrier of
(AMSpace V0,w0,y0),the
CONGR of
(AMSpace V0,w0,y0) #) is
AffinPlane & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b ) ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) )
by A1, Lm10, Th33, Th34, Th35, Th36, Th37, Th38, Th40, DIRAF:53;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfPl-like means :
Def10:
(
AffinStruct(# the
carrier of
IT,the
CONGR of
IT #) is
AffinPlane & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b ) ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) );
end;
:: deftheorem Def10 defines OrtAfPl-like ANALMETR:def 10 :
for
IT being non
empty ParOrtStr holds
(
IT is
OrtAfPl-like iff (
AffinStruct(# the
carrier of
IT,the
CONGR of
IT #) is
AffinPlane & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b ) ) ) & ( for
a,
b,
c being
Element of ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) ) ) );
theorem
canceled;
theorem
theorem
theorem Th48:
for
POS being non
empty ParOrtStr for
a,
b,
c,
d being
Element of
for
a',
b',
c',
d' being
Element of st
a = a' &
b = b' &
c = c' &
d = d' holds
(
a,
b // c,
d iff
a',
b' // c',
d' )
theorem Th49:
theorem
theorem
for
POS being non
empty ParOrtStr holds
(
POS is
OrtAfPl-like iff ( ex
a,
b being
Element of st
a <> b & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of holds
(
a,
b // b,
a &
a,
b // c,
c & (
a,
b // p,
q &
a,
b // r,
s & not
p,
q // r,
s implies
a = b ) & (
a,
b // a,
c implies
b,
a // b,
c ) & ex
x being
Element of st
(
a,
b // c,
x &
a,
c // b,
x ) & not for
x,
y,
z being
Element of holds
x,
y // x,
z & ex
x being
Element of st
(
a,
b // c,
x &
c <> x ) & (
a,
b // b,
d &
b <> a implies ex
x being
Element of st
(
c,
b // b,
x &
c,
a // d,
x ) ) & (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b ) & ex
x being
Element of st
(
a,
b _|_ c,
x &
c <> x ) & ( not
a,
b // c,
d implies ex
x being
Element of st
(
a,
b // a,
x &
c,
d // c,
x ) ) ) ) ) )
:: deftheorem Def11 defines LIN ANALMETR:def 11 :
definition
let POS be non
empty ParOrtStr ;
let a,
b be
Element of ;
func Line a,
b -> Subset of
means :
Def12:
for
x being
Element of holds
(
x in it iff
LIN a,
b,
x );
existence
ex b1 being Subset of st
for x being Element of holds
( x in b1 iff LIN a,b,x )
uniqueness
for b1, b2 being Subset of st ( for x being Element of holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines Line ANALMETR:def 12 :
:: deftheorem Def13 defines being_line ANALMETR:def 13 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th55:
theorem Th56:
theorem
theorem Th58:
:: deftheorem Def14 defines _|_ ANALMETR:def 14 :
:: deftheorem Def15 defines _|_ ANALMETR:def 15 :
:: deftheorem Def16 defines // ANALMETR:def 16 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
theorem
theorem
canceled;
theorem Th69:
theorem
canceled;
theorem Th71:
theorem
canceled;
theorem Th73:
theorem
canceled;
theorem
theorem Th76:
theorem
theorem Th78:
theorem
theorem Th80:
for
POS being
OrtAfSp for
b,
c,
a being
Element of holds
(
b,
c _|_ a,
a &
a,
a _|_ b,
c &
b,
c // a,
a &
a,
a // b,
c )
theorem Th81:
for
POS being
OrtAfSp for
a,
b,
c,
d being
Element of st
a,
b // c,
d holds
(
a,
b // d,
c &
b,
a // c,
d &
b,
a // d,
c &
c,
d // a,
b &
c,
d // b,
a &
d,
c // a,
b &
d,
c // b,
a )
theorem
for
POS being
OrtAfSp for
p,
q,
a,
b,
c,
d being
Element of st
p <> q & ( (
p,
q // a,
b &
p,
q // c,
d ) or (
p,
q // a,
b &
c,
d // p,
q ) or (
a,
b // p,
q &
c,
d // p,
q ) or (
a,
b // p,
q &
p,
q // c,
d ) ) holds
a,
b // c,
d
theorem Th83:
for
POS being
OrtAfSp for
a,
b,
c,
d being
Element of st
a,
b _|_ c,
d holds
(
a,
b _|_ d,
c &
b,
a _|_ c,
d &
b,
a _|_ d,
c &
c,
d _|_ a,
b &
c,
d _|_ b,
a &
d,
c _|_ a,
b &
d,
c _|_ b,
a )
theorem Th84:
for
POS being
OrtAfSp for
p,
q,
a,
b,
c,
d being
Element of st
p <> q & ( (
p,
q // a,
b &
p,
q _|_ c,
d ) or (
p,
q // c,
d &
p,
q _|_ a,
b ) or (
p,
q // a,
b &
c,
d _|_ p,
q ) or (
p,
q // c,
d &
a,
b _|_ p,
q ) or (
a,
b // p,
q &
c,
d _|_ p,
q ) or (
c,
d // p,
q &
a,
b _|_ p,
q ) or (
a,
b // p,
q &
p,
q _|_ c,
d ) or (
c,
d // p,
q &
p,
q _|_ a,
b ) ) holds
a,
b _|_ c,
d
theorem Th85:
for
POS being
OrtAfPl for
p,
q,
a,
b,
c,
d being
Element of st
p <> q & ( (
p,
q _|_ a,
b &
p,
q _|_ c,
d ) or (
p,
q _|_ a,
b &
c,
d _|_ p,
q ) or (
a,
b _|_ p,
q &
c,
d _|_ p,
q ) or (
a,
b _|_ p,
q &
p,
q _|_ c,
d ) ) holds
a,
b // c,
d
theorem
theorem
theorem Th88:
theorem Th89:
theorem
theorem Th91:
theorem