:: DIRAF semantic presentation

definition

let X be non empty set ;
let R be Relation of [:X,X:];
func lambda R -> Relation of [:X,X:] means :Def1: :: DIRAF:def 1
for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in it iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines lambda DIRAF:def 1 :

definition

let S be non empty AffinStruct ;
func Lambda S -> strict AffinStruct equals :: DIRAF:def 2
AffinStruct(# the carrier of S,(lambda the CONGR of S) #);
correctness ;

end;

:: deftheorem defines Lambda DIRAF:def 2 :

registration

let S be non empty AffinStruct ;
cluster Lambda S -> non empty strict ;
coherence

proof end;

end;

theorem :: DIRAF:1

canceled;

theorem :: DIRAF:2

canceled;

theorem :: DIRAF:3

canceled;

theorem Th4: :: DIRAF:4

for S being OAffinSpace
for x, y being Element of S holds x,y // x,y

proof end;

Lm1: for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
z,t // x,y

proof end;

theorem Th5: :: DIRAF:5

for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
( y,x // t,z & z,t // x,y & t,z // y,x )

proof end;

theorem Th6: :: DIRAF:6

for S being OAffinSpace
for z, t, x, y, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds
x,y // u,w

proof end;

theorem Th7: :: DIRAF:7

for S being OAffinSpace
for x, y, z being Element of S holds
( x,x // y,z & y,z // x,x )

proof end;

theorem Th8: :: DIRAF:8

for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t & x,y // t,z & not x = y holds
z = t

proof end;

theorem Th9: :: DIRAF:9

for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )

proof end;

definition

let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred Mid a,b,c means :Def3: :: DIRAF:def 3
a,b // b,c;

end;

:: deftheorem Def3 defines Mid DIRAF:def 3 :

theorem :: DIRAF:10

canceled;

theorem Th11: :: DIRAF:11

for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) )

proof end;

theorem Th12: :: DIRAF:12

for S being OAffinSpace
for a, b being Element of S st Mid a,b,a holds
a = b

proof end;

theorem :: DIRAF:13

for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
Mid c,b,a

proof end;

theorem :: DIRAF:14

for S being OAffinSpace
for x, y being Element of S holds
( Mid x,x,y & Mid x,y,y )

proof end;

theorem :: DIRAF:15

for S being OAffinSpace
for a, b, c, d being Element of S st Mid a,b,c & Mid a,c,d holds
Mid b,c,d

proof end;

theorem :: DIRAF:16

for S being OAffinSpace
for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d

proof end;

theorem Th17: :: DIRAF:17

for S being OAffinSpace
for x, y being Element of S ex z being Element of S st
( Mid x,y,z & y <> z )

proof end;

theorem :: DIRAF:18

for S being OAffinSpace
for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds
x = y

proof end;

theorem :: DIRAF:19

for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid y,z,t holds
Mid y,t,z

proof end;

theorem :: DIRAF:20

for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid x,z,t holds
Mid x,t,z

proof end;

theorem :: DIRAF:21

for S being OAffinSpace
for x, y, t, z being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds
Mid x,z,y

proof end;

definition

let S be non empty AffinStruct ;
let a, b, c, d be Element of S;
pred a,b '||' c,d means :Def4: :: DIRAF:def 4
( a,b // c,d or a,b // d,c );

end;

:: deftheorem Def4 defines '||' DIRAF:def 4 :

theorem :: DIRAF:22

canceled;

theorem :: DIRAF:23

for S being OAffinSpace
for a, b, c, d being Element of S holds
( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )

proof end;

theorem Th24: :: DIRAF:24

for S being OAffinSpace
for x, y being Element of S holds
( x,y '||' y,x & x,y '||' x,y )

proof end;

theorem Th25: :: DIRAF:25

for S being OAffinSpace
for x, y, z being Element of S holds
( x,y '||' z,z & z,z '||' x,y )

proof end;

Lm2: for S being OAffinSpace
for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds
z,t '||' u,w

proof end;

theorem Th26: :: DIRAF:26

for S being OAffinSpace
for x, y, z being Element of S st x,y '||' x,z holds
y,x '||' y,z

proof end;

theorem Th27: :: DIRAF:27

for S being OAffinSpace
for x, y, z, t being Element of S st x,y '||' z,t holds
( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )

proof end;

theorem Th28: :: DIRAF:28

for S being OAffinSpace
for a, b, x, y, z, t being Element of S st a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) holds
x,y '||' z,t

proof end;

theorem Th29: :: DIRAF:29

for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y '||' x,z

proof end;

theorem Th30: :: DIRAF:30

for S being OAffinSpace
for x, z, y being Element of S ex t being Element of S st
( x,z '||' y,t & y <> t )

proof end;

theorem Th31: :: DIRAF:31

for S being OAffinSpace
for x, y, z being Element of S ex t being Element of S st
( x,y '||' z,t & x,z '||' y,t )

proof end;

