:: Parallelity and Lines in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let AS be AffinSpace;
let a, b, c be Element of AS;

pred LIN a,b,c means :: AFF_1:def 1
a,b // a,c;

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

theorem :: AFF_1:1

canceled;

::$CT

theorem Th1: :: AFF_1:2

for AS being AffinSpace
for x, y being Element of AS holds
( x,y // y,x & x,y // x,y ) by DIRAF:40;

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 Th2: :: AFF_1:3

for AS being AffinSpace
for x, y, z being Element of AS holds
( x,y // z,z & z,z // x,y ) by Lm1, DIRAF:40;

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 )

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

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 )

proof end;

theorem Th6: :: AFF_1:7

for AS being AffinSpace
for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x ) by Th1, Th2;

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

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

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

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

proof end;

theorem Th11: :: AFF_1:12

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

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

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

proof end;

::
:: Definition of the Line joining two points
::

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
ex b₁ being Subset of AS st
for x being Element of AS holds
( x in b₁ iff LIN a,b,x )

proof end;

uniqueness
for b₁, b₂ being Subset of AS st ( for x being Element of AS holds
( x in b₁ iff LIN a,b,x ) ) & ( for x being Element of AS holds
( x in b₂ iff LIN a,b,x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Line AFF_1:def 2 :
for AS being AffinSpace
for a, b being Element of AS
for b₄ being Subset of AS holds
( b₄ = Line (a,b) iff for x being Element of AS holds
( x in b₄ iff LIN a,b,x ) );

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)

proof end;

end;

theorem Th14: :: AFF_1:15

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

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)

proof end;

::
:: Definition of the Line
::

definition

let AS be AffinSpace;
let A be Subset of AS;

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

end;

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

registration

let AS be AffinSpace;

cluster being_line for M3(K24( the carrier of AS));

existence
ex b₁ being Subset of AS st b₁ is being_line

proof end;

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.

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

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 )

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 )

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

proof end;

::
:: Definition of the parallelity between segments and lines
::

definition

let AS be AffinSpace;
let a, b be Element of AS;
let A be Subset of AS;

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

end;

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

definition

let AS be AffinSpace;
let A, C be Subset of AS;

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

end;

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

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 )

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 )

proof end;

theorem :: AFF_1:24

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 being_line & a in A & b in A & a <> b ) ) by Lm6, Th14;

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

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 ;

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 )

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 )

proof end;

theorem Th28: :: AFF_1:29

for AS being AffinSpace
for a, b being Element of AS st a <> b holds
a,b // Line (a,b) by Th1;

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

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

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

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

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

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

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 )

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

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 )

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

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

proof end;

theorem Th40: :: AFF_1:41

for AS being AffinSpace
for A being being_line Subset of AS holds A // A

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₁,b₁) by Th40;

end;

theorem Th41: :: AFF_1:42

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
for A, C being Subset of AS st (AS,b₁,b₂) holds
(AS,b₂,b₁) by Th41;

end;

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

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

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

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

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

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

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 )

proof end;

theorem :: AFF_1:50

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 by Lm7, Th44;

::
:: Additional theorems
::

theorem :: AFF_1:51

for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & c in A & d in A holds
a,b // c,d by Th38, Th40;

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;

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

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 )

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

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

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;

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 )

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 )

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 )

proof end;