:: 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 :

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 :

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Orthogonality ANALMETR:def 4 :

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 c₁ is strict;
struct ParOrtStr -> AffinStruct ;
aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
sel orthogonality c₁ -> Relation of [:the carrier of c₁,the carrier of c₁:];

end;

registration

cluster non empty ParOrtStr ;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def5 defines // ANALMETR:def 5 :

:: deftheorem Def6 defines _|_ ANALMETR:def 6 :

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 ;

end;

:: deftheorem defines AMSpace ANALMETR:def 7 :

registration

let V be RealLinearSpace;
let w, y be VECTOR of V;
cluster AMSpace V,w,y -> non empty strict ;
coherence

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 ;

end;

:: deftheorem defines Af ANALMETR:def 8 :

registration

let POS be non empty ParOrtStr ;
cluster Af POS -> non empty strict ;
coherence

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; :: thesis:

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 = 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 Def9 defines OrtAfSp-like ANALMETR:def 9 :

registration

cluster non empty strict OrtAfSp-like ParOrtStr ;
existence

proof end;

end;

definition

mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ;

end;

theorem :: ANALMETR:43

canceled;

theorem :: ANALMETR:44

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 Th7;

consider w0, y0 being VECTOR of V0 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 V0 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 (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, Th33, Th34, Th35, Th36, Th37, Th38, Th40, DIRAF:53; :: thesis:

end;

definition

let IT be non empty ParOrtStr ;
attr IT is OrtAfPl-like means :Def10: :: ANALMETR:def 10
( 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 Def10 defines OrtAfPl-like ANALMETR:def 10 :

registration

cluster non empty strict OrtAfPl-like ParOrtStr ;
existence

proof end;

end;

definition

mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ;

end;

theorem :: ANALMETR:45

canceled;

theorem :: ANALMETR:46

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:47

for POS being non empty ParOrtStr
for x being set holds
( x is Element of POS iff x is Element of (Af POS) ) ;

theorem Th48: :: ANALMETR:48

for POS being non empty ParOrtStr
for a, b, c, d being Element of POS
for a', b', c', d' being Element of (Af POS) st a = a' & b = b' & c = c' & d = d' holds
( a,b // c,d iff a',b' // c',d' )

proof end;

Lm12: for POS being OrtAfSp holds Af POS is AffinSpace
by Def9;

registration

let POS be OrtAfSp;
cluster Af POS -> non empty non trivial strict AffinSpace-like ;
correctness by Lm12;

end;

Lm13: for POS being OrtAfPl holds Af POS is AffinPlane
by Def10;

registration

let POS be OrtAfPl;
cluster Af POS -> non empty non trivial strict AffinSpace-like 2-dimensional ;
correctness by Lm13;

end;

theorem Th49: :: ANALMETR:49

for POS being OrtAfPl holds POS is OrtAfSp

proof end;

registration

cluster non empty OrtAfPl-like -> non empty OrtAfSp-like ParOrtStr ;
coherence by Th49;

end;

theorem :: ANALMETR:50

for POS being OrtAfSp st Af POS is AffinPlane holds
POS is OrtAfPl

proof end;

theorem :: ANALMETR:51

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 :Def11: :: ANALMETR:def 11
a,b // a,c;

end;

:: deftheorem Def11 defines LIN ANALMETR:def 11 :

definition

let POS be non empty ParOrtStr ;
let a, b be Element of POS;
func Line a,b -> Subset of POS means :Def12: :: ANALMETR:def 12
for x being Element of POS holds
( x in it iff LIN a,b,x );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Line ANALMETR:def 12 :

definition

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

end;

:: deftheorem Def13 defines being_line ANALMETR:def 13 :

notation

let POS be non empty ParOrtStr ;
let A be Subset of POS;
synonym A is_line for being_line A;

end;

theorem :: ANALMETR:52

canceled;

theorem :: ANALMETR:53

canceled;

theorem :: ANALMETR:54

canceled;

theorem Th55: :: ANALMETR:55

for POS being OrtAfSp
for a, b, c being Element of POS
for a', b', c' being Element of (Af POS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )

proof end;

theorem Th56: :: ANALMETR:56

for POS being OrtAfSp
for a, b being Element of POS
for a', b' being Element of (Af POS) st a = a' & b = b' holds
Line a,b = Line a',b'

proof end;

theorem :: ANALMETR:57

for POS being non empty ParOrtStr
for X being set holds
( X is Subset of POS iff X is Subset of (Af POS) ) ;

theorem Th58: :: ANALMETR:58

for POS being OrtAfSp
for X being Subset of POS
for Y being Subset of (Af POS) st X = Y holds
( X is_line iff Y is_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 :Def14: :: ANALMETR:def 14
ex p, q being Element of POS st
( p <> q & K = Line p,q & a,b _|_ p,q );

end;

:: deftheorem Def14 defines _|_ ANALMETR:def 14 :

definition

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

end;

:: deftheorem Def15 defines _|_ ANALMETR:def 15 :

definition

let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
pred K // M means :Def16: :: ANALMETR:def 16
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 Def16 defines // ANALMETR:def 16 :

theorem :: ANALMETR:59

canceled;

theorem :: ANALMETR:60

canceled;

theorem :: ANALMETR:61

canceled;

theorem Th62: :: ANALMETR:62

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_line ) & ( K _|_ M implies ( K is_line & M is_line ) ) )

proof end;

theorem Th63: :: ANALMETR:63

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 Th64: :: ANALMETR:64

for POS being OrtAfSp
for M, N being Subset of POS
for M', N' being Subset of (Af POS) st M = M' & N = N' holds
( M // N iff M' // N' )

proof end;

theorem :: ANALMETR:65

for POS being OrtAfSp
for K being Subset of POS
for a being Element of POS st K is_line holds
a,a _|_ K

proof end;

theorem :: ANALMETR:66

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:67

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;

theorem Th68: :: ANALMETR:68

for POS being OrtAfSp
for K, M being Subset of POS st K // M holds
M // K

proof end;

theorem Th69: :: ANALMETR:69

for POS being OrtAfSp
for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & ( K // M or M // K ) holds
r,s _|_ M

proof end;

theorem Th70: :: ANALMETR:70

for POS being OrtAfSp
for K, M being Subset of POS st K _|_ M holds
M _|_ K

proof end;

definition

let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: //
redefine pred K // M;
symmetry by Th68;
:: original: _|_
redefine pred K _|_ M;
symmetry by Th70;

end;

theorem Th71: :: ANALMETR:71

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;

theorem Th72: :: ANALMETR:72

for POS being OrtAfSp
for K being Subset of POS holds not K _|_ K

proof end;

theorem Th73: :: ANALMETR:73

for POS being OrtAfSp
for K, M, N being Subset of POS st ( K _|_ M or M _|_ K ) & ( K // N or N // K ) holds
( M _|_ N & N _|_ M )

proof end;

theorem Th74: :: ANALMETR:74

for POS being OrtAfSp
for K, N being Subset of POS st K // N holds
not K _|_ N

proof end;

theorem :: ANALMETR:75

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 Th76: :: ANALMETR:76

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_line holds
K = Line a,b

proof end;

theorem :: ANALMETR:77

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_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K

proof end;

theorem Th78: :: ANALMETR:78

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:79

for POS being OrtAfSp
for M, N, K, A being Subset of POS
for p, a, b 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_line holds
A _|_ K

proof end;

theorem Th80: :: ANALMETR:80

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 )

proof end;

theorem Th81: :: ANALMETR:81

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:82

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

proof end;

theorem Th83: :: ANALMETR:83

proof end;

theorem Th84: :: ANALMETR:84

proof end;

theorem Th85: :: ANALMETR:85

proof end;

theorem :: ANALMETR:86

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_line & c in N & d in N & c <> d & N is_line & a,b // c,d holds
M // N

proof end;

theorem :: ANALMETR:87

for POS being OrtAfPl
for K, M, N being Subset of POS st ( K _|_ M or M _|_ K ) & ( K _|_ N or N _|_ K ) holds
( M // N & N // M )

proof end;

theorem Th88: :: ANALMETR:88

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 Th89: :: ANALMETR:89

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:90

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 Th91: :: ANALMETR:91

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:92

for POS being OrtAfPl
for K being Subset of POS
for a being Element of POS st K is_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )

proof end;