:: AFF_1 semantic presentation

definition

let AS be AffinSpace;
let a, b, c be Element of AS;
pred LIN a,b,c means :Def1: :: AFF_1:def 1
a,b // a,c;

end;

:: deftheorem Def1 defines LIN AFF_1:def 1 :

theorem :: AFF_1:1

canceled;

theorem :: AFF_1:2

canceled;

theorem :: AFF_1:3

canceled;

theorem :: AFF_1:4

canceled;

theorem :: AFF_1:5

canceled;

theorem :: AFF_1:6

canceled;

theorem :: AFF_1:7

canceled;

theorem :: AFF_1:8

canceled;

theorem :: AFF_1:9

canceled;

theorem Th10: :: AFF_1:10

for AS being AffinSpace
for a being Element of AS ex b being Element of AS st a <> b

proof end;

theorem Th11: :: AFF_1:11

for AS being AffinSpace
for x, y being Element of AS holds
( x,y // y,x & x,y // x,y )

proof end;

Lm1: for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y

proof end;

theorem Th12: :: AFF_1:12

for AS being AffinSpace
for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y )

proof end;

Lm2: for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t

proof end;

Lm3: for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z

proof end;

theorem Th13: :: AFF_1:13

for AS being AffinSpace
for x, y, z, t being Element of AS 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 Th14: :: AFF_1:14

for AS being AffinSpace
for a, b, x, y, z, t being Element of AS 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;

Lm4: for AS being AffinSpace
for x, y, z being Element of AS st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z )

proof end;

theorem Th15: :: AFF_1:15

for AS being AffinSpace
for x, y, z being Element of AS st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )

proof end;

theorem Th16: :: AFF_1:16

for AS being AffinSpace
for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x )

proof end;

theorem Th17: :: AFF_1:17

for AS being AffinSpace
for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds
LIN z,t,u

proof end;

theorem Th18: :: AFF_1:18

for AS being AffinSpace
for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds
LIN x,y,t

proof end;

theorem Th19: :: AFF_1:19

for AS being AffinSpace
for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds
x,y // z,t

proof end;

theorem Th20: :: AFF_1:20

for AS being AffinSpace
for u, z, x, y, w being Element of AS st u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w holds
LIN x,y,w

proof end;

theorem Th21: :: AFF_1:21

for AS being AffinSpace holds
not for x, y, z being Element of AS holds LIN x,y,z

proof end;

theorem :: AFF_1:22

for AS being AffinSpace
for x, y being Element of AS st x <> y holds
ex z being Element of AS st not LIN x,y,z

proof end;

theorem :: AFF_1:23

for AS being AffinSpace
for o, a, b, b' being Element of AS st not LIN o,a,b & LIN o,b,b' & a,b // a,b' holds
b = b'

proof end;

definition

let AS be AffinSpace;
let a, b be Element of AS;
func Line a,b -> Subset of AS means :Def2: :: AFF_1:def 2
for x being Element of AS holds
( x in it iff LIN a,b,x );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Line AFF_1:def 2 :

Lm5: for AS being AffinSpace
for a, b being Element of AS holds Line a,b c= Line b,a

proof end;

theorem :: AFF_1:24

canceled;

theorem Th25: :: AFF_1:25

for AS being AffinSpace
for a, b being Element of AS holds Line a,b = Line b,a

proof end;

definition

let AS be AffinSpace;
let a, b be Element of AS;
:: original: Line
redefine func Line a,b -> Subset of AS;
commutativity by Th25;

end;

theorem Th26: :: AFF_1:26

for AS being AffinSpace
for a, b being Element of AS holds
( a in Line a,b & b in Line a,b )

proof end;

theorem Th27: :: AFF_1:27

for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line a,b & d in Line a,b & c <> d holds
Line c,d c= Line a,b

proof end;

theorem Th28: :: AFF_1:28

for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line a,b & d in Line a,b & a <> b holds
Line a,b c= Line c,d

proof end;

definition

