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


begin

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 :
for AS being AffinSpace
for a, b, c being Element of AS holds
( LIN a,b,c iff a,b // a,c );

theorem Th1: :: AFF_1:1
for AS being AffinSpace
for a being Element of AS ex b being Element of AS st a <> b
proof end;

theorem Th2: :: AFF_1:2
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 Th3: :: AFF_1:3
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 Th4: :: 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 Th5: :: 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 )

proof end;

theorem Th6: :: 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 Th7: :: 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 )
proof end;

theorem Th8: :: 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 Th9: :: 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 Th10: :: 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 Th11: :: AFF_1:11
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 Th12: :: 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 o, a, b, b9 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 b1 being Subset of AS st
for x being Element of AS holds
( x in b1 iff LIN a,b,x )
proof end;
uniqueness
for b1, b2 being Subset of AS st ( for x being Element of AS holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of AS holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Line AFF_1:def 2 :
for AS being AffinSpace
for a, b being Element of AS
for b4 being Subset of AS holds
( b4 = Line (a,b) iff for x being Element of AS holds
( x in b4 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 Th15: :: 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 Th16: :: AFF_1:16
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 Th17: :: AFF_1:17
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 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 M2(K24( the carrier of AS));
existence
ex b1 being Subset of AS st b1 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 Th18: :: 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 Th19: :: 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 Th20: :: 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 Th21: :: 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 :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 :
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 :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 :
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 Th22: :: AFF_1:22
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 Th23: :: 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 Def3, Lm6, Th15;

theorem Th25: :: 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 Th26: :: 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
proof end;

theorem Th27: :: AFF_1:27
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 being_line & c <> d holds
( a,b // A iff a,b // c,d )
proof end;

theorem Th28: :: 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 Th29: :: AFF_1:29
for AS being AffinSpace
for a, b being Element of AS st a <> b holds
a,b // Line (a,b)
proof end;

theorem Th30: :: 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 Th32: :: 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 Th33: :: 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 Th34: :: 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 Th36: :: 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 Th37: :: 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 Th38: :: 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 Th39: :: 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 Th41: :: 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,b1,b1)
by Th41;
end;

theorem Th42: :: 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,b1,b2) holds
(AS,b2,b1)
by Th42;
end;

theorem Th43: :: 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 Th45: :: 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 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:47
for AS being AffinSpace
for a9, b9, p, a, b 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, Th45;

::
:: 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 Th39, Th41;

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

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 Th54: :: AFF_1:54
for AS being AffinSpace
for o, a, b, a9, b9 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 Th55: :: AFF_1:55
for AS being AffinSpace
for o, a, b, b9, a9 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 o, a, b, a9, b9, 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 Th58: :: 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;