:: Lines on Planes in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received May 24, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: EUCLIDLP:1
theorem :: EUCLIDLP:2
canceled;
theorem :: EUCLIDLP:3
canceled;
theorem :: EUCLIDLP:4
canceled;
theorem :: EUCLIDLP:5
canceled;
theorem :: EUCLIDLP:6
canceled;
theorem Th7: :: EUCLIDLP:7
theorem Th8: :: EUCLIDLP:8
theorem Th9: :: EUCLIDLP:9
theorem Th10: :: EUCLIDLP:10
theorem Th11: :: EUCLIDLP:11
theorem Th12: :: EUCLIDLP:12
theorem Th13: :: EUCLIDLP:13
Lm1:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
theorem Th14: :: EUCLIDLP:14
theorem Th15: :: EUCLIDLP:15
theorem Th16: :: EUCLIDLP:16
theorem Th17: :: EUCLIDLP:17
theorem Th18: :: EUCLIDLP:18
theorem Th19: :: EUCLIDLP:19
theorem :: EUCLIDLP:20
theorem Th21: :: EUCLIDLP:21
theorem Th22: :: EUCLIDLP:22
theorem Th23: :: EUCLIDLP:23
theorem :: EUCLIDLP:24
theorem Th25: :: EUCLIDLP:25
theorem Th26: :: EUCLIDLP:26
theorem Th27: :: EUCLIDLP:27
theorem Th28: :: EUCLIDLP:28
theorem Th29: :: EUCLIDLP:29
for
a1,
a2,
a3,
b1,
b2,
b3 being
Real for
n being
Element of
NAT for
x1,
x2,
x3 being
Element of
REAL n holds
(((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3)
theorem Th30: :: EUCLIDLP:30
theorem Th31: :: EUCLIDLP:31
for
a1,
a2,
a3,
b1,
b2,
b3 being
Real for
n being
Element of
NAT for
x1,
x2,
x3 being
Element of
REAL n holds
(((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)
theorem Th32: :: EUCLIDLP:32
for
a1,
a2,
a3 being
Real for
n being
Element of
NAT for
x1,
x2,
x3 being
Element of
REAL n st
(a1 + a2) + a3 = 1 holds
((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1))
theorem Th33: :: EUCLIDLP:33
for
a2,
a3 being
Real for
n being
Element of
NAT for
x,
x1,
x2,
x3 being
Element of
REAL n st
x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds
ex
a1 being
Real st
(
x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) &
(a1 + a2) + a3 = 1 )
theorem :: EUCLIDLP:34
theorem Th35: :: EUCLIDLP:35
theorem Th36: :: EUCLIDLP:36
:: deftheorem Def1 defines // EUCLIDLP:def 1 :
theorem Th37: :: EUCLIDLP:37
theorem Th38: :: EUCLIDLP:38
:: deftheorem Def2 defines are_lindependent2 EUCLIDLP:def 2 :
Lm2:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> 0* n
theorem :: EUCLIDLP:39
theorem Th40: :: EUCLIDLP:40
theorem Th41: :: EUCLIDLP:41
for
a1,
a2,
b1,
b2 being
Real for
n being
Element of
NAT for
y2,
x1,
x2,
y1,
y1 being
Element of
REAL n st
y1,
y2 are_lindependent2 &
y1 = (a1 * x1) + (a2 * x2) &
y2 = (b1 * x1) + (b2 * x2) holds
ex
c1,
c2,
d1,
d2 being
Real st
(
x1 = (c1 * y1) + (c2 * y2) &
x2 = (d1 * y1) + (d2 * y2) )
theorem Th42: :: EUCLIDLP:42
theorem :: EUCLIDLP:43
theorem :: EUCLIDLP:44
theorem Th45: :: EUCLIDLP:45
for
n being
Element of
NAT for
x1,
x0,
x3,
x2,
y0,
y1,
y2,
y3 being
Element of
REAL n st
x1 - x0,
x3 - x2 are_lindependent2 &
y0 in Line x0,
x1 &
y1 in Line x0,
x1 &
y0 <> y1 &
y2 in Line x2,
x3 &
y3 in Line x2,
x3 &
y2 <> y3 holds
y1 - y0,
y3 - y2 are_lindependent2
Lm3:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
theorem :: EUCLIDLP:46
Lm4:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds
x1 // x2
theorem :: EUCLIDLP:47
theorem Th48: :: EUCLIDLP:48
:: deftheorem Def3 defines _|_ EUCLIDLP:def 3 :
theorem Th49: :: EUCLIDLP:49
theorem Th50: :: EUCLIDLP:50
theorem :: EUCLIDLP:51
:: deftheorem defines line_of_REAL EUCLIDLP:def 4 :
theorem Th52: :: EUCLIDLP:52
theorem Th53: :: EUCLIDLP:53
theorem Th54: :: EUCLIDLP:54
theorem :: EUCLIDLP:55
theorem Th56: :: EUCLIDLP:56
theorem Th57: :: EUCLIDLP:57
theorem Th58: :: EUCLIDLP:58
theorem Th59: :: EUCLIDLP:59
theorem Th60: :: EUCLIDLP:60
:: deftheorem defines dist_v EUCLIDLP:def 5 :
:: deftheorem defines dist EUCLIDLP:def 6 :
theorem :: EUCLIDLP:61
theorem Th62: :: EUCLIDLP:62
theorem :: EUCLIDLP:63
theorem :: EUCLIDLP:64
definition
let n be
Element of
NAT ;
let L1,
L2 be
Element of
line_of_REAL n;
pred L1 // L2 means :
Def7:
:: EUCLIDLP:def 7
ex
x1,
x2,
y1,
y2 being
Element of
REAL n st
(
L1 = Line x1,
x2 &
L2 = Line y1,
y2 &
x2 - x1 // y2 - y1 );
symmetry
for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line x1,x2 & L2 = Line y1,y2 & x2 - x1 // y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line x1,x2 & L1 = Line y1,y2 & x2 - x1 // y2 - y1 )
;
end;
:: deftheorem Def7 defines // EUCLIDLP:def 7 :
theorem Th65: :: EUCLIDLP:65
definition
let n be
Element of
NAT ;
let L1,
L2 be
Element of
line_of_REAL n;
pred L1 _|_ L2 means :
Def8:
:: EUCLIDLP:def 8
ex
x1,
x2,
y1,
y2 being
Element of
REAL n st
(
L1 = Line x1,
x2 &
L2 = Line y1,
y2 &
x2 - x1 _|_ y2 - y1 );
symmetry
for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line x1,x2 & L2 = Line y1,y2 & x2 - x1 _|_ y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line x1,x2 & L1 = Line y1,y2 & x2 - x1 _|_ y2 - y1 )
;
end;
:: deftheorem Def8 defines _|_ EUCLIDLP:def 8 :
theorem Th66: :: EUCLIDLP:66
theorem Th67: :: EUCLIDLP:67
theorem Th68: :: EUCLIDLP:68
theorem Th69: :: EUCLIDLP:69
theorem Th70: :: EUCLIDLP:70
theorem Th71: :: EUCLIDLP:71
theorem Th72: :: EUCLIDLP:72
theorem :: EUCLIDLP:73
theorem :: EUCLIDLP:74
theorem Th75: :: EUCLIDLP:75
theorem Th76: :: EUCLIDLP:76
theorem Th77: :: EUCLIDLP:77
theorem :: EUCLIDLP:78
theorem Th79: :: EUCLIDLP:79
theorem Th80: :: EUCLIDLP:80
theorem Th81: :: EUCLIDLP:81
theorem Th82: :: EUCLIDLP:82
theorem :: EUCLIDLP:83
for
n being
Element of
NAT for
x2,
x1,
x3,
y2,
y3 being
Element of
REAL n for
L1,
L2 being
Element of
line_of_REAL n st
x2 - x1,
x3 - x1 are_lindependent2 &
y2 in Line x1,
x2 &
y3 in Line x1,
x3 &
L1 = Line x2,
x3 &
L2 = Line y2,
y3 holds
(
L1 // L2 iff ex
a being
Real st
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) ) )
theorem Th84: :: EUCLIDLP:84
theorem Th85: :: EUCLIDLP:85
theorem Th86: :: EUCLIDLP:86
:: deftheorem defines plane EUCLIDLP:def 9 :
:: deftheorem Def10 defines being_plane EUCLIDLP:def 10 :
theorem Th87: :: EUCLIDLP:87
theorem Th88: :: EUCLIDLP:88
for
n being
Element of
NAT for
x1,
y1,
y2,
y3,
x2,
x3 being
Element of
REAL n st
x1 in plane y1,
y2,
y3 &
x2 in plane y1,
y2,
y3 &
x3 in plane y1,
y2,
y3 holds
plane x1,
x2,
x3 c= plane y1,
y2,
y3
theorem :: EUCLIDLP:89
theorem Th90: :: EUCLIDLP:90
for
n being
Element of
NAT for
y1,
x1,
x2,
x3,
y2 being
Element of
REAL n st
y1 in plane x1,
x2,
x3 &
y2 in plane x1,
x2,
x3 holds
Line y1,
y2 c= plane x1,
x2,
x3
theorem :: EUCLIDLP:91
theorem :: EUCLIDLP:92
for
a1,
a2,
a3 being
Real for
n being
Element of
NAT for
x1,
x3,
x,
x2 being
Element of
REAL n st
x1 - x1,
x3 - x1 are_lindependent2 &
x in plane x1,
x2,
x3 &
x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not
(a1 + a2) + a3 = 1 holds
0* n in plane x1,
x2,
x3
theorem Th93: :: EUCLIDLP:93
theorem :: EUCLIDLP:94
for
a1,
a2,
a3,
b1,
b2,
b3 being
Real for
n being
Element of
NAT for
x2,
x1,
x3,
x being
Element of
REAL n st
x2 - x1,
x3 - x1 are_lindependent2 &
x in plane x1,
x2,
x3 &
(a1 + a2) + a3 = 1 &
x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) &
(b1 + b2) + b3 = 1 &
x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
(
a1 = b1 &
a2 = b2 &
a3 = b3 )
:: deftheorem defines plane_of_REAL EUCLIDLP:def 11 :
theorem Th95: :: EUCLIDLP:95
theorem Th96: :: EUCLIDLP:96
theorem Th97: :: EUCLIDLP:97
theorem :: EUCLIDLP:98
theorem :: EUCLIDLP:99
for
n being
Element of
NAT for
x1,
x2,
x3 being
Element of
REAL n holds
(
Line x1,
x2 c= plane x1,
x2,
x3 &
Line x2,
x3 c= plane x1,
x2,
x3 &
Line x3,
x1 c= plane x1,
x2,
x3 )
theorem Th100: :: EUCLIDLP:100
:: deftheorem Def12 defines are_coplane EUCLIDLP:def 12 :
theorem Th101: :: EUCLIDLP:101
theorem Th102: :: EUCLIDLP:102
theorem Th103: :: EUCLIDLP:103
theorem Th104: :: EUCLIDLP:104
theorem Th105: :: EUCLIDLP:105
theorem Th106: :: EUCLIDLP:106
theorem Th107: :: EUCLIDLP:107
theorem :: EUCLIDLP:108
theorem :: EUCLIDLP:109
theorem :: EUCLIDLP:110
theorem Th111: :: EUCLIDLP:111
theorem Th112: :: EUCLIDLP:112
theorem Th113: :: EUCLIDLP:113
theorem Th114: :: EUCLIDLP:114
theorem Th115: :: EUCLIDLP:115
theorem Th116: :: EUCLIDLP:116
theorem Th117: :: EUCLIDLP:117
theorem Th118: :: EUCLIDLP:118
theorem :: EUCLIDLP:119