:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received May 4, 1990

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

definition
end;

:: deftheorem defines LIN AFF_1:def 1 :

for AS being AffinSpace

for a, b, c being Element of AS holds

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

for AS being AffinSpace

for a, b, c being Element of AS holds

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

::$CT

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;

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 Th3: :: AFF_1:4

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 )

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

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

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 )

by DIRAF:40, Th3;

theorem Th5: :: AFF_1:6

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 )

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 Th7: :: AFF_1:8

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

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 Th8: :: AFF_1:9

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

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 Th9: :: AFF_1:10

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

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 Th10: :: AFF_1:11

for AS being AffinSpace

for x, y, z, u, 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

for x, y, z, u, 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 :: AFF_1:13

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

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

for AS being AffinSpace

for a, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds

b = b9

for a, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds

b = b9

proof end;

::

:: Definition of the Line joining two points

::

:: Definition of the Line joining two points

::

definition

let AS be AffinSpace;

let a, b be Element of AS;

ex b_{1} being Subset of AS st

for x being Element of AS holds

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

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

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

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

b_{1} = b_{2}

end;
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 for x being Element of AS holds

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

ex b

for x being Element of AS holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines Line AFF_1:def 2 :

for AS being AffinSpace

for a, b being Element of AS

for b_{4} being Subset of AS holds

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

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

for AS being AffinSpace

for a, b being Element of AS

for b

( b

( x in b

Lm5: for AS being AffinSpace

for a, b being Element of AS holds Line (a,b) c= 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

for a, b being Element of AS holds Line (a,b) = Line (b,a)

end;
let a, b be Element of AS;

:: original: Line

redefine func Line (a,b) -> Subset of AS;

commutativity

for a, b being Element of AS holds Line (a,b) = Line (b,a)

proof end;

theorem Th15: :: AFF_1:16

for AS being AffinSpace

for a, b, c, 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)

for a, b, c, 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 Th16: :: AFF_1:17

for AS being AffinSpace

for a, b, c, 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)

for a, b, c, 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 of the Line

::

:: Definition of the Line

::

definition

let AS be AffinSpace;

let A be Subset of AS;

end;
let A be Subset of AS;

::

:: Definition of the Line

::

:: Definition of the Line

::

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

ex a, b being Element of AS st

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

:: deftheorem Def3 defines being_line AFF_1:def 3 :

for AS being AffinSpace

for A being Subset of AS holds

( A is being_line iff ex a, b being Element of AS st

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

for AS being AffinSpace

for A being Subset of AS holds

( A is being_line iff ex a, b being Element of AS st

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

registration
end;

Lm6: for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b)

proof end;

:: Otrzymujemy stad zasadnicze stwierdzenie, ze kazda prosta

:: jest jednoznacznie wyznaczona przez swoje dowolne dwa punkty.

:: jest jednoznacznie wyznaczona przez swoje dowolne dwa punkty.

theorem Th17: :: AFF_1:18

for AS being AffinSpace

for a, b being Element of AS

for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds

A = C

for a, b being Element of AS

for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds

A = C

proof end;

theorem Th18: :: AFF_1:19

for AS being AffinSpace

for A being Subset of AS st A is being_line holds

ex a, b being Element of AS st

( a in A & b in A & a <> b )

for A being Subset of AS st A is being_line holds

ex a, b being Element of AS st

( a in A & b in A & a <> b )

proof end;

theorem Th19: :: AFF_1:20

for AS being AffinSpace

for a being Element of AS

for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

for a being Element of AS

for A being Subset of AS st A is being_line holds

ex b being Element of AS st

( a <> b & b in A )

proof end;

theorem Th20: :: AFF_1:21

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 being_line & a in A & b in A & c in A ) )

for a, b, c being Element of AS holds

