:: Lines in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received August 8, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: EUCLID_4:1
theorem Th2: :: EUCLID_4:2
theorem Th3: :: EUCLID_4:3
theorem :: EUCLID_4:4
theorem :: EUCLID_4:5
theorem :: EUCLID_4:6
theorem :: EUCLID_4:7
theorem :: EUCLID_4:8
:: deftheorem defines Line EUCLID_4:def 1 :
for
n being
Nat for
x1,
x2 being
Element of
REAL n holds
Line x1,
x2 = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;
Lm1:
for n being Nat
for x1, x2 being Element of REAL n holds Line x1,x2 c= Line x2,x1
theorem Th9: :: EUCLID_4:9
theorem Th10: :: EUCLID_4:10
Lm2:
for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3
by FINSEQOP:29;
theorem Th11: :: EUCLID_4:11
theorem Th12: :: EUCLID_4:12
:: deftheorem Def2 defines being_line EUCLID_4:def 2 :
Lm3:
for n being Nat
for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line x1,x2
theorem :: EUCLID_4:13
theorem Th14: :: EUCLID_4:14
theorem :: EUCLID_4:15
theorem :: EUCLID_4:16
canceled;
theorem :: EUCLID_4:17
canceled;
theorem :: EUCLID_4:18
canceled;
theorem :: EUCLID_4:19
canceled;
theorem :: EUCLID_4:20
theorem Th21: :: EUCLID_4:21
theorem Th22: :: EUCLID_4:22
theorem Th23: :: EUCLID_4:23
theorem :: EUCLID_4:24
theorem Th25: :: EUCLID_4:25
theorem Th26: :: EUCLID_4:26
theorem :: EUCLID_4:27
theorem Th28: :: EUCLID_4:28
theorem :: EUCLID_4:29
theorem :: EUCLID_4:30
theorem Th31: :: EUCLID_4:31
theorem :: EUCLID_4:32
theorem :: EUCLID_4:33
theorem :: EUCLID_4:34
theorem Th35: :: EUCLID_4:35
theorem Th36: :: EUCLID_4:36
theorem Th37: :: EUCLID_4:37
theorem Th38: :: EUCLID_4:38
theorem :: EUCLID_4:39
theorem :: EUCLID_4:40
theorem :: EUCLID_4:41
theorem :: EUCLID_4:42
theorem :: EUCLID_4:43
theorem :: EUCLID_4:44
Lm4:
for a being Real
for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
Lm5:
for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
Lm6:
for n being Nat
for y1, y2, x1, x2 being Element of REAL n st y1 in Line x1,x2 & y2 in Line x1,x2 holds
ex a being Real st y1 - y2 = a * (x1 - x2)
Lm7:
for n being Nat
for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line x1,x2 holds
|.(y1 - y2).| <= |.(y1 - x).| ) )
theorem :: EUCLID_4:45
:: deftheorem EUCLID_4:def 3 :
canceled;
:: deftheorem EUCLID_4:def 4 :
canceled;
:: deftheorem EUCLID_4:def 5 :
canceled;
:: deftheorem EUCLID_4:def 6 :
canceled;
:: deftheorem defines Line EUCLID_4:def 7 :
for
n being
Nat for
p1,
p2 being
Point of
(TOP-REAL n) holds
Line p1,
p2 = { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ;
Lm8:
for n being Nat
for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
theorem Th46: :: EUCLID_4:46
theorem Th47: :: EUCLID_4:47
theorem Th48: :: EUCLID_4:48
theorem Th49: :: EUCLID_4:49
:: deftheorem Def8 defines being_line EUCLID_4:def 8 :
Lm9:
for n being Nat
for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line p1,p2
theorem :: EUCLID_4:50
theorem Th51: :: EUCLID_4:51
theorem :: EUCLID_4:52
:: deftheorem defines TPn2Rn EUCLID_4:def 9 :
theorem :: EUCLID_4:53