:: Analytical Metric Affine Spaces and Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users


Lm1: for V being RealLinearSpace
for v1, v2, w, y 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 a, b1, b2 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 Th1: :: ANALMETR:1
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:2
for V being RealLinearSpace
for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
proof end;

theorem Th3: :: ANALMETR:3
ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y by Def1, FUNCSDOM:23;

theorem :: ANALMETR:4
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 ;

theorem Th5: :: ANALMETR:5
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 Th6: :: ANALMETR:6
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 Th7: :: ANALMETR:7
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 Th8: :: ANALMETR:8
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 Th9: :: ANALMETR:9
for V being RealLinearSpace
for u1, u2, v, w, y 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 Th10: :: ANALMETR:10
for V being RealLinearSpace
for u, v1, v2, w, y 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 Th11: :: ANALMETR:11
for V being RealLinearSpace
for u, w, y being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
proof end;

theorem Th12: :: ANALMETR:12
for V being RealLinearSpace
for u, u1, u2, w, y 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 Th13: :: ANALMETR:13
for V being RealLinearSpace
for u, v, w, y 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 Th14: :: ANALMETR:14
for V being RealLinearSpace
for u, u1, v, 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 Th15: :: ANALMETR:15
for V being RealLinearSpace
for u, u1, v, 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 :: ANALMETR:def 3
u1 - u,v1 - v are_Ort_wrt w,y;
end;

:: deftheorem 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 object 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 object 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 object 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 object 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 object 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 Th16: :: ANALMETR:16
for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V
proof end;

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

theorem :: ANALMETR:18
for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of V
for p, p1, q, 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 OrtStr -> 1-sorted ;
aggr OrtStr(# carrier, orthogonality #) -> OrtStr ;
sel orthogonality c1 -> Relation of [: the carrier of c1, the carrier of c1:];
end;

definition
attr c1 is strict ;
struct ParOrtStr -> AffinStruct , OrtStr ;
aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
end;

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

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

definition
let POS be OrtStr ;
let a, b, c, d be Element of POS;
pred a,b _|_ c,d means :: ANALMETR:def 5
[[a,b],[c,d]] in the orthogonality of POS;
end;

:: deftheorem defines _|_ ANALMETR:def 5 :
for POS being OrtStr
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 6
 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 6 :
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 ;
end;

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

:: deftheorem ANALMETR:def 7 :
canceled;

registration
let POS be non empty ParOrtStr ;
cluster AffinStruct(# the carrier of POS, the CONGR of POS #) -> non empty ;
coherence
not AffinStruct(# the carrier of POS, the CONGR of POS #) is empty ;
end;

theorem Th20: :: ANALMETR:20
for V being RealLinearSpace
for w, y being VECTOR of V holds AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V)
proof end;

theorem Th21: :: ANALMETR:21
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 Th22: :: ANALMETR:22
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 & 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 Th23: :: ANALMETR:23
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
proof end;

theorem Th24: :: ANALMETR:24
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
proof end;

theorem Th25: :: ANALMETR:25
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 Th26: :: ANALMETR:26
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 Th27: :: ANALMETR:27
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 Th28: :: ANALMETR:28
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 Th29: :: ANALMETR:29
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 Th30: :: ANALMETR:30
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:31
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, p2, q 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 Th32: :: ANALMETR:32
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 Th3;

consider w0, y0 being VECTOR of V0 such that
Lm7: Gen w0,y0 by Lm6;

Lm8: now :: thesis: ( 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)) #);
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 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; :: thesis: verum
end;

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

registration
cluster non empty strict OrtAfSp-like for ParOrtStr ;
existence
ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfSp-like ) by Def7, Lm8;
end;

definition
mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ;
end;

theorem :: ANALMETR:33
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfSp
proof end;

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 :: thesis: ( 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)) #);
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 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; :: thesis: verum
end;

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

