:: by Eugeniusz Kusak and Krzysztof Radziszewski

::

:: Received November 30, 1990

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

definition

let IT be non empty AffinStruct ;

end;
attr IT is Semi_Affine_Space-like means :Def1: :: SEMI_AF1:def 1

( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds

p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds

b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st

( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st

for b, c being Element of IT holds

( o,a // o,p & ex d being Element of IT st

( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds

a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds

not a,d // b,c ) );

( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds

p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds

b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st

( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st

for b, c being Element of IT holds

( o,a // o,p & ex d being Element of IT st

( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds

a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds

not a,d // b,c ) );

:: deftheorem Def1 defines Semi_Affine_Space-like SEMI_AF1:def 1 :

for IT being non empty AffinStruct holds

( IT is Semi_Affine_Space-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds

p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds

b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st

( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st

for b, c being Element of IT holds

( o,a // o,p & ex d being Element of IT st

( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds

a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds

not a,d // b,c ) ) );

for IT being non empty AffinStruct holds

( IT is Semi_Affine_Space-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds

p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds

b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st

( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st

for b, c being Element of IT holds

( o,a // o,p & ex d being Element of IT st

( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds

a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds

not a,d // b,c ) ) );

registration
end;

theorem Th6: :: SEMI_AF1:6

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st a,b // c,d holds

( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a )

for a, b, c, d being Element of SAS st a,b // c,d holds

( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a )

proof end;

theorem Th7: :: SEMI_AF1:7

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st a,b // a,c holds

( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c )

for a, b, c being Element of SAS st a,b // a,c holds

( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c )

proof end;

theorem Th8: :: SEMI_AF1:8

for SAS being Semi_Affine_Space

for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds

p,q // r,s

for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds

p,q // r,s

proof end;

theorem :: SEMI_AF1:9

theorem :: SEMI_AF1:10

theorem :: SEMI_AF1:11

for SAS being Semi_Affine_Space

for a, b, c, x being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds

a,b // a,c

for a, b, c, x being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds

a,b // a,c

proof end;

theorem Th12: :: SEMI_AF1:12

for SAS being Semi_Affine_Space

for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds

not p,q // p,c

for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds

not p,q // p,c

proof end;

theorem Th13: :: SEMI_AF1:13

for SAS being Semi_Affine_Space

for p, q being Element of SAS st p <> q holds

ex r being Element of SAS st not p,q // p,r

for p, q being Element of SAS st p <> q holds

ex r being Element of SAS st not p,q // p,r

proof end;

theorem Th14: :: SEMI_AF1:14

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st not a,b // a,c holds

( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b )

for a, b, c being Element of SAS st not a,b // a,c holds

( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b )

proof end;

theorem Th15: :: SEMI_AF1:15

for SAS being Semi_Affine_Space

for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds

not p,q // r,s

for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds

not p,q // r,s

proof end;

theorem Th16: :: SEMI_AF1:16

for SAS being Semi_Affine_Space

for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds

not p,q // p,r

for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds

not p,q // p,r

proof end;

theorem Th17: :: SEMI_AF1:17

for SAS being Semi_Affine_Space

for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds

p = r

for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds

p = r

proof end;

theorem Th18: :: SEMI_AF1:18

for SAS being Semi_Affine_Space

for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds

r1 = r2

for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds

r1 = r2

proof end;

theorem Th19: :: SEMI_AF1:19

for SAS being Semi_Affine_Space

for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds

r1 = r2

for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds

r1 = r2

proof end;

theorem :: SEMI_AF1:20

theorem :: SEMI_AF1:21

:: deftheorem defines are_collinear SEMI_AF1:def 2 :

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS holds

( a,b,c are_collinear iff a,b // a,c );

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS holds

( a,b,c are_collinear iff a,b // a,c );

theorem Th22: :: SEMI_AF1:22

for SAS being Semi_Affine_Space

for a1, a2, a3 being Element of SAS st a1,a2,a3 are_collinear holds

( a1,a3,a2 are_collinear & a2,a1,a3 are_collinear & a2,a3,a1 are_collinear & a3,a1,a2 are_collinear & a3,a2,a1 are_collinear ) by Th7;

for a1, a2, a3 being Element of SAS st a1,a2,a3 are_collinear holds

( a1,a3,a2 are_collinear & a2,a1,a3 are_collinear & a2,a3,a1 are_collinear & a3,a1,a2 are_collinear & a3,a2,a1 are_collinear ) by Th7;

theorem Th23: :: SEMI_AF1:23

for SAS being Semi_Affine_Space

for a, b, c, p, q, r being Element of SAS st not a,b,c are_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds

not p,q,r are_collinear by Th15;

for a, b, c, p, q, r being Element of SAS st not a,b,c are_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds

not p,q,r are_collinear by Th15;

theorem Th24: :: SEMI_AF1:24

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds

a,b,c are_collinear by Def1, Th1, Th3;

for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds

a,b,c are_collinear by Def1, Th1, Th3;

theorem Th25: :: SEMI_AF1:25

for SAS being Semi_Affine_Space

for p, q being Element of SAS st p <> q holds

ex r being Element of SAS st not p,q,r are_collinear

for p, q being Element of SAS st p <> q holds

ex r being Element of SAS st not p,q,r are_collinear

proof end;

theorem Th26: :: SEMI_AF1:26

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st a,b,c are_collinear & a,b,d are_collinear holds

a,b // c,d

for a, b, c, d being Element of SAS st a,b,c are_collinear & a,b,d are_collinear holds

a,b // c,d

proof end;

theorem Th27: :: SEMI_AF1:27

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st not a,b,c are_collinear & a,b // c,d holds

not a,b,d are_collinear

for a, b, c, d being Element of SAS st not a,b,c are_collinear & a,b // c,d holds

not a,b,d are_collinear

proof end;

theorem Th28: :: SEMI_AF1:28

for SAS being Semi_Affine_Space

for a, b, c, d, x being Element of SAS st not a,b,c are_collinear & a,b // c,d & c <> d & c,d,x are_collinear holds

not a,b,x are_collinear by Th8, Th27;

for a, b, c, d, x being Element of SAS st not a,b,c are_collinear & a,b // c,d & c <> d & c,d,x are_collinear holds

not a,b,x are_collinear by Th8, Th27;

theorem :: SEMI_AF1:29

for SAS being Semi_Affine_Space

for a, b, o, x being Element of SAS st not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear holds

o = x

for a, b, o, x being Element of SAS st not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear holds

o = x

proof end;

theorem :: SEMI_AF1:30

for SAS being Semi_Affine_Space

for a, a9, b, b9, o being Element of SAS st o <> a & o <> b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear holds

a,b // a9,b9

for a, a9, b, b9, o being Element of SAS st o <> a & o <> b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear holds

a,b // a9,b9

proof end;

theorem :: SEMI_AF1:31

for SAS being Semi_Affine_Space

for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 are_collinear & a,b,p2 are_collinear & c,d,p1 are_collinear & c,d,p2 are_collinear holds

p1 = p2

for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 are_collinear & a,b,p2 are_collinear & c,d,p1 are_collinear & c,d,p2 are_collinear holds

p1 = p2

proof end;

theorem Th32: :: SEMI_AF1:32

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds

a,c // b,d

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds

a,c // b,d

proof end;

theorem Th33: :: SEMI_AF1:33

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds

c,b // c,d

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds

c,b // c,d

proof end;

theorem Th34: :: SEMI_AF1:34

for SAS being Semi_Affine_Space

for a, b, c, d1, d2, o being Element of SAS st not o,a,c are_collinear & o,a,b are_collinear & o,c,d1 are_collinear & o,c,d2 are_collinear & a,c // b,d1 & a,c // b,d2 holds

d1 = d2 by Th19;

for a, b, c, d1, d2, o being Element of SAS st not o,a,c are_collinear & o,a,b are_collinear & o,c,d1 are_collinear & o,c,d2 are_collinear & a,c // b,d1 & a,c // b,d2 holds

d1 = d2 by Th19;

theorem :: SEMI_AF1:35

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear by Def1;

for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear by Def1;

::

:: PARALLELOGRAM

::

:: PARALLELOGRAM

::

definition

let SAS be Semi_Affine_Space;

let a, b, c, d be Element of SAS;

end;
let a, b, c, d be Element of SAS;

pred parallelogram a,b,c,d means :: SEMI_AF1:def 3

( not a,b,c are_collinear & a,b // c,d & a,c // b,d );

( not a,b,c are_collinear & a,b // c,d & a,c // b,d );

:: deftheorem defines parallelogram SEMI_AF1:def 3 :

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS holds

( parallelogram a,b,c,d iff ( not a,b,c are_collinear & a,b // c,d & a,c // b,d ) );

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS holds

( parallelogram a,b,c,d iff ( not a,b,c are_collinear & a,b // c,d & a,c // b,d ) );

theorem Th36: :: SEMI_AF1:36

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d )

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d )

proof end;

theorem Th37: :: SEMI_AF1:37

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )

proof end;

theorem Th38: :: SEMI_AF1:38

for SAS being Semi_Affine_Space

for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds

( not a1,a2,a3 are_collinear & not a1,a3,a2 are_collinear & not a1,a2,a4 are_collinear & not a1,a4,a2 are_collinear & not a1,a3,a4 are_collinear & not a1,a4,a3 are_collinear & not a2,a1,a3 are_collinear & not a2,a3,a1 are_collinear & not a2,a1,a4 are_collinear & not a2,a4,a1 are_collinear & not a2,a3,a4 are_collinear & not a2,a4,a3 are_collinear & not a3,a1,a2 are_collinear & not a3,a2,a1 are_collinear & not a3,a1,a4 are_collinear & not a3,a4,a1 are_collinear & not a3,a2,a4 are_collinear & not a3,a4,a2 are_collinear & not a4,a1,a2 are_collinear & not a4,a2,a1 are_collinear & not a4,a1,a3 are_collinear & not a4,a3,a1 are_collinear & not a4,a2,a3 are_collinear & not a4,a3,a2 are_collinear )

for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds

( not a1,a2,a3 are_collinear & not a1,a3,a2 are_collinear & not a1,a2,a4 are_collinear & not a1,a4,a2 are_collinear & not a1,a3,a4 are_collinear & not a1,a4,a3 are_collinear & not a2,a1,a3 are_collinear & not a2,a3,a1 are_collinear & not a2,a1,a4 are_collinear & not a2,a4,a1 are_collinear & not a2,a3,a4 are_collinear & not a2,a4,a3 are_collinear & not a3,a1,a2 are_collinear & not a3,a2,a1 are_collinear & not a3,a1,a4 are_collinear & not a3,a4,a1 are_collinear & not a3,a2,a4 are_collinear & not a3,a4,a2 are_collinear & not a4,a1,a2 are_collinear & not a4,a2,a1 are_collinear & not a4,a1,a3 are_collinear & not a4,a3,a1 are_collinear & not a4,a2,a3 are_collinear & not a4,a3,a2 are_collinear )

proof end;

theorem Th39: :: SEMI_AF1:39

for SAS being Semi_Affine_Space

for a, b, c, d, x being Element of SAS holds

( not parallelogram a,b,c,d or not a,b,x are_collinear or not c,d,x are_collinear )

for a, b, c, d, x being Element of SAS holds

( not parallelogram a,b,c,d or not a,b,x are_collinear or not c,d,x are_collinear )

proof end;

theorem :: SEMI_AF1:40

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram a,c,b,d by Th38;

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram a,c,b,d by Th38;

theorem :: SEMI_AF1:41

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram c,d,a,b by Th6, Th38;

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram c,d,a,b by Th6, Th38;

theorem :: SEMI_AF1:42

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram b,a,d,c by Th6, Th38;

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

parallelogram b,a,d,c by Th6, Th38;

theorem Th43: :: SEMI_AF1:43

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) by Th38, Th6;

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) by Th38, Th6;

theorem Th44: :: SEMI_AF1:44

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st not a,b,c are_collinear holds

ex d being Element of SAS st parallelogram a,b,c,d

for a, b, c being Element of SAS st not a,b,c are_collinear holds

ex d being Element of SAS st parallelogram a,b,c,d

proof end;

theorem Th45: :: SEMI_AF1:45

for SAS being Semi_Affine_Space

for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds

d1 = d2

for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds

d1 = d2

proof end;

theorem Th46: :: SEMI_AF1:46

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

not a,d // b,c

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

not a,d // b,c

proof end;

theorem Th47: :: SEMI_AF1:47

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

not parallelogram a,b,d,c

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

not parallelogram a,b,d,c

proof end;

theorem Th48: :: SEMI_AF1:48

for SAS being Semi_Affine_Space

for a, b being Element of SAS st a <> b holds

ex c being Element of SAS st

( a,b,c are_collinear & c <> a & c <> b )

for a, b being Element of SAS st a <> b holds

ex c being Element of SAS st

( a,b,c are_collinear & c <> a & c <> b )

proof end;

theorem Th49: :: SEMI_AF1:49

for SAS being Semi_Affine_Space

for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

b,c // b9,c9

for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

b,c // b9,c9

proof end;

theorem Th50: :: SEMI_AF1:50

for SAS being Semi_Affine_Space

for a, a9, b, b9, c, c9 being Element of SAS st not b,b9,c are_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

parallelogram b,b9,c,c9

for a, a9, b, b9, c, c9 being Element of SAS st not b,b9,c are_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

parallelogram b,b9,c,c9

proof end;

theorem Th51: :: SEMI_AF1:51

for SAS being Semi_Affine_Space

for a, a9, b, b9, c, c9 being Element of SAS st a,b,c are_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

parallelogram b,b9,c,c9

for a, a9, b, b9, c, c9 being Element of SAS st a,b,c are_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds

parallelogram b,b9,c,c9

proof end;

theorem Th52: :: SEMI_AF1:52

for SAS being Semi_Affine_Space

for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 holds

c,d // c9,d9

for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 holds

c,d // c9,d9

proof end;

Lm1: for SAS being Semi_Affine_Space

for a, b being Element of SAS st a <> b holds

ex c, d being Element of SAS st parallelogram a,b,c,d

proof end;

theorem :: SEMI_AF1:53

for SAS being Semi_Affine_Space

for a, d being Element of SAS st a <> d holds

ex b, c being Element of SAS st parallelogram a,b,c,d

for a, d being Element of SAS st a <> d holds

ex b, c being Element of SAS st parallelogram a,b,c,d

proof end;

::

:: CONGRUENCE

::

:: CONGRUENCE

::

definition

let SAS be Semi_Affine_Space;

let a, b, r, s be Element of SAS;

end;
let a, b, r, s be Element of SAS;

pred congr a,b,r,s means :: SEMI_AF1:def 4

( ( a = b & r = s ) or ex p, q being Element of SAS st

( parallelogram p,q,a,b & parallelogram p,q,r,s ) );

( ( a = b & r = s ) or ex p, q being Element of SAS st

( parallelogram p,q,a,b & parallelogram p,q,r,s ) );

:: deftheorem defines congr SEMI_AF1:def 4 :

for SAS being Semi_Affine_Space

for a, b, r, s being Element of SAS holds

( congr a,b,r,s iff ( ( a = b & r = s ) or ex p, q being Element of SAS st

( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) );

for SAS being Semi_Affine_Space

for a, b, r, s being Element of SAS holds

( congr a,b,r,s iff ( ( a = b & r = s ) or ex p, q being Element of SAS st

( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) );

theorem Th54: :: SEMI_AF1:54

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st congr a,a,b,c holds

b = c by Th36;

for a, b, c being Element of SAS st congr a,a,b,c holds

b = c by Th36;

theorem Th55: :: SEMI_AF1:55

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS st congr a,b,c,c holds

a = b by Th36;

for a, b, c being Element of SAS st congr a,b,c,c holds

a = b by Th36;

theorem Th57: :: SEMI_AF1:57

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

a,b // c,d

for a, b, c, d being Element of SAS st congr a,b,c,d holds

a,b // c,d

proof end;

theorem Th58: :: SEMI_AF1:58

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

a,c // b,d

for a, b, c, d being Element of SAS st congr a,b,c,d holds

a,c // b,d

proof end;

theorem Th59: :: SEMI_AF1:59

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d & not a,b,c are_collinear holds

parallelogram a,b,c,d by Th57, Th58;

for a, b, c, d being Element of SAS st congr a,b,c,d & not a,b,c are_collinear holds

parallelogram a,b,c,d by Th57, Th58;

theorem Th60: :: SEMI_AF1:60

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

congr a,b,c,d

for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds

congr a,b,c,d

proof end;

theorem Th61: :: SEMI_AF1:61

for SAS being Semi_Affine_Space

for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c are_collinear & parallelogram r,s,a,b holds

parallelogram r,s,c,d

for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c are_collinear & parallelogram r,s,a,b holds

parallelogram r,s,c,d

proof end;

theorem Th62: :: SEMI_AF1:62

for SAS being Semi_Affine_Space

for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds

x = y

for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds

x = y

proof end;

theorem Th63: :: SEMI_AF1:63

for SAS being Semi_Affine_Space

for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d

for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d

proof end;

theorem Th65: :: SEMI_AF1:65

for SAS being Semi_Affine_Space

for a, b, c, d, r, s being Element of SAS st congr r,s,a,b & congr r,s,c,d holds

congr a,b,c,d

for a, b, c, d, r, s being Element of SAS st congr r,s,a,b & congr r,s,c,d holds

congr a,b,c,d

proof end;

theorem :: SEMI_AF1:66

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr c,d,a,b ;

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr c,d,a,b ;

theorem Th67: :: SEMI_AF1:67

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr b,a,d,c

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr b,a,d,c

proof end;

theorem Th68: :: SEMI_AF1:68

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr a,c,b,d

for a, b, c, d being Element of SAS st congr a,b,c,d holds

congr a,c,b,d

proof end;

theorem Th69: :: SEMI_AF1:69

for SAS being Semi_Affine_Space

for a, b, c, d being Element of SAS st congr a,b,c,d holds

( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a )

for a, b, c, d being Element of SAS st congr a,b,c,d holds

( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a )

proof end;

theorem Th70: :: SEMI_AF1:70

for SAS being Semi_Affine_Space

for a, b, c, p, q, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds

congr a,c,p,s

for a, b, c, p, q, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds

congr a,c,p,s

proof end;

theorem Th71: :: SEMI_AF1:71

for SAS being Semi_Affine_Space

for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds

congr b,c,r,q

for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds

congr b,c,r,q

proof end;

theorem :: SEMI_AF1:72

theorem Th73: :: SEMI_AF1:73

for SAS being Semi_Affine_Space

for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds

b,c // q,r

for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds

b,c // q,r

proof end;

theorem :: SEMI_AF1:74

::

:: A VECTOR' GROUP

::

:: A VECTOR' GROUP

::

definition

let SAS be Semi_Affine_Space;

let a, b, o be Element of SAS;

correctness

existence

ex b_{1} being Element of SAS st congr o,a,b,b_{1};

uniqueness

for b_{1}, b_{2} being Element of SAS st congr o,a,b,b_{1} & congr o,a,b,b_{2} holds

b_{1} = b_{2};

by Th62, Th63;

end;
let a, b, o be Element of SAS;

correctness

existence

ex b

uniqueness

for b

b

by Th62, Th63;

:: deftheorem Def5 defines sum SEMI_AF1:def 5 :

for SAS being Semi_Affine_Space

for a, b, o, b_{5} being Element of SAS holds

( b_{5} = sum (a,b,o) iff congr o,a,b,b_{5} );

for SAS being Semi_Affine_Space

for a, b, o, b

( b

definition

let SAS be Semi_Affine_Space;

let a, o be Element of SAS;

existence

ex b_{1} being Element of SAS st sum (a,b_{1},o) = o

for b_{1}, b_{2} being Element of SAS st sum (a,b_{1},o) = o & sum (a,b_{2},o) = o holds

b_{1} = b_{2}

end;
let a, o be Element of SAS;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines opposite SEMI_AF1:def 6 :

for SAS being Semi_Affine_Space

for a, o, b_{4} being Element of SAS holds

( b_{4} = opposite (a,o) iff sum (a,b_{4},o) = o );

for SAS being Semi_Affine_Space

for a, o, b

( b

definition

let SAS be Semi_Affine_Space;

let a, b, o be Element of SAS;

correctness

coherence

sum (a,(opposite (b,o)),o) is Element of SAS;

;

end;
let a, b, o be Element of SAS;

correctness

coherence

sum (a,(opposite (b,o)),o) is Element of SAS;

;

:: deftheorem defines diff SEMI_AF1:def 7 :

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS holds diff (a,b,o) = sum (a,(opposite (b,o)),o);

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS holds diff (a,b,o) = sum (a,(opposite (b,o)),o);

theorem :: SEMI_AF1:76

for SAS being Semi_Affine_Space

for a, o being Element of SAS ex x being Element of SAS st sum (a,x,o) = o

for a, o being Element of SAS ex x being Element of SAS st sum (a,x,o) = o

proof end;

theorem :: SEMI_AF1:77

for SAS being Semi_Affine_Space

for a, b, c, o being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o)

for a, b, c, o being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o)

proof end;

theorem :: SEMI_AF1:80

for SAS being Semi_Affine_Space

for a, o, x, y being Element of SAS st sum (a,x,o) = sum (a,y,o) holds

x = y

for a, o, x, y being Element of SAS st sum (a,x,o) = sum (a,y,o) holds

x = y

proof end;

theorem Th82: :: SEMI_AF1:82

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS st opposite (a,o) = opposite (b,o) holds

a = b

for a, b, o being Element of SAS st opposite (a,o) = opposite (b,o) holds

a = b

proof end;

theorem :: SEMI_AF1:83

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS holds a,b // opposite (a,o), opposite (b,o)

for a, b, o being Element of SAS holds a,b // opposite (a,o), opposite (b,o)

proof end;

theorem Th85: :: SEMI_AF1:85

for SAS being Semi_Affine_Space

for o, p, q, r being Element of SAS holds p,q // sum (p,r,o), sum (q,r,o)

for o, p, q, r being Element of SAS holds p,q // sum (p,r,o), sum (q,r,o)

proof end;

theorem :: SEMI_AF1:86

for SAS being Semi_Affine_Space

for o, p, q, r, s being Element of SAS st p,q // r,s holds

p,q // sum (p,r,o), sum (q,s,o)

for o, p, q, r, s being Element of SAS st p,q // r,s holds

p,q // sum (p,r,o), sum (q,s,o)

proof end;

theorem Th87: :: SEMI_AF1:87

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS holds

( diff (a,b,o) = o iff a = b )

for a, b, o being Element of SAS holds

( diff (a,b,o) = o iff a = b )

proof end;

theorem :: SEMI_AF1:89

for SAS being Semi_Affine_Space

for a, b, c, d, o being Element of SAS holds

( o, diff (b,a,o), diff (d,c,o) are_collinear iff a,b // c,d )

for a, b, c, d, o being Element of SAS holds

( o, diff (b,a,o), diff (d,c,o) are_collinear iff a,b // c,d )

proof end;

::

:: A TRAPEZIUM RELATION

::

:: A TRAPEZIUM RELATION

::

definition

let SAS be Semi_Affine_Space;

let a, b, c, d, o be Element of SAS;

end;
let a, b, c, d, o be Element of SAS;

pred trap a,b,c,d,o means :: SEMI_AF1:def 8

( not o,a,c are_collinear & o,a,b are_collinear & o,c,d are_collinear & a,c // b,d );

( not o,a,c are_collinear & o,a,b are_collinear & o,c,d are_collinear & a,c // b,d );

:: deftheorem defines trap SEMI_AF1:def 8 :

for SAS being Semi_Affine_Space

for a, b, c, d, o being Element of SAS holds

( trap a,b,c,d,o iff ( not o,a,c are_collinear & o,a,b are_collinear & o,c,d are_collinear & a,c // b,d ) );

for SAS being Semi_Affine_Space

for a, b, c, d, o being Element of SAS holds

( trap a,b,c,d,o iff ( not o,a,c are_collinear & o,a,b are_collinear & o,c,d are_collinear & a,c // b,d ) );

definition

let SAS be Semi_Affine_Space;

let o, p be Element of SAS;

end;
let o, p be Element of SAS;

pred qtrap o,p means :: SEMI_AF1:def 9

for b, c being Element of SAS ex d being Element of SAS st

( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) );

for b, c being Element of SAS ex d being Element of SAS st

( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) );

:: deftheorem defines qtrap SEMI_AF1:def 9 :

for SAS being Semi_Affine_Space

for o, p being Element of SAS holds

( qtrap o,p iff for b, c being Element of SAS ex d being Element of SAS st

( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) ) );

for SAS being Semi_Affine_Space

for o, p being Element of SAS holds

( qtrap o,p iff for b, c being Element of SAS ex d being Element of SAS st

( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) ) );

theorem :: SEMI_AF1:91

theorem :: SEMI_AF1:92

for SAS being Semi_Affine_Space

for a, b, o being Element of SAS st not o,a,b are_collinear holds

trap a,o,b,o,o by Def1, Th24;

for a, b, o being Element of SAS st not o,a,b are_collinear holds

trap a,o,b,o,o by Def1, Th24;

theorem Th95: :: SEMI_AF1:95

for SAS being Semi_Affine_Space

for a, b, c, d, o being Element of SAS st o <> b & trap a,b,c,d,o holds

not o,b,d are_collinear

for a, b, c, d, o being Element of SAS st o <> b & trap a,b,c,d,o holds

not o,b,d are_collinear

proof end;

theorem :: SEMI_AF1:96

theorem :: SEMI_AF1:97

theorem Th98: :: SEMI_AF1:98

for SAS being Semi_Affine_Space

for a, b, c, o, p, q, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o holds

b,c // q,r

for a, b, c, o, p, q, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o holds

b,c // q,r

proof end;

theorem Th99: :: SEMI_AF1:99

for SAS being Semi_Affine_Space

for a, b, c, o, p, q, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c are_collinear holds

trap b,q,c,r,o by Th98;

for a, b, c, o, p, q, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c are_collinear holds

trap b,q,c,r,o by Th98;

theorem :: SEMI_AF1:100

for SAS being Semi_Affine_Space

for a, b, c, d, o, p, q, r, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds

c,d // r,s

for a, b, c, d, o, p, q, r, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds

c,d // r,s

proof end;

theorem Th101: :: SEMI_AF1:101

for SAS being Semi_Affine_Space

for o, a being Element of SAS ex p being Element of SAS st

( o,a,p are_collinear & qtrap o,p )

for o, a being Element of SAS ex p being Element of SAS st

( o,a,p are_collinear & qtrap o,p )

proof end;

theorem :: SEMI_AF1:104

for SAS being Semi_Affine_Space

for o, p being Element of SAS st qtrap o,p holds

ex q being Element of SAS st

( not o,p,q are_collinear & qtrap o,q )

for o, p being Element of SAS st qtrap o,p holds

ex q being Element of SAS st

( not o,p,q are_collinear & qtrap o,q )

proof end;

theorem :: SEMI_AF1:105

for SAS being Semi_Affine_Space

for b, c, o, p being Element of SAS st not o,p,c are_collinear & o,p,b are_collinear & qtrap o,p holds

ex d being Element of SAS st trap p,b,c,d,o

for b, c, o, p being Element of SAS st not o,p,c are_collinear & o,p,b are_collinear & qtrap o,p holds

ex d being Element of SAS st trap p,b,c,d,o

proof end;

:: BASIC FACTS ABOUT COLLINEARITY RELATION

::