begin
definition
let IT be non
empty AffinStruct ;
attr IT is
Semi_Affine_Space-like means :
Def1:
( ( for
a,
b being
Element of holds
a,
b // b,
a ) & ( for
a,
b,
c being
Element of holds
a,
b // c,
c ) & ( for
a,
b,
p,
q,
r,
s being
Element of st
a <> b &
a,
b // p,
q &
a,
b // r,
s holds
p,
q // r,
s ) & ( for
a,
b,
c being
Element of st
a,
b // a,
c holds
b,
a // b,
c ) & not for
a,
b,
c being
Element of holds
a,
b // a,
c & ( for
a,
b,
p being
Element of ex
q being
Element of st
(
a,
b // p,
q &
a,
p // b,
q ) ) & ( for
o,
a being
Element of ex
p being
Element of st
for
b,
c being
Element of holds
(
o,
a // o,
p & ex
d being
Element of st
(
o,
p // o,
b implies (
o,
c // o,
d &
p,
c // b,
d ) ) ) ) & ( for
o,
a,
a',
b,
b',
c,
c' being
Element of st not
o,
a // o,
b & not
o,
a // o,
c &
o,
a // o,
a' &
o,
b // o,
b' &
o,
c // o,
c' &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
a',
b,
b',
c,
c' being
Element of st not
a,
a' // a,
b & not
a,
a' // a,
c &
a,
a' // b,
b' &
a,
a' // c,
c' &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a1,
a2,
a3,
b1,
b2,
b3 being
Element of 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 st not
a,
b // a,
c &
a,
b // c,
d &
a,
c // b,
d holds
not
a,
d // b,
c ) );
end;
:: 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 holds
a,
b // b,
a ) & ( for
a,
b,
c being
Element of holds
a,
b // c,
c ) & ( for
a,
b,
p,
q,
r,
s being
Element of st
a <> b &
a,
b // p,
q &
a,
b // r,
s holds
p,
q // r,
s ) & ( for
a,
b,
c being
Element of st
a,
b // a,
c holds
b,
a // b,
c ) & not for
a,
b,
c being
Element of holds
a,
b // a,
c & ( for
a,
b,
p being
Element of ex
q being
Element of st
(
a,
b // p,
q &
a,
p // b,
q ) ) & ( for
o,
a being
Element of ex
p being
Element of st
for
b,
c being
Element of holds
(
o,
a // o,
p & ex
d being
Element of st
(
o,
p // o,
b implies (
o,
c // o,
d &
p,
c // b,
d ) ) ) ) & ( for
o,
a,
a',
b,
b',
c,
c' being
Element of st not
o,
a // o,
b & not
o,
a // o,
c &
o,
a // o,
a' &
o,
b // o,
b' &
o,
c // o,
c' &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
a',
b,
b',
c,
c' being
Element of st not
a,
a' // a,
b & not
a,
a' // a,
c &
a,
a' // b,
b' &
a,
a' // c,
c' &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a1,
a2,
a3,
b1,
b2,
b3 being
Element of 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 st not
a,
b // a,
c &
a,
b // c,
d &
a,
c // b,
d holds
not
a,
d // b,
c ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of 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 )
theorem Th18:
for
SAS being
Semi_Affine_Space for
a,
b,
c being
Element of 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 )
theorem
canceled;
theorem Th20:
for
SAS being
Semi_Affine_Space for
a,
b,
p,
q,
r,
s being
Element of st
a <> b &
p,
q // a,
b &
a,
b // r,
s holds
p,
q // r,
s
theorem
theorem
theorem
for
SAS being
Semi_Affine_Space for
a,
b,
x,
c being
Element of st
a,
b // a,
x &
b,
c // b,
x &
c,
a // c,
x holds
a,
b // a,
c
theorem
canceled;
theorem Th25:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
p,
q being
Element of st not
a,
b // a,
c &
p <> q &
p,
q // p,
a &
p,
q // p,
b holds
not
p,
q // p,
c
theorem Th26:
theorem
canceled;
theorem Th28:
for
SAS being
Semi_Affine_Space for
a,
b,
c being
Element of 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 )
theorem Th29:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
p,
q,
r,
s being
Element of st not
a,
b // c,
d &
a,
b // p,
q &
c,
d // r,
s &
p <> q &
r <> s holds
not
p,
q // r,
s
theorem Th30:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
p,
q,
r being
Element of 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
theorem Th31:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
p,
r being
Element of st not
a,
b // a,
c &
a,
c // p,
r &
b,
c // p,
r holds
p = r
theorem Th32:
theorem Th33:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
p,
q,
r1,
r2 being
Element of 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
theorem
theorem
:: deftheorem Def2 defines is_collinear SEMI_AF1:def 2 :
theorem
canceled;
theorem Th37:
for
SAS being
Semi_Affine_Space for
a1,
a2,
a3 being
Element of st
a1,
a2,
a3 is_collinear holds
(
a1,
a3,
a2 is_collinear &
a2,
a1,
a3 is_collinear &
a2,
a3,
a1 is_collinear &
a3,
a1,
a2 is_collinear &
a3,
a2,
a1 is_collinear )
theorem
canceled;
theorem Th39:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
p,
q,
r being
Element of st not
a,
b,
c is_collinear &
a,
b // p,
q &
a,
c // p,
r &
p <> q &
p <> r holds
not
p,
q,
r is_collinear
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
x being
Element of st not
a,
b,
c is_collinear &
a,
b // c,
d &
c <> d &
c,
d,
x is_collinear holds
not
a,
b,
x is_collinear
theorem
theorem
for
SAS being
Semi_Affine_Space for
o,
a,
b,
a',
b' being
Element of st
o <> a &
o <> b &
o,
a,
b is_collinear &
o,
a,
a' is_collinear &
o,
b,
b' is_collinear holds
a,
b // a',
b'
theorem
canceled;
theorem
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
p1,
p2 being
Element of st not
a,
b // c,
d &
a,
b,
p1 is_collinear &
a,
b,
p2 is_collinear &
c,
d,
p1 is_collinear &
c,
d,
p2 is_collinear holds
p1 = p2
theorem Th49:
theorem Th50:
theorem Th51:
for
SAS being
Semi_Affine_Space for
o,
a,
c,
b,
d1,
d2 being
Element of st not
o,
a,
c is_collinear &
o,
a,
b is_collinear &
o,
c,
d1 is_collinear &
o,
c,
d2 is_collinear &
a,
c // b,
d1 &
a,
c // b,
d2 holds
d1 = d2
theorem
definition
let SAS be
Semi_Affine_Space;
let a,
b,
c,
d be
Element of ;
pred parallelogram a,
b,
c,
d means :
Def3:
( not
a,
b,
c is_collinear &
a,
b // c,
d &
a,
c // b,
d );
end;
:: deftheorem Def3 defines parallelogram SEMI_AF1:def 3 :
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of holds
(
parallelogram a,
b,
c,
d iff ( not
a,
b,
c is_collinear &
a,
b // c,
d &
a,
c // b,
d ) );
theorem
canceled;
theorem Th54:
theorem Th55:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of st
parallelogram a,
b,
c,
d holds
( not
a,
b,
c is_collinear & not
b,
a,
d is_collinear & not
c,
d,
a is_collinear & not
d,
c,
b is_collinear )
theorem Th56:
for
SAS being
Semi_Affine_Space for
a1,
a2,
a3,
a4 being
Element of st
parallelogram a1,
a2,
a3,
a4 holds
( not
a1,
a2,
a3 is_collinear & not
a1,
a3,
a2 is_collinear & not
a1,
a2,
a4 is_collinear & not
a1,
a4,
a2 is_collinear & not
a1,
a3,
a4 is_collinear & not
a1,
a4,
a3 is_collinear & not
a2,
a1,
a3 is_collinear & not
a2,
a3,
a1 is_collinear & not
a2,
a1,
a4 is_collinear & not
a2,
a4,
a1 is_collinear & not
a2,
a3,
a4 is_collinear & not
a2,
a4,
a3 is_collinear & not
a3,
a1,
a2 is_collinear & not
a3,
a2,
a1 is_collinear & not
a3,
a1,
a4 is_collinear & not
a3,
a4,
a1 is_collinear & not
a3,
a2,
a4 is_collinear & not
a3,
a4,
a2 is_collinear & not
a4,
a1,
a2 is_collinear & not
a4,
a2,
a1 is_collinear & not
a4,
a1,
a3 is_collinear & not
a4,
a3,
a1 is_collinear & not
a4,
a2,
a3 is_collinear & not
a4,
a3,
a2 is_collinear )
theorem Th57:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
x being
Element of holds
( not
parallelogram a,
b,
c,
d or not
a,
b,
x is_collinear or not
c,
d,
x is_collinear )
theorem
theorem
theorem
theorem Th61:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of 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 )
theorem Th62:
theorem Th63:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d1,
d2 being
Element of st
parallelogram a,
b,
c,
d1 &
parallelogram a,
b,
c,
d2 holds
d1 = d2
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
for
SAS being
Semi_Affine_Space for
a,
a',
b,
b',
c,
c' being
Element of st
parallelogram a,
a',
b,
b' &
parallelogram a,
a',
c,
c' holds
b,
c // b',
c'
theorem Th68:
for
SAS being
Semi_Affine_Space for
b,
b',
c,
a,
a',
c' being
Element of st not
b,
b',
c is_collinear &
parallelogram a,
a',
b,
b' &
parallelogram a,
a',
c,
c' holds
parallelogram b,
b',
c,
c'
theorem Th69:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b,
c is_collinear &
b <> c &
parallelogram a,
a',
b,
b' &
parallelogram a,
a',
c,
c' holds
parallelogram b,
b',
c,
c'
theorem Th70:
for
SAS being
Semi_Affine_Space for
a,
a',
b,
b',
c,
c',
d,
d' being
Element of st
parallelogram a,
a',
b,
b' &
parallelogram a,
a',
c,
c' &
parallelogram b,
b',
d,
d' holds
c,
d // c',
d'
Lm1:
for SAS being Semi_Affine_Space
for a, b being Element of st a <> b holds
ex c, d being Element of st parallelogram a,b,c,d
theorem
definition
let SAS be
Semi_Affine_Space;
let a,
b,
r,
s be
Element of ;
pred congr a,
b,
r,
s means :
Def4:
( (
a = b &
r = s ) or ex
p,
q being
Element of st
(
parallelogram p,
q,
a,
b &
parallelogram p,
q,
r,
s ) );
end;
:: deftheorem Def4 defines congr SEMI_AF1:def 4 :
for
SAS being
Semi_Affine_Space for
a,
b,
r,
s being
Element of holds
(
congr a,
b,
r,
s iff ( (
a = b &
r = s ) or ex
p,
q being
Element of st
(
parallelogram p,
q,
a,
b &
parallelogram p,
q,
r,
s ) ) );
theorem
canceled;
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of st
congr a,
b,
c,
d & not
a,
b,
c is_collinear holds
parallelogram a,
b,
c,
d
theorem Th79:
theorem Th80:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
r,
s being
Element of st
congr a,
b,
c,
d &
a,
b,
c is_collinear &
parallelogram r,
s,
a,
b holds
parallelogram r,
s,
c,
d
theorem Th81:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
x,
y being
Element of st
congr a,
b,
c,
x &
congr a,
b,
c,
y holds
x = y
theorem Th82:
theorem
canceled;
theorem Th84:
theorem Th85:
for
SAS being
Semi_Affine_Space for
r,
s,
a,
b,
c,
d being
Element of st
congr r,
s,
a,
b &
congr r,
s,
c,
d holds
congr a,
b,
c,
d
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d being
Element of 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 )
theorem Th90:
for
SAS being
Semi_Affine_Space for
a,
b,
p,
q,
c,
s being
Element of st
congr a,
b,
p,
q &
congr b,
c,
q,
s holds
congr a,
c,
p,
s
theorem Th91:
for
SAS being
Semi_Affine_Space for
b,
a,
p,
q,
c,
r being
Element of st
congr b,
a,
p,
q &
congr c,
a,
p,
r holds
congr b,
c,
r,
q
theorem
for
SAS being
Semi_Affine_Space for
a,
o,
p,
b,
q being
Element of st
congr a,
o,
o,
p &
congr b,
o,
o,
q holds
congr a,
b,
q,
p by Th91;
theorem Th93:
for
SAS being
Semi_Affine_Space for
b,
a,
p,
q,
c,
r being
Element of st
congr b,
a,
p,
q &
congr c,
a,
p,
r holds
b,
c // q,
r
theorem
for
SAS being
Semi_Affine_Space for
a,
o,
p,
b,
q being
Element of st
congr a,
o,
o,
p &
congr b,
o,
o,
q holds
a,
b // p,
q by Th93;
definition
let SAS be
Semi_Affine_Space;
let a,
b,
o be
Element of ;
func sum a,
b,
o -> Element of
means :
Def5:
congr o,
a,
b,
it;
correctness
existence
ex b1 being Element of st congr o,a,b,b1;
uniqueness
for b1, b2 being Element of st congr o,a,b,b1 & congr o,a,b,b2 holds
b1 = b2;
by Th81, Th82;
end;
:: deftheorem Def5 defines sum SEMI_AF1:def 5 :
definition
let SAS be
Semi_Affine_Space;
let a,
o be
Element of ;
func opposite a,
o -> Element of
means :
Def6:
sum a,
it,
o = o;
existence
ex b1 being Element of st sum a,b1,o = o
uniqueness
for b1, b2 being Element of st sum a,b1,o = o & sum a,b2,o = o holds
b1 = b2
end;
:: deftheorem Def6 defines opposite SEMI_AF1:def 6 :
definition
let SAS be
Semi_Affine_Space;
let a,
b,
o be
Element of ;
func diff a,
b,
o -> Element of
equals
sum a,
(opposite b,o),
o;
correctness
coherence
sum a,(opposite b,o),o is Element of ;
;
end;
:: deftheorem defines diff SEMI_AF1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th99:
theorem
theorem
for
SAS being
Semi_Affine_Space for
a,
b,
o,
c being
Element of holds
sum (sum a,b,o),
c,
o = sum a,
(sum b,c,o),
o
theorem Th102:
theorem
theorem
theorem
canceled;
theorem Th106:
theorem Th107:
theorem
theorem
theorem Th110:
theorem
for
SAS being
Semi_Affine_Space for
p,
q,
r,
s,
o being
Element of st
p,
q // r,
s holds
p,
q // sum p,
r,
o,
sum q,
s,
o
theorem
canceled;
theorem Th113:
theorem Th114:
theorem
for
SAS being
Semi_Affine_Space for
o,
b,
a,
d,
c being
Element of holds
(
o,
diff b,
a,
o,
diff d,
c,
o is_collinear iff
a,
b // c,
d )
definition
let SAS be
Semi_Affine_Space;
let a,
b,
c,
d,
o be
Element of ;
pred trap a,
b,
c,
d,
o means :
Def8:
( not
o,
a,
c is_collinear &
o,
a,
b is_collinear &
o,
c,
d is_collinear &
a,
c // b,
d );
end;
:: deftheorem Def8 defines trap SEMI_AF1:def 8 :
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
o being
Element of holds
(
trap a,
b,
c,
d,
o iff ( not
o,
a,
c is_collinear &
o,
a,
b is_collinear &
o,
c,
d is_collinear &
a,
c // b,
d ) );
:: deftheorem Def9 defines qtrap SEMI_AF1:def 9 :
theorem
canceled;
theorem
canceled;
theorem Th118:
theorem
for
SAS being
Semi_Affine_Space for
a,
b,
c,
x,
o,
y being
Element of st
trap a,
b,
c,
x,
o &
trap a,
b,
c,
y,
o holds
x = y
theorem
theorem Th121:
for
SAS being
Semi_Affine_Space for
a,
b,
c,
d,
o being
Element of st
trap a,
b,
c,
d,
o holds
trap c,
d,
a,
b,
o
theorem Th122:
theorem Th123:
for
SAS being
Semi_Affine_Space for
o,
b,
a,
c,
d being
Element of st
o <> b &
trap a,
b,
c,
d,
o holds
not
o,
b,
d is_collinear
theorem
for
SAS being
Semi_Affine_Space for
o,
b,
a,
c,
d being
Element of st
o <> b &
trap a,
b,
c,
d,
o holds
trap b,
a,
d,
c,
o
theorem
theorem Th126:
for
SAS being
Semi_Affine_Space for
a,
p,
b,
q,
o,
c,
r being
Element of st
trap a,
p,
b,
q,
o &
trap a,
p,
c,
r,
o holds
b,
c // q,
r
theorem Th127:
for
SAS being
Semi_Affine_Space for
a,
p,
b,
q,
o,
c,
r being
Element of st
trap a,
p,
b,
q,
o &
trap a,
p,
c,
r,
o & not
o,
b,
c is_collinear holds
trap b,
q,
c,
r,
o
theorem
for
SAS being
Semi_Affine_Space for
a,
p,
b,
q,
o,
c,
r,
d,
s being
Element of st
trap a,
p,
b,
q,
o &
trap a,
p,
c,
r,
o &
trap b,
q,
d,
s,
o holds
c,
d // r,
s
theorem Th129:
theorem Th130:
theorem Th131:
theorem
theorem
for
SAS being
Semi_Affine_Space for
o,
p,
c,
b being
Element of st not
o,
p,
c is_collinear &
o,
p,
b is_collinear &
qtrap o,
p holds
ex
d being
Element of st
trap p,
b,
c,
d,
o