:: ANALMETR semantic presentation

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) )
proof end;

Lm2: for V being RealLinearSpace
for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
proof end;

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)
proof end;

definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
pred Gen w,y means :Def1: :: ANALMETR:def 1
( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) );
end;

:: deftheorem Def1 defines Gen ANALMETR:def 1 :
for V being RealLinearSpace
for w, y being VECTOR of V holds
( Gen w,y iff ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) ) );

definition
let V be RealLinearSpace;
let u, v, w, y be VECTOR of V;
pred u,v are_Ort_wrt w,y means :Def2: :: ANALMETR:def 2
 ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 );
end;

:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def 2 :
for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( u,v are_Ort_wrt w,y iff ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) );

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 )
proof end;

theorem :: ANALMETR:1
canceled;

theorem :: ANALMETR:2
canceled;

theorem :: ANALMETR:3
canceled;

theorem :: ANALMETR:4
canceled;

theorem Th5: :: ANALMETR:5
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
proof end;

Lm5: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
proof end;

theorem :: ANALMETR:6
for V being RealLinearSpace
for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
proof end;

theorem Th7: :: ANALMETR:7
ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y
proof end;

theorem Th8: :: ANALMETR:8
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds
v,u are_Ort_wrt w,y
proof end;

theorem Th9: :: ANALMETR:9
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
proof end;

theorem Th10: :: ANALMETR:10
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,b * v are_Ort_wrt w,y
proof end;

theorem Th11: :: ANALMETR:11
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 )
proof end;

theorem Th12: :: ANALMETR:12
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
proof end;

theorem Th13: :: ANALMETR:13
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 ) )
proof end;

theorem Th14: :: ANALMETR:14
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 )
proof end;

theorem Th15: :: ANALMETR:15
for V being RealLinearSpace
for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
proof end;

theorem Th16: :: ANALMETR:16
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
proof end;

theorem Th17: :: ANALMETR:17
for V being RealLinearSpace
for w, y, u, v being VECTOR of V st Gen w,y & u <> 0. V holds
ex a being Real st v - (a * u),u are_Ort_wrt w,y
proof end;

theorem Th18: :: ANALMETR:18
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

theorem Th19: :: ANALMETR:19
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

definition
let V be RealLinearSpace;
let u, u1, v, v1, w, y be VECTOR of V;
pred u,u1,v,v1 are_Ort_wrt w,y means :Def3: :: ANALMETR:def 3
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 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: :: ANALMETR:def 4
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 ) )
proof end;
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
proof end;
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 :: ANALMETR:20
canceled;

theorem :: ANALMETR:21
canceled;

theorem Th22: :: ANALMETR:22
for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V
proof end;

theorem Th23: :: ANALMETR:23
for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V)
proof end;

theorem :: ANALMETR:24
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (Lambda (OASpace V)) 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 ) ) )
proof end;

definition
attr c1 is strict;
struct ParOrtStr -> AffinStruct ;
aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
sel orthogonality c1 -> Relation of [:the carrier of c1,the carrier of c1:];
end;

registration
cluster non empty ParOrtStr ;
existence
not for b1 being ParOrtStr holds b1 is empty
proof end;
end;

definition
let POS be non empty ParOrtStr ;
let a, b, c, d be Element of POS;
canceled;
pred a,b _|_ c,d means :Def6: :: ANALMETR:def 6
[[a,b],[c,d]] in the orthogonality of POS;
end;

:: deftheorem ANALMETR:def 5 :
canceled;

:: deftheorem Def6 defines _|_ ANALMETR:def 6 :
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS holds
( a,b _|_ c,d iff [[a,b],[c,d]] in the orthogonality of POS );

definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
func AMSpace V,w,y -> strict ParOrtStr equals :: ANALMETR:def 7
 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 :
for V being RealLinearSpace
for w, y being VECTOR of V holds AMSpace V,w,y = ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality V,w,y) #);

registration
let V be RealLinearSpace;
let w, y be VECTOR of V;
cluster AMSpace V,w,y -> non empty strict ;
coherence
not AMSpace V,w,y is empty
proof end;
end;

theorem :: ANALMETR:25
canceled;

theorem :: ANALMETR:26
canceled;

theorem :: ANALMETR:27
canceled;

theorem :: ANALMETR:28
for V being RealLinearSpace
for w, y being VECTOR of V holds
( the carrier of (AMSpace V,w,y) = the carrier of V & the CONGR of (AMSpace V,w,y) = lambda (DirPar V) & the orthogonality of (AMSpace V,w,y) = Orthogonality V,w,y ) ;

definition
let POS be non empty ParOrtStr ;
func Af POS -> strict AffinStruct equals :: ANALMETR:def 8
 AffinStruct(# the carrier of POS,the CONGR of POS #);
correctness
coherence
AffinStruct(# the carrier of POS,the CONGR of POS #) is strict AffinStruct ;
;
end;

:: deftheorem defines Af ANALMETR:def 8 :
for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS,the CONGR of POS #);

registration
let POS be non empty ParOrtStr ;
cluster Af POS -> non empty strict ;
coherence
not Af POS is empty
proof end;
end;

theorem :: ANALMETR:29
canceled;

theorem Th30: :: ANALMETR:30
for V being RealLinearSpace
for w, y being VECTOR of V holds Af (AMSpace V,w,y) = Lambda (OASpace V)
proof end;

theorem Th31: :: ANALMETR:31
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 )
proof end;

theorem Th32: :: ANALMETR:32
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 ) ) )
proof end;

theorem Th33: :: ANALMETR:33
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
proof end;

theorem Th34: :: ANALMETR:34
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
proof end;

theorem Th35: :: ANALMETR:35
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) holds p,q _|_ r,r
proof end;

theorem Th36: :: ANALMETR:36
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
proof end;

theorem Th37: :: ANALMETR:37
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 )
proof end;

theorem Th38: :: ANALMETR:38
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
proof end;

theorem Th39: :: ANALMETR:39
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
proof end;

theorem Th40: :: ANALMETR:40
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ p,q holds
p = q
proof end;

theorem :: ANALMETR:41
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
proof end;

theorem Th42: :: ANALMETR:42
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 )
proof end;

consider V0 being RealLinearSpace such that
Lm6: ex w, y being VECTOR of V0 st Gen w,y by Th7;

consider w0, y0 being VECTOR of V0 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 (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, Th33, Th34, Th35, Th36, Th37, Th39, Th40, Th42, DIRAF:48;
end;

definition
let IT be non empty ParOrtStr ;
attr IT is OrtAfSp-like means :Def9: :: ANALMETR:def 9
( 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 =