begin
Lm1:
for V being RealLinearSpace
for v1, w, y, v2 being VECTOR of V
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 V holds (0 * w) + (0 * y) = 0. V
Lm3:
for V being RealLinearSpace
for v, w, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
Lm4:
for V being RealLinearSpace
for w, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
Lm5:
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
theorem Th7:
for
V being
RealLinearSpace for
u,
v,
w,
y being
VECTOR of
V 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 Th9:
for
V being
RealLinearSpace for
w,
y,
v,
u1,
u2 being
VECTOR of
V 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 Th10:
for
V being
RealLinearSpace for
w,
y,
u,
v1,
v2 being
VECTOR of
V 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 Th12:
for
V being
RealLinearSpace for
w,
y,
u,
u1,
u2 being
VECTOR of
V 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
::
deftheorem Def3 defines
are_Ort_wrt ANALMETR:def 3 :
for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V 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
V;
func Orthogonality (
V,
w,
y)
-> Relation of
[: the carrier of V, the carrier of V:] means :
Def4:
for
x,
z being
set holds
(
[x,z] in it iff ex
u,
u1,
v,
v1 being
VECTOR of
V st
(
x = [u,u1] &
z = [v,v1] &
u,
u1,
v,
v1 are_Ort_wrt 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, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt 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, u1, v, v1 being VECTOR of V 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 V 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 V
for b4 being Relation of [: the carrier of V, the carrier of V:] 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 V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) );
theorem Th21:
for
V being
RealLinearSpace for
u,
u1,
v,
v1,
w,
y being
VECTOR of
V for
p,
p1,
q,
q1 being
Element of
(AMSpace (V,w,y)) 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 Th22:
for
V being
RealLinearSpace for
w,
y,
u,
v,
u1,
v1 being
VECTOR of
V for
p,
q,
p1,
q1 being
Element of
(AMSpace (V,w,y)) 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 Th23:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
q,
p1,
q1 being
Element of
(AMSpace (V,w,y)) st
p,
q _|_ p1,
q1 holds
p1,
q1 _|_ p,
q
theorem Th24:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
q,
p1,
q1 being
Element of
(AMSpace (V,w,y)) st
p,
q _|_ p1,
q1 holds
p,
q _|_ q1,
p1
theorem Th26:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
p1,
q,
q1,
r,
r1 being
Element of
(AMSpace (V,w,y)) st
p,
p1 _|_ q,
q1 &
p,
p1 // r,
r1 & not
p = p1 holds
q,
q1 _|_ r,
r1
theorem Th27:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V st
Gen w,
y holds
for
p,
q,
r being
Element of
(AMSpace (V,w,y)) ex
r1 being
Element of
(AMSpace (V,w,y)) st
(
p,
q _|_ r,
r1 &
r <> r1 )
theorem Th28:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
p1,
q,
q1,
r,
r1 being
Element of
(AMSpace (V,w,y)) st
Gen w,
y &
p,
p1 _|_ q,
q1 &
p,
p1 _|_ r,
r1 & not
p = p1 holds
q,
q1 // r,
r1
theorem Th29:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
q,
r,
r1,
r2 being
Element of
(AMSpace (V,w,y)) st
Gen w,
y &
p,
q _|_ r,
r1 &
p,
q _|_ r,
r2 holds
p,
q _|_ r1,
r2
theorem
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
q,
p1,
p2 being
Element of
(AMSpace (V,w,y)) st
Gen w,
y &
p,
q _|_ p1,
p2 &
p1,
q _|_ p2,
p holds
p2,
q _|_ p,
p1
theorem Th32:
for
V being
RealLinearSpace for
w,
y being
VECTOR of
V for
p,
p1 being
Element of
(AMSpace (V,w,y)) st
Gen w,
y &
p <> p1 holds
for
q being
Element of
(AMSpace (V,w,y)) ex
q1 being
Element of
(AMSpace (V,w,y)) st
(
p,
p1 // p,
q1 &
p,
p1 _|_ q1,
q )
consider V0 being RealLinearSpace such that
Lm6:
ex w, y being VECTOR of V0 st Gen w,y
by Th3;
consider w0, y0 being VECTOR of V0 such that
Lm7:
Gen w0,y0
by Lm6;
Lm8:
now ( 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 (AMSpace (V0,w0,y0)) 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 (AMSpace (V0,w0,y0)) st a <> b holds
ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b _|_ c,x & c <> x ) ) )
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 Th20;
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:26;
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
(AMSpace (V0,w0,y0)) 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
(AMSpace (V0,w0,y0)) st
a <> b holds
ex
x being
Element of
(AMSpace (V0,w0,y0)) st
(
a,
b // a,
x &
a,
b _|_ x,
c ) ) & ( for
a,
b,
c being
Element of
(AMSpace (V0,w0,y0)) ex
x being
Element of
(AMSpace (V0,w0,y0)) st
(
a,
b _|_ c,
x &
c <> x ) ) )
by A1, Lm7, Th23, Th24, Th25, Th26, Th27, Th29, Th30, Th32, DIRAF:41;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfSp-like means :
Def8:
(
AffinStruct(# the
carrier of
IT, the
CONGR of
IT #) is
AffinSpace & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
IT 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
IT st
a <> b holds
ex
x being
Element of
IT st
(
a,
b // a,
x &
a,
b _|_ x,
c ) ) & ( for
a,
b,
c being
Element of
IT ex
x being
Element of
IT st
(
a,
b _|_ c,
x &
c <> x ) ) );
end;
::
deftheorem Def8 defines
OrtAfSp-like ANALMETR:def 8 :
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 IT 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 IT st a <> b holds
ex x being Element of IT st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );
consider V0 being RealLinearSpace such that
Lm9:
ex w, y being VECTOR of V0 st Gen w,y
by Th3;
consider w0, y0 being VECTOR of V0 such that
Lm10:
Gen w0,y0
by Lm9;
Lm11:
now ( 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 (AMSpace (V0,w0,y0)) 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 (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b _|_ c,x & c <> x ) ) )
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 Th20;
( ( for
a,
b being
Real st
(a * w0) + (b * y0) = 0. V0 holds
(
a = 0 &
b = 0 ) ) & ( for
w1 being
VECTOR of
V0 ex
a,
b being
Real st
w1 = (a * w0) + (b * y0) ) )
by Def1, Lm10;
then
OASpace V0 is
OAffinPlane
by ANALOAF:28;
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
(AMSpace (V0,w0,y0)) 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
(AMSpace (V0,w0,y0)) ex
x being
Element of
(AMSpace (V0,w0,y0)) st
(
a,
b _|_ c,
x &
c <> x ) ) )
by A1, Lm10, Th23, Th24, Th25, Th26, Th27, Th28, Th30, DIRAF:45;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfPl-like means :
Def9:
(
AffinStruct(# the
carrier of
IT, the
CONGR of
IT #) is
AffinPlane & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
IT 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
IT ex
x being
Element of
IT st
(
a,
b _|_ c,
x &
c <> x ) ) );
end;
::
deftheorem Def9 defines
OrtAfPl-like ANALMETR:def 9 :
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 IT 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 IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );
theorem Th36:
for
POS being non
empty ParOrtStr for
a,
b,
c,
d being
Element of
POS for
a9,
b9,
c9,
d9 being
Element of
(Af POS) st
a = a9 &
b = b9 &
c = c9 &
d = d9 holds
(
a,
b // c,
d iff
a9,
b9 // c9,
d9 )
theorem
for
POS being non
empty ParOrtStr holds
(
POS is
OrtAfPl-like iff ( ex
a,
b being
Element of
POS st
a <> b & ( for
a,
b,
c,
d,
p,
q,
r,
s being
Element of
POS 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
POS st
(
a,
b // c,
x &
a,
c // b,
x ) & not for
x,
y,
z being
Element of
POS holds
x,
y // x,
z & ex
x being
Element of
POS st
(
a,
b // c,
x &
c <> x ) & (
a,
b // b,
d &
b <> a implies ex
x being
Element of
POS 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
POS st
(
a,
b _|_ c,
x &
c <> x ) & ( not
a,
b // c,
d implies ex
x being
Element of
POS st
(
a,
b // a,
x &
c,
d // c,
x ) ) ) ) ) )
theorem Th40:
for
POS being
OrtAfSp for
a,
b,
c being
Element of
POS for
a9,
b9,
c9 being
Element of
(Af POS) st
a = a9 &
b = b9 &
c = c9 holds
(
LIN a,
b,
c iff
LIN a9,
b9,
c9 )
theorem Th46:
for
POS being
OrtAfSp for
M,
N being
Subset of
POS for
M9,
N9 being
Subset of
(Af POS) st
M = M9 &
N = N9 holds
(
M // N iff
M9 // N9 )
theorem Th58:
for
POS being
OrtAfSp for
b,
c,
a being
Element of
POS holds
(
b,
c _|_ a,
a &
a,
a _|_ b,
c &
b,
c // a,
a &
a,
a // b,
c )
theorem Th59:
for
POS being
OrtAfSp for
a,
b,
c,
d being
Element of
POS 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
POS 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 Th61:
for
POS being
OrtAfSp for
a,
b,
c,
d being
Element of
POS 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 Th62:
for
POS being
OrtAfSp for
p,
q,
a,
b,
c,
d being
Element of
POS 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 Th63:
for
POS being
OrtAfPl for
p,
q,
a,
b,
c,
d being
Element of
POS 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