registration
cluster non empty strict OrtAfPl-like for ParOrtStr ;
existence
ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfPl-like ) by Def8, Lm11;
end;

definition
mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ;
end;

theorem :: ANALMETR:34
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfPl
proof end;

theorem :: ANALMETR:35
for POS being non empty ParOrtStr
for x being set holds
( x is Element of POS iff x is Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ) ;

theorem Th36: :: ANALMETR:36
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS
for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )
proof end;

registration
let POS be OrtAfSp;
cluster AffinStruct(# the carrier of POS, the CONGR of POS #) -> non trivial AffinSpace-like ;
correctness
coherence
( AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinSpace-like & not AffinStruct(# the carrier of POS, the CONGR of POS #) is trivial );
by Def7;
end;

registration
let POS be OrtAfPl;
cluster AffinStruct(# the carrier of POS, the CONGR of POS #) -> non trivial AffinSpace-like 2-dimensional ;
correctness
coherence
( AffinStruct(# the carrier of POS, the CONGR of POS #) is 2-dimensional & AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinSpace-like & not AffinStruct(# the carrier of POS, the CONGR of POS #) is trivial );
by Def8;
end;

theorem Th37: :: ANALMETR:37
for POS being OrtAfPl holds POS is OrtAfSp
proof end;

registration
cluster non empty OrtAfPl-like -> non empty OrtAfSp-like for ParOrtStr ;
coherence
for b1 being non empty ParOrtStr st b1 is OrtAfPl-like holds
b1 is OrtAfSp-like by Th37;
end;

theorem :: ANALMETR:38
for POS being OrtAfSp st AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane holds
POS is OrtAfPl
proof end;

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

definition
let POS be non empty ParOrtStr ;
let a, b, c be Element of POS;
pred LIN a,b,c means :: ANALMETR:def 10
a,b // a,c;
end;

:: deftheorem defines LIN ANALMETR:def 10 :
for POS being non empty ParOrtStr
for a, b, c being Element of POS holds
( LIN a,b,c iff a,b // a,c );

definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
func Line (a,b) -> Subset of POS means :Def10: :: ANALMETR:def 11
 for x being Element of POS holds
( x in it iff LIN a,b,x );
existence
ex b1 being Subset of POS st
for x being Element of POS holds
( x in b1 iff LIN a,b,x )
proof end;
uniqueness
for b1, b2 being Subset of POS st ( for x being Element of POS holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of POS holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Line ANALMETR:def 11 :
for POS being non empty ParOrtStr
for a, b being Element of POS
for b4 being Subset of POS holds
( b4 = Line (a,b) iff for x being Element of POS holds
( x in b4 iff LIN a,b,x ) );

definition
let POS be non empty ParOrtStr ;
let A be Subset of POS;
attr A is being_line means :: ANALMETR:def 12
 ex a, b being Element of POS st
( a <> b & A = Line (a,b) );
end;

:: deftheorem defines being_line ANALMETR:def 12 :
for POS being non empty ParOrtStr
for A being Subset of POS holds
( A is being_line iff ex a, b being Element of POS st
( a <> b & A = Line (a,b) ) );

theorem Th40: :: ANALMETR:40
for POS being OrtAfSp
for a, b, c being Element of POS
for a9, b9, c9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
proof end;

theorem Th41: :: ANALMETR:41
for POS being OrtAfSp
for a, b being Element of POS
for a9, b9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
proof end;

theorem :: ANALMETR:42
for POS being non empty ParOrtStr
for X being set holds
( X is Subset of POS iff X is Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) ) ;

theorem Th43: :: ANALMETR:43
for POS being OrtAfSp
for X being Subset of POS
for Y being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st X = Y holds
( X is being_line iff Y is being_line )
proof end;

definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
let K be Subset of POS;
pred a,b _|_ K means :: ANALMETR:def 13
 ex p, q being Element of POS st
( p <> q & K = Line (p,q) & a,b _|_ p,q );
end;

:: deftheorem defines _|_ ANALMETR:def 13 :
for POS being non empty ParOrtStr
for a, b being Element of POS
for K being Subset of POS holds
( a,b _|_ K iff ex p, q being Element of POS st
( p <> q & K = Line (p,q) & a,b _|_ p,q ) );

definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
pred K _|_ M means :Def13: :: ANALMETR:def 14
 ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M );
end;

:: deftheorem Def13 defines _|_ ANALMETR:def 14 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M ) );

definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
pred K // M means :: ANALMETR:def 15
 ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d );
end;

:: deftheorem defines // ANALMETR:def 15 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K // M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d ) );

theorem Th44: :: ANALMETR:44
for POS being non empty ParOrtStr
for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
proof end;

theorem Th45: :: ANALMETR:45
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
proof end;

theorem Th46: :: ANALMETR:46
for POS being OrtAfSp
for M, N being Subset of POS
for M9, N9 being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
proof end;

theorem :: ANALMETR:47
for POS being OrtAfSp
for K being Subset of POS
for a being Element of POS st K is being_line holds
a,a _|_ K
proof end;

theorem :: ANALMETR:48
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
proof end;

theorem :: ANALMETR:49
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
proof end;

definition
let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: //
redefine pred K // M;
symmetry
for K, M being Subset of POS st (POS,b1,b2) holds
(POS,b2,b1)
proof end;
end;

theorem Th50: :: ANALMETR:50
for POS being OrtAfSp
for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
proof end;

theorem Th51: :: ANALMETR:51
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
proof end;

definition
let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: _|_
redefine pred K _|_ M;
irreflexivity
for K being Subset of POS holds (POS,b1,b1)
proof end;
symmetry
for K, M being Subset of POS st (POS,b1,b2) holds
(POS,b2,b1)
proof end;
end;

theorem Th52: :: ANALMETR:52
for POS being OrtAfSp
for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M
proof end;

theorem :: ANALMETR:53
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
proof end;

theorem Th54: :: ANALMETR:54
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
proof end;

theorem :: ANALMETR:55
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
proof end;

theorem Th56: :: ANALMETR:56
for POS being OrtAfSp
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
proof end;

theorem :: ANALMETR:57
for POS being OrtAfSp
for A, K, M, N being Subset of POS
for a, b, p being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
proof end;

theorem Th58: :: ANALMETR:58
for POS being OrtAfSp
for a, b, c being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
proof end;

theorem Th59: :: ANALMETR:59
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 )
proof end;

theorem :: ANALMETR:60
for POS being OrtAfSp
for a, b, c, d, p, q 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
proof end;

theorem Th61: :: ANALMETR:61
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 )
proof end;

theorem Th62: :: ANALMETR:62
for POS being OrtAfSp
for a, b, c, d, p, q 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
proof end;

theorem Th63: :: ANALMETR:63
for POS being OrtAfPl
for a, b, c, d, p, q 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
proof end;

theorem :: ANALMETR:64
for POS being OrtAfPl
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
proof end;

theorem :: ANALMETR:65
for POS being OrtAfPl
for K, M, N being Subset of POS st M _|_ K & N _|_ K holds
M // N
proof end;

theorem Th66: :: ANALMETR:66
for POS being OrtAfPl
for M, N being Subset of POS st M _|_ N holds
ex p being Element of POS st
( p in M & p in N )
proof end;

theorem Th67: :: ANALMETR:67
for POS being OrtAfPl
for a, b, c, d being Element of POS st a,b _|_ c,d holds
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
proof end;

theorem :: ANALMETR:68
for POS being OrtAfPl
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
proof end;

theorem Th69: :: ANALMETR:69
for POS being OrtAfPl
for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
proof end;

theorem :: ANALMETR:70
for POS being OrtAfPl
for K being Subset of POS
for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
proof end;