:: Parallelity and Lines in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 4, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: 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
theorem Th11: :: AFF_1:11
Lm1:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y
theorem Th12: :: AFF_1:12
Lm2:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t
Lm3:
for AS being AffinSpace
for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z
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 )
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
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 )
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 )
theorem Th16: :: AFF_1:16
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
theorem Th18: :: AFF_1:18
theorem Th19: :: AFF_1:19
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
theorem Th21: :: AFF_1:21
theorem :: AFF_1:22
theorem :: AFF_1:23
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 )
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
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
theorem :: AFF_1:24
canceled;
theorem Th25: :: AFF_1:25
theorem Th26: :: AFF_1:26
theorem Th27: :: AFF_1:27
theorem Th28: :: AFF_1:28
:: deftheorem Def3 defines being_line AFF_1:def 3 :
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
theorem :: AFF_1:29
canceled;
theorem Th30: :: AFF_1:30
theorem Th31: :: AFF_1:31
theorem Th32: :: AFF_1:32
theorem Th33: :: AFF_1:33
:: deftheorem Def4 defines // AFF_1:def 4 :
:: deftheorem Def5 defines // AFF_1:def 5 :
theorem :: AFF_1:34
canceled;
theorem :: AFF_1:35
canceled;
theorem Th36: :: AFF_1:36
theorem Th37: :: AFF_1:37
theorem :: AFF_1:38
theorem Th39: :: AFF_1:39
theorem Th40: :: AFF_1:40
theorem Th41: :: AFF_1:41
theorem :: AFF_1:42
canceled;
theorem Th43: :: AFF_1:43
theorem Th44: :: AFF_1:44
theorem :: AFF_1:45
theorem Th46: :: AFF_1:46
theorem Th47: :: AFF_1:47
theorem Th48: :: AFF_1:48
theorem :: AFF_1:49
theorem Th50: :: AFF_1:50
theorem Th51: :: AFF_1:51
theorem Th52: :: AFF_1:52
theorem Th53: :: AFF_1:53
theorem :: AFF_1:54
theorem Th55: :: AFF_1:55
theorem Th56: :: AFF_1:56
theorem Th57: :: AFF_1:57
Lm7:
for AS being AffinSpace
for A, C, D being Subset of AS st A // C & C // D holds
A // D
theorem :: AFF_1:58
theorem Th59: :: AFF_1:59
theorem :: AFF_1:60
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'
theorem :: AFF_1:62
theorem :: AFF_1:63
theorem :: AFF_1:64
theorem :: AFF_1:65
theorem :: AFF_1:66
theorem :: AFF_1:67
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 )
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
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
theorem :: AFF_1:71
theorem Th72: :: AFF_1:72
theorem :: AFF_1:73
theorem :: AFF_1:74