( LIN a,b,c iff ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

proof end;

::

:: Definition of the parallelity between segments and lines

::

:: Definition of the parallelity between segments and lines

::

:: deftheorem defines // AFF_1:def 4 :

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS holds

( a,b // A iff ex c, d being Element of AS st

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

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS holds

( a,b // A iff ex c, d being Element of AS st

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

:: deftheorem defines // AFF_1:def 5 :

for AS being AffinSpace

for A, C being Subset of AS holds

( A // C iff ex a, b being Element of AS st

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

for AS being AffinSpace

for A, C being Subset of AS holds

( A // C iff ex a, b being Element of AS st

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

theorem Th21: :: AFF_1:22

for AS being AffinSpace

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

( d in Line (a,b) iff a,b // c,d )

for a, b, c, 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 Th22: :: AFF_1:23

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A holds

( b in A iff a,b // A )

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A holds

( b in A iff a,b // A )

proof end;

theorem :: AFF_1:24

theorem Th24: :: AFF_1:25

for AS being AffinSpace

for a, b, x being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

for a, b, x being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

proof end;

theorem :: AFF_1:26

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

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

A is being_line ;

theorem Th26: :: AFF_1:27

for AS being AffinSpace

for a, b, c, d being Element of AS

for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

for a, b, c, d being Element of AS

for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

proof end;

theorem Th27: :: AFF_1:28

for AS being AffinSpace

for a, b being Element of AS

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

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

for a, b being Element of AS

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

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

proof end;

theorem Th29: :: AFF_1:30

for AS being AffinSpace

for a, b being Element of AS

for A being being_line Subset of AS 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 ) )

for a, b being Element of AS

for A being being_line Subset of AS 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:31

for AS being AffinSpace

for a, b, c, d being Element of AS

for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

for a, b, c, d being Element of AS

for A being being_line Subset of AS st a,b // A & c,d // A holds

a,b // c,d

proof end;

theorem Th31: :: AFF_1:32

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

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 Th32: :: AFF_1:33

for AS being AffinSpace

for a being Element of AS

for A being being_line Subset of AS holds a,a // A

for a being Element of AS

for A being being_line Subset of AS holds a,a // A

proof end;

theorem Th33: :: AFF_1:34

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

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

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

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 Th35: :: AFF_1:36

for AS being AffinSpace

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

( A is being_line & C is being_line )

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

( A is being_line & C is being_line )

proof end;

theorem Th36: :: AFF_1:37

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

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 Th37: :: AFF_1:38

for AS being AffinSpace

for a, b, c, d being Element of AS

for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds

( A // C iff a,b // c,d )

for a, b, c, d being Element of AS

for A, C being being_line Subset of AS st 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 Th38: :: AFF_1:39

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

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

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

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;

definition

let AS be AffinSpace;

let A, B be being_line Subset of AS;

:: original: //

redefine pred A // B;

reflexivity

for A being being_line Subset of AS holds (AS,b_{1},b_{1})
by Th40;

end;
let A, B be being_line Subset of AS;

:: original: //

redefine pred A // B;

reflexivity

for A being being_line Subset of AS holds (AS,b

definition

let AS be AffinSpace;

let A, C be Subset of AS;

:: original: //

redefine pred A // C;

symmetry

for A, C being Subset of AS st (AS,b_{1},b_{2}) holds

(AS,b_{2},b_{1})
by Th41;

end;
let A, C be Subset of AS;

:: original: //

redefine pred A // C;

symmetry

for A, C being Subset of AS st (AS,b

(AS,b

theorem Th42: :: AFF_1:43

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

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

theorem Th44: :: AFF_1:45

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

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

for AS being AffinSpace

for a, b, x 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

for a, b, x 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:47

for AS being AffinSpace

for a, a9, b, b9, p being Element of AS

for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

for a, a9, b, b9, p being Element of AS

for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

proof end;

theorem :: AFF_1:48

for AS being AffinSpace

for a, b, c, d being Element of AS

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

d in A

for a, b, c, d being Element of AS

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

d in A

proof end;

theorem :: AFF_1:49

for AS being AffinSpace

for a being Element of AS

for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

for a being Element of AS

for A being being_line Subset of AS ex C being Subset of AS st

( a in C & A // C )

proof end;

theorem :: AFF_1:50

::

:: Additional theorems

::

:: Additional theorems

::

theorem :: AFF_1:51

theorem :: AFF_1:52

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A holds

a,b // A by Th22;

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A holds

a,b // A by Th22;

theorem :: AFF_1:53

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

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 Th53: :: AFF_1:54

for AS being AffinSpace

for a, a9, b, b9, o being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds

( a9 = o & b9 = o )

for a, a9, b, b9, o being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds

( a9 = o & b9 = o )

proof end;

theorem Th54: :: AFF_1:55

for AS being AffinSpace

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

b9 = o

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

b9 = o

proof end;

theorem :: AFF_1:56

for AS being AffinSpace

for a, a9, b, b9, o, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds

b9 = x

for a, a9, b, b9, o, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds

b9 = x

proof end;

theorem :: AFF_1:57

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b) by Lm6;

for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b) by Lm6;

theorem Th57: :: AFF_1:58

for AP being AffinPlane

for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds

ex x being Element of AP st

( x in A & x in C )

for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds

ex x being Element of AP st

( x in A & x in C )

proof end;

theorem :: AFF_1:59

for AP being AffinPlane

for a, b being Element of AP

for A being Subset of AP st A is being_line & not a,b // A holds

ex x being Element of AP st

( x in A & LIN a,b,x )

for a, b being Element of AP

for A being Subset of AP st A is being_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:60

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 )

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;