theorem Th32: :: DIRAF:32

for S being OAffinSpace
for z, x, t, y being Element of S st z,x '||' x,t & x <> z holds
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )

proof end;

definition

let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred LIN a,b,c means :Def5: :: DIRAF:def 5
a,b '||' a,c;

end;

:: deftheorem Def5 defines LIN DIRAF:def 5 :

notation

let S be non empty AffinStruct ;
let a, b, c be Element of S;
synonym a,b,c is_collinear for LIN a,b,c;

end;

theorem :: DIRAF:33

canceled;

theorem :: DIRAF:34

for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
a,b,c is_collinear

proof end;

theorem :: DIRAF:35

for S being OAffinSpace
for a, b, c being Element of S holds
( not a,b,c is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b )

proof end;

Lm3: for S being OAffinSpace
for x, y, z being Element of S st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear )

proof end;

theorem Th36: :: DIRAF:36

for S being OAffinSpace
for x, y, z being Element of S st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear )

proof end;

theorem Th37: :: DIRAF:37

for S being OAffinSpace
for x, y being Element of S holds
( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear )

proof end;

theorem Th38: :: DIRAF:38

for S being OAffinSpace
for x, y, z, t, u being Element of S st x <> y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear holds
z,t,u is_collinear

proof end;

theorem :: DIRAF:39

for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & x,y,z is_collinear & x,y '||' z,t holds
x,y,t is_collinear

proof end;

theorem :: DIRAF:40

for S being OAffinSpace
for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds
x,y '||' z,t

proof end;

theorem :: DIRAF:41

for S being OAffinSpace
for u, z, x, y, w being Element of S st u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear holds
x,y,w is_collinear

proof end;

theorem Th42: :: DIRAF:42

for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y,z is_collinear

proof end;

theorem :: DIRAF:43

for S being OAffinSpace
for x, y being Element of S st x <> y holds
ex z being Element of S st not x,y,z is_collinear

proof end;

theorem :: DIRAF:44

canceled;

theorem Th45: :: DIRAF:45

for S being OAffinSpace
for AS being non empty AffinStruct st AS = Lambda S holds
for a, b, c, d being Element of S
for a', b', c', d' being Element of AS st a = a' & b = b' & c = c' & d = d' holds
( a',b' // c',d' iff a,b '||' c,d )

proof end;

theorem Th46: :: DIRAF:46

for S being OAffinSpace
for AS being non empty AffinStruct st AS = Lambda S holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )

proof end;

definition

let IT be non empty AffinStruct ;
canceled;
attr IT is AffinSpace-like means :Def7: :: DIRAF:def 7
( ( for x, y, z, t, u, w being Element of IT holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds
ex u being Element of IT st
( y,x // x,u & y,z // t,u ) ) );

end;

:: deftheorem DIRAF:def 6 :

:: deftheorem Def7 defines AffinSpace-like DIRAF:def 7 :

registration

cluster non empty non trivial strict AffinSpace-like AffinStruct ;
existence

proof end;

end;

definition

mode AffinSpace is non empty non trivial AffinSpace-like AffinStruct ;

end;

theorem :: DIRAF:47

for AS being AffinSpace holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) by Def7, REALSET2:def 7;

theorem Th48: :: DIRAF:48

for S being OAffinSpace holds Lambda S is AffinSpace

proof end;

theorem :: DIRAF:49

for AS being non empty AffinStruct holds
( ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) iff AS is AffinSpace ) by Def7, REALSET2:def 7;

theorem Th50: :: DIRAF:50

for S being OAffinPlane
for x, y, z, t being Element of S st not x,y '||' z,t holds
ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u )

proof end;

theorem Th51: :: DIRAF:51

for AS being non empty AffinStruct
for S being OAffinPlane st AS = Lambda S holds
for x, y, z, t being Element of AS st not x,y // z,t holds
ex u being Element of AS st
( x,y // x,u & z,t // z,u )

proof end;

definition

let IT be non empty AffinStruct ;
attr IT is 2-dimensional means :Def8: :: DIRAF:def 8
for x, y, z, t being Element of IT st not x,y // z,t holds
ex u being Element of IT st
( x,y // x,u & z,t // z,u );

end;

:: deftheorem Def8 defines 2-dimensional DIRAF:def 8 :

registration

cluster strict 2-dimensional AffinStruct ;
existence

proof end;

end;

definition

mode AffinPlane is 2-dimensional AffinSpace;

end;

theorem :: DIRAF:52

canceled;

theorem :: DIRAF:53

for S being OAffinPlane holds Lambda S is AffinPlane

proof end;

theorem :: DIRAF:54

for AS being non empty AffinStruct holds
( AS is AffinPlane iff ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) & ( for x, y, z, t being Element of AS st not x,y // z,t holds
ex u being Element of AS st
( x,y // x,u & z,t // z,u ) ) ) ) by Def7, Def8, REALSET2:def 7;