:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received August 10, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

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

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;

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

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

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

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 )

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

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

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

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 )

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 )

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

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 Th10: :: ANALMETR:10

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 )

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 Th11: :: ANALMETR:11

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

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 Th12: :: ANALMETR:12

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

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 Th13: :: ANALMETR:13

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

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 Th14: :: ANALMETR:14

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

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 Th15: :: ANALMETR:15

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

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;

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

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;

ex b_{1} being Relation of [: the carrier of V, the carrier of V:] st

for x, z being set holds

( [x,z] in b_{1} 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 b_{1}, b_{2} being Relation of [: the carrier of V, the carrier of V:] st ( for x, z being set holds

( [x,z] in b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for x, z being set holds

( [x,z] in b

( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )

proof end;

uniqueness for b

( [x,z] in b

( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds

( [x,z] in b

( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Orthogonality ANALMETR:def 4 :

for V being RealLinearSpace

for w, y being VECTOR of V

for b_{4} being Relation of [: the carrier of V, the carrier of V:] holds

( b_{4} = Orthogonality (V,w,y) iff for x, z being set holds

( [x,z] in b_{4} 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 V being RealLinearSpace

for w, y being VECTOR of V

for b

( b

( [x,z] in b

( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) );

theorem :: ANALMETR:18

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

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_{1} is strict ;

struct ParOrtStr -> AffinStruct ;

aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;

sel orthogonality c_{1} -> Relation of [: the carrier of c_{1}, the carrier of c_{1}:];

end;
struct ParOrtStr -> AffinStruct ;

aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;

sel orthogonality c

:: deftheorem Def5 defines _|_ ANALMETR:def 5 :

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

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;

coherence

ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #) is strict ParOrtStr ;

;

end;
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 ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #);

coherence

ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #) is strict ParOrtStr ;

;

:: 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)) #);

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

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 ;

coherence

AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct ;

;

end;
func Af POS -> strict AffinStruct equals :: ANALMETR:def 7

AffinStruct(# the carrier of POS, the CONGR of POS #);

correctness AffinStruct(# the carrier of POS, the CONGR of POS #);

coherence

AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct ;

;

:: deftheorem defines Af ANALMETR:def 7 :

for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #);

for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #);

theorem Th20: :: ANALMETR:20

for V being RealLinearSpace

for w, y being VECTOR of V holds Af (AMSpace (V,w,y)) = Lambda (OASpace V)

for w, y being VECTOR of V holds Af (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 )

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

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 Th23: :: ANALMETR:23

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

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 Th24: :: ANALMETR:24

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

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

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

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 )

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

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

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

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

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

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

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

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

definition

let IT be non empty ParOrtStr ;

end;
attr IT is OrtAfSp-like means :Def8: :: 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 ) ) );

( 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 ) ) );

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

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

existence

ex b_{1} being non empty ParOrtStr st

( b_{1} is strict & b_{1} is OrtAfSp-like )

end;
ex b

( b

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

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

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

definition

let IT be non empty ParOrtStr ;

end;
attr IT is OrtAfPl-like means :Def9: :: 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 ) ) );

( 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 ) ) );

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

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

existence

ex b_{1} being non empty ParOrtStr st

( b_{1} is strict & b_{1} is OrtAfPl-like )

end;
ex b

( b

proof end;

theorem :: ANALMETR:35

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 (Af POS) st a = a9 & b = b9 & c = c9 & d = d9 holds

( a,b // c,d iff a9,b9 // c9,d9 )

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 )

proof end;

registration

let POS be OrtAfSp;

correctness

coherence

( Af POS is AffinSpace-like & not Af POS is trivial );

by Def8;

end;
correctness

coherence

( Af POS is AffinSpace-like & not Af POS is trivial );

by Def8;

registration

let POS be OrtAfPl;

correctness

coherence

( Af POS is 2-dimensional & Af POS is AffinSpace-like & not Af POS is trivial );

by Def9;

end;
correctness

coherence

( Af POS is 2-dimensional & Af POS is AffinSpace-like & not Af POS is trivial );

by Def9;

registration

coherence

for b_{1} being non empty ParOrtStr st b_{1} is OrtAfPl-like holds

b_{1} is OrtAfSp-like
by Th37;

end;
for b

b

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

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

:: deftheorem Def10 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 );

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;

ex b_{1} being Subset of POS st

for x being Element of POS holds

( x in b_{1} iff LIN a,b,x )

for b_{1}, b_{2} being Subset of POS st ( for x being Element of POS holds

( x in b_{1} iff LIN a,b,x ) ) & ( for x being Element of POS holds

( x in b_{2} iff LIN a,b,x ) ) holds

b_{1} = b_{2}

end;
let a, b be Element of POS;

func Line (a,b) -> Subset of POS means :Def11: :: ANALMETR:def 11

for x being Element of POS holds

( x in it iff LIN a,b,x );

existence for x being Element of POS holds

( x in it iff LIN a,b,x );

ex b

for x being Element of POS holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 defines Line ANALMETR:def 11 :

for POS being non empty ParOrtStr

for a, b being Element of POS

for b_{4} being Subset of POS holds

( b_{4} = Line (a,b) iff for x being Element of POS holds

( x in b_{4} iff LIN a,b,x ) );

for POS being non empty ParOrtStr

for a, b being Element of POS

for b

( b

( x in b

definition

let POS be non empty ParOrtStr ;

let A be Subset of POS;

end;
let A be Subset of POS;

attr A is being_line means :Def12: :: ANALMETR:def 12

ex a, b being Element of POS st

( a <> b & A = Line (a,b) );

ex a, b being Element of POS st

( a <> b & A = Line (a,b) );

:: deftheorem Def12 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) ) );

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 (Af POS) st a = a9 & b = b9 & c = c9 holds

( LIN a,b,c iff LIN a9,b9,c9 )

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 )

proof end;

theorem Th41: :: ANALMETR:41

for POS being OrtAfSp

for a, b being Element of POS

for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds

Line (a,b) = Line (a9,b9)

for a, b being Element of POS

for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds

Line (a,b) = Line (a9,b9)

proof end;

theorem :: ANALMETR:42

theorem Th43: :: ANALMETR:43

for POS being OrtAfSp

for X being Subset of POS

for Y being Subset of (Af POS) st X = Y holds

( X is being_line iff Y is being_line )

for X being Subset of POS

for Y being Subset of (Af POS) st X = Y holds

( X is being_line iff Y is being_line )

proof end;

:: deftheorem Def13 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 ) );

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

:: deftheorem Def14 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 ) );

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

:: deftheorem Def15 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 ) );

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

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

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 (Af POS) st M = M9 & N = N9 holds

( M // N iff M9 // N9 )

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 )

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

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

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

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,b_{1},b_{2}) holds

(POS,b_{2},b_{1})

end;
let K, M be Subset of POS;

:: original: //

redefine pred K // M;

symmetry

for K, M being Subset of POS st (POS,b

(POS,b

proof 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

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

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,b_{1},b_{1})

for K, M being Subset of POS st (POS,b_{1},b_{2}) holds

(POS,b_{2},b_{1})

end;
let K, M be Subset of POS;

:: original: _|_

redefine pred K _|_ M;

irreflexivity

for K being Subset of POS holds (POS,b

proof end;

symmetry for K, M being Subset of POS st (POS,b

(POS,b

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 )

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)

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

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

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 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 being_line holds

A _|_ K

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 being_line holds

A _|_ K

proof end;

theorem Th58: :: ANALMETR:58

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 )

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

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

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

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

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

proof end;

theorem Th63: :: ANALMETR:63

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

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

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

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 )

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 )

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 )

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 )

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;