let AS be AffinSpace;
let A be Subset of AS;
attr A is being_line means :Def3: :: AFF_1:def 3
ex a, b being Element of AS st
( a <> b & A = Line a,b );

end;

:: deftheorem Def3 defines being_line AFF_1:def 3 :

notation

let AS be AffinSpace;
let A be Subset of AS;
synonym A is_line for being_line A;

end;

Lm6: for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is_line & a in A & b in A & a <> b holds
A = Line a,b

proof end;

theorem :: AFF_1:29

canceled;

theorem Th30: :: AFF_1:30

for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st A is_line & C is_line & a in A & b in A & a in C & b in C & not a = b holds
A = C

proof end;

theorem Th31: :: AFF_1:31

for AS being AffinSpace
for A being Subset of AS st A is_line holds
ex a, b being Element of AS st
( a in A & b in A & a <> b )

proof end;

theorem Th32: :: AFF_1:32

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
ex b being Element of AS st
( a <> b & b in A )

proof end;

theorem Th33: :: AFF_1:33

for AS being AffinSpace
for a, b, c being Element of AS holds
( LIN a,b,c iff ex A being Subset of AS st
( A is_line & a in A & b in A & c in A ) )

proof end;

definition

let AS be AffinSpace;
let a, b be Element of AS;
let A be Subset of AS;
pred a,b // A means :Def4: :: AFF_1:def 4
ex c, d being Element of AS st
( c <> d & A = Line c,d & a,b // c,d );

end;

:: deftheorem Def4 defines // AFF_1:def 4 :

definition

let AS be AffinSpace;
let A, C be Subset of AS;
pred A // C means :Def5: :: AFF_1:def 5
ex a, b being Element of AS st
( A = Line a,b & a <> b & a,b // C );

end;

:: deftheorem Def5 defines // AFF_1:def 5 :

theorem :: AFF_1:34

canceled;

theorem :: AFF_1:35

canceled;

theorem Th36: :: AFF_1:36

for AS being AffinSpace
for c, a, b, d being Element of AS st c in Line a,b & a <> b holds
( d in Line a,b iff a,b // c,d )

proof end;

theorem Th37: :: AFF_1:37

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is_line & a in A holds
( b in A iff a,b // A )

proof end;

theorem :: AFF_1:38

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS holds
( a <> b & A = Line a,b iff ( A is_line & a in A & b in A & a <> b ) ) by Def3, Lm6, Th26;

theorem Th39: :: AFF_1:39

for AS being AffinSpace
for a, b, x being Element of AS
for A being Subset of AS st A is_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A

proof end;

theorem Th40: :: AFF_1:40

for AS being AffinSpace
for A being Subset of AS st ex a, b being Element of AS st a,b // A holds
A is_line

proof end;

theorem Th41: :: AFF_1:41

for AS being AffinSpace
for c, d, a, b being Element of AS
for A being Subset of AS st c in A & d in A & A is_line & c <> d holds
( a,b // A iff a,b // c,d )

proof end;

theorem :: AFF_1:42

canceled;

theorem Th43: :: AFF_1:43

for AS being AffinSpace
for a, b being Element of AS st a <> b holds
a,b // Line a,b

proof end;

theorem Th44: :: AFF_1:44

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is_line holds
( a,b // A iff ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d ) )

proof end;

theorem :: AFF_1:45

for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st A is_line & a,b // A & c,d // A holds
a,b // c,d

proof end;

theorem Th46: :: AFF_1:46

for AS being AffinSpace
for a, b, p, q being Element of AS
for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds
p,q // A

proof end;

theorem Th47: :: AFF_1:47

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
a,a // A

proof end;

theorem Th48: :: AFF_1:48

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A holds
b,a // A

proof end;

theorem :: AFF_1:49

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A & not a in A holds
not b in A

proof end;

theorem Th50: :: AFF_1:50

for AS being AffinSpace
for A, C being Subset of AS st A // C holds
( A is_line & C is_line )

proof end;

theorem Th51: :: AFF_1:51

for AS being AffinSpace
for A, C being Subset of AS holds
( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line a,b & C = Line c,d ) )

proof end;

theorem Th52: :: AFF_1:52

for AS being AffinSpace
for a, b, c, d being Element of AS
for A, C being Subset of AS st A is_line & C is_line & a in A & b in A & c in C & d in C & a <> b & c <> d holds
( A // C iff a,b // c,d )

proof end;

theorem Th53: :: AFF_1:53

for AS being AffinSpace
for a, b, c, d being Element of AS
for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d

proof end;

theorem :: AFF_1:54

for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a in A & b in A & A // C holds
a,b // C

proof end;

theorem Th55: :: AFF_1:55

for AS being AffinSpace
for A being Subset of AS st A is_line holds
A // A

proof end;

theorem Th56: :: AFF_1:56

for AS being AffinSpace
for A, C being Subset of AS st A // C holds
C // A

proof end;

definition

let AS be AffinSpace;
let A, C be Subset of AS;
:: original: //
redefine pred A // C;
symmetry by Th56;

end;

theorem Th57: :: AFF_1:57

for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a,b // A & A // C holds
a,b // C

proof end;

Lm7: for AS being AffinSpace
for A, C, D being Subset of AS st A // C & C // D holds
A // D

proof end;

theorem :: AFF_1:58

for AS being AffinSpace
for A, C, D being Subset of AS st ( ( A // C & C // D ) or ( A // C & D // C ) or ( C // A & C // D ) or ( C // A & D // C ) ) holds
A // D by Lm7;

theorem Th59: :: AFF_1:59

for AS being AffinSpace
for p being Element of AS
for A, C being Subset of AS st A // C & p in A & p in C holds
A = C

proof end;

theorem :: AFF_1:60

for AS being AffinSpace
for x, a, b being Element of AS
for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b

proof end;

theorem :: AFF_1:61

for AS being AffinSpace
for a, b, a', b', p being Element of AS
for K being Subset of AS st a,b // K & a',b' // K & LIN p,a,a' & LIN p,b,b' & p in K & not a in K & a = b holds
a' = b'

proof end;

theorem :: AFF_1:62

for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st A is_line & a in A & b in A & c in A & a <> b & a,b // c,d holds
d in A

proof end;

theorem :: AFF_1:63

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
ex C being Subset of AS st
( a in C & A // C )

proof end;

theorem :: AFF_1:64

for AS being AffinSpace
for p being Element of AS
for A, C, D being Subset of AS st A // C & A // D & p in C & p in D holds
C = D

proof end;

theorem :: AFF_1:65

for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st A is_line & a in A & b in A & c in A & d in A holds
a,b // c,d

proof end;

theorem :: AFF_1:66

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is_line & a in A & b in A holds
a,b // A by Th37;

theorem :: AFF_1:67

for AS being AffinSpace
for a, b being Element of AS
for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds
A // C

proof end;

theorem Th68: :: AFF_1:68

for AS being AffinSpace
for o, a, b, a', b' being Element of AS st not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a' = b' holds
( a' = o & b' = o )

proof end;

theorem Th69: :: AFF_1:69

for AS being AffinSpace
for o, a, b, a', b' being Element of AS st not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a' = o holds
b' = o

proof end;

theorem :: AFF_1:70

for AS being AffinSpace
for o, a, b, a', b', x being Element of AS st not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & LIN o,b,x & a,b // a',b' & a,b // a',x holds
b' = x

proof end;

theorem :: AFF_1:71

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st A is_line & a in A & b in A & a <> b holds
A = Line a,b by Lm6;

theorem Th72: :: AFF_1:72

for AP being AffinPlane
for A, C being Subset of AP st A is_line & C is_line & not A // C holds
ex x being Element of AP st
( x in A & x in C )

proof end;

theorem :: AFF_1:73

for AP being AffinPlane
for a, b being Element of AP
for A being Subset of AP st A is_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )

proof end;

theorem :: AFF_1:74

for AP being AffinPlane
for a, b, c, d being Element of AP st not a,b // c,d holds
ex p being Element of AP st
( LIN a,b,p & LIN c,d,p )

proof end;