:: Lines on Planes in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received May 24, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, ARYTM_3, RELAT_1, ARYTM_1, EUCLID,
COMPLEX1, CARD_1, RVSUM_1, XXREAL_0, JORDAN2C, FINSEQ_1, FINSEQ_2,
FUNCT_1, AFF_1, INCSP_1, TARSKI, ANALOAF, EUCLID_3, SQUARE_1, SYMSP_1,
SETFAM_1, ZFMISC_1, XBOOLE_0, METRIC_1, SEQ_4, XXREAL_2, AFF_4, EUCLIDLP,
NAT_1;
notations ORDINAL1, ZFMISC_1, FUNCT_1, SEQ_4, TARSKI, SETFAM_1, XBOOLE_0,
XXREAL_0, XXREAL_2, XCMPLX_0, XREAL_0, NUMBERS, REAL_1, SUBSET_1,
FINSEQ_1, FINSEQ_2, SQUARE_1, RVSUM_1, EUCLID, EUCLID_4;
constructors REAL_1, SQUARE_1, SEQ_4, FINSEQOP, EUCLID_4, RVSUM_1, BINOP_2;
registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, EUCLID,
VALUED_0, SQUARE_1, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
reserve a,a1,a2,a3,b,b1,b2,b3,r,s,t,u for Real;
reserve n for Nat;
reserve x0,x,x1,x2,x3,y0,y,y1,y2,y3 for Element of REAL n;
:: Preliminaries
theorem :: EUCLIDLP:1
(s/t)*(u*x)=(s*u)/t*x & (1/t)*(u*x)= u/t*x;
theorem :: EUCLIDLP:2
x - x = 0*n & x + -x = 0*n;
theorem :: EUCLIDLP:3
-a*x = (-a)*x & -a*x = a*(-x);
theorem :: EUCLIDLP:4
x1 - (x2 - x3) = x1 - x2 + x3;
theorem :: EUCLIDLP:5
x1 + (x2 - x3) = x1 + x2 - x3;
theorem :: EUCLIDLP:6
x1 = x2 + x3 iff x2 = x1 - x3;
theorem :: EUCLIDLP:7
x=x1+x2+x3 iff x-x1=x2+x3;
theorem :: EUCLIDLP:8
-(x1 + x2 + x3) = -x1 + -x2 + -x3;
theorem :: EUCLIDLP:9
x1=x2 iff x1-x2=0*n;
theorem :: EUCLIDLP:10
x1 - x0 = t*x & x1 <> x0 implies t <> 0;
theorem :: EUCLIDLP:11
(a - b)*x = a*x + (-b)*x & (a - b)*x = a*x + -b*x & (a - b)*x = a*x - b*x;
theorem :: EUCLIDLP:12
a*(x - y) = a*x + -a*y & a*(x - y) = a*x + (-a)*y & a*(x - y) = a*x - a*y;
theorem :: EUCLIDLP:13
(s - t - u)*x = s*x - t*x - u*x;
theorem :: EUCLIDLP:14
x - (a1*x1+a2*x2+a3*x3) = x + ((-a1)*x1 + (-a2)*x2 + (-a3)*x3);
theorem :: EUCLIDLP:15
x - (s+t+u)*y = x + (-s)*y + (-t)*y + (-u)*y;
theorem :: EUCLIDLP:16
(x1+x2)+(y1+y2)=(x1+y1)+(x2+y2);
theorem :: EUCLIDLP:17
(x1+x2+x3)+(y1+y2+y3)=(x1+y1)+(x2+y2)+(x3+y3);
theorem :: EUCLIDLP:18
(x1+x2)-(y1+y2)=(x1-y1)+(x2-y2);
theorem :: EUCLIDLP:19
(x1+x2+x3)-(y1+y2+y3)=(x1-y1)+(x2-y2)+(x3-y3);
theorem :: EUCLIDLP:20
a*(x1+x2+x3)=a*x1+a*x2+a*x3;
theorem :: EUCLIDLP:21
a*(b1*x1+b2*x2) = (a*b1)*x1+(a*b2)*x2;
theorem :: EUCLIDLP:22
a*(b1*x1+b2*x2+b3*x3) = (a*b1)*x1+(a*b2)*x2+(a*b3)*x3;
theorem :: EUCLIDLP:23
(a1*x1+a2*x2)+(b1*x1+b2*x2)=(a1+b1)*x1+(a2+b2)*x2;
theorem :: EUCLIDLP:24
(a1*x1+a2*x2+a3*x3)+(b1*x1+b2*x2+b3*x3)=(a1+b1)*x1+(a2+b2)*x2+( a3+b3)*x3;
theorem :: EUCLIDLP:25
(a1*x1+a2*x2)-(b1*x1+b2*x2)=(a1-b1)*x1+(a2-b2)*x2;
theorem :: EUCLIDLP:26
(a1*x1+a2*x2+a3*x3)-(b1*x1+b2*x2+b3*x3)=(a1-b1)*x1+(a2-b2)*x2+( a3-b3)*x3;
theorem :: EUCLIDLP:27
a1+a2+a3=1 implies a1*x1+a2*x2+a3*x3=x1+a2*(x2-x1)+a3*(x3-x1);
theorem :: EUCLIDLP:28
x=x1+a2*(x2-x1)+a3*(x3-x1) implies ex a1 be Real st x=a1*x1+a2*
x2+a3*x3 & a1+a2+a3=1;
theorem :: EUCLIDLP:29
for n being Nat st n >= 1 holds 1*n <> 0*n;
:: Lines
theorem :: EUCLIDLP:30
for A be Subset of REAL n,x1,x2 holds A is being_line & x1 in A
& x2 in A & x1<>x2 implies A=Line(x1,x2);
theorem :: EUCLIDLP:31
for x1, x2 being Element of REAL n holds y1 in Line(x1,x2) & y2
in Line(x1,x2) implies ex a st y2 - y1 =a*(x2 - x1);
definition
let n;
let x1,x2 be Element of REAL n;
pred x1 // x2 means
:: EUCLIDLP:def 1
x1 <> 0*n & x2 <> 0*n & ex r st x1 = r*x2;
end;
theorem :: EUCLIDLP:32
for x1,x2 be Element of REAL n st x1 // x2 holds ex a st a <> 0 & x1 = a*x2;
definition
let n;
let x1,x2 be Element of REAL n;
redefine pred x1 // x2;
symmetry;
end;
theorem :: EUCLIDLP:33
x1 // x2 & x2 // x3 implies x1 // x3;
definition
let n be Nat,x1,x2 be Element of REAL n;
pred x1,x2 are_lindependent2 means
:: EUCLIDLP:def 2
for a1,a2 being Real st a1*x1+a2* x2=0*n holds a1=0 & a2=0;
symmetry;
end;
notation
let n;
let x1,x2 be Element of REAL n;
antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2;
end;
theorem :: EUCLIDLP:34
x1,x2 are_lindependent2 implies x1<>0*n & x2<>0*n;
theorem :: EUCLIDLP:35
for x1,x2 st x1,x2 are_lindependent2 holds a1*x1+a2*x2=b1*x1+b2*
x2 implies a1=b1 & a2=b2;
theorem :: EUCLIDLP:36
for x1,x2,y1,y1 st y1,y2 are_lindependent2 & y1 = a1*x1+a2*
x2 & y2=b1*x1+b2*x2
ex c1,c2,d1,d2 be Real st x1=c1*y1+c2*y2 & x2=d1*y1 +d2*y2;
theorem :: EUCLIDLP:37
x1,x2 are_lindependent2 implies x1 <> x2;
theorem :: EUCLIDLP:38
x2 - x1,x3 - x1 are_lindependent2 implies x2 <> x3;
theorem :: EUCLIDLP:39
x1,x2 are_lindependent2 implies x1+t*x2,x2 are_lindependent2;
theorem :: EUCLIDLP:40
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
implies y1 - y0, y3 - y2 are_lindependent2;
theorem :: EUCLIDLP:41
x1 // x2 implies x1,x2 are_ldependent2 & x1 <> 0*n & x2 <> 0*n;
theorem :: EUCLIDLP:42
x1, x2 are_ldependent2 implies x1 = 0*n or x2 = 0*n or x1 // x2;
theorem :: EUCLIDLP:43
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;
definition
let n;
let x1,x2 be Element of REAL n;
pred x1 _|_ x2 means
:: EUCLIDLP:def 3
x1 <> 0*n & x2 <> 0*n & x1, x2 are_orthogonal;
symmetry;
end;
theorem :: EUCLIDLP:44
x _|_ y0 & y0 // y1 implies x _|_ y1;
theorem :: EUCLIDLP:45
x _|_ y implies x, y are_lindependent2;
theorem :: EUCLIDLP:46
x1 // x2 implies not x1 _|_ x2;
definition
let n;
func line_of_REAL n -> Subset-Family of REAL n equals
:: EUCLIDLP:def 4
the set of all Line(x1,x2) where x1,x2 is Element of REAL n;
end;
registration
let n;
cluster line_of_REAL n -> non empty;
end;
theorem :: EUCLIDLP:47
Line(x1,x2) in line_of_REAL n;
reserve L,L0,L1,L2 for Element of line_of_REAL n;
theorem :: EUCLIDLP:48
x1 in L & x2 in L implies Line(x1,x2) c= L;
theorem :: EUCLIDLP:49
L1 meets L2 iff ex x st x in L1 & x in L2;
theorem :: EUCLIDLP:50
L0 misses L1 & x in L0 implies not x in L1;
theorem :: EUCLIDLP:51
ex x1,x2 st L = Line(x1,x2);
theorem :: EUCLIDLP:52
ex x st x in L;
theorem :: EUCLIDLP:53
L is being_line implies ex x1 st x1 <> x0 & x1 in L;
theorem :: EUCLIDLP:54
(not x in L) & L is being_line implies ex x1,x2 st L = Line(x1,
x2) & x - x1 _|_ x2 - x1;
theorem :: EUCLIDLP:55
(not x in L) & L is being_line implies ex x1,x2 st L = Line(x1,
x2) & x - x1,x2 - x1 are_lindependent2;
definition
let n be Nat,x be Element of REAL n, L be Element of line_of_REAL
n;
func dist_v(x,L) -> Subset of REAL equals
:: EUCLIDLP:def 5
{|.x-x0.| where x0 is Element of
REAL n : x0 in L};
end;
definition
let n be Nat,x be Element of REAL n, L be Element of line_of_REAL
n;
func dist(x,L) -> Real equals
:: EUCLIDLP:def 6
lower_bound dist_v(x,L);
end;
theorem :: EUCLIDLP:56
L = Line(x1,x2) implies {|.x-x0.| where x0 is Element of REAL n : x0
in Line(x1,x2)} = dist_v(x,L);
theorem :: EUCLIDLP:57
ex x0 st x0 in L & |.x-x0.|=dist(x,L);
theorem :: EUCLIDLP:58
dist(x,L) >= 0;
theorem :: EUCLIDLP:59
x in L iff dist(x,L) = 0;
definition
let n;
let L1,L2;
pred L1 // L2 means
:: 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;
end;
theorem :: EUCLIDLP:60
L0 // L1 & L1 // L2 implies L0 // L2;
definition
let n;
let L1,L2;
pred L1 _|_ L2 means
:: 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;
end;
theorem :: EUCLIDLP:61
L0 _|_ L1 & L1 // L2 implies L0 _|_ L2;
theorem :: EUCLIDLP:62
(not x in L) & L is being_line implies ex L0 st x in L0 & L0 _|_
L & L0 meets L;
theorem :: EUCLIDLP:63
L1 misses L2 implies ex x st x in L1 & not x in L2;
theorem :: EUCLIDLP:64
x1 in L & x2 in L & x1 <> x2 implies Line(x1,x2) = L & L is being_line;
theorem :: EUCLIDLP:65
L1 is being_line & L1 = L2 implies L1 // L2;
theorem :: EUCLIDLP:66
L1 // L2 implies L1 is being_line & L2 is being_line;
theorem :: EUCLIDLP:67
L1 _|_ L2 implies L1 is being_line & L2 is being_line;
theorem :: EUCLIDLP:68
x in L & a<>1 & a*x in L implies 0*n in L;
theorem :: EUCLIDLP:69
x1 in L & x2 in L implies ex x3 st x3 in L & x3 - x1 = a*(x2 - x1);
theorem :: EUCLIDLP:70
x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a st x3 - x1 = a*(x2 - x1);
theorem :: EUCLIDLP:71
L1 // L2 & L1<>L2 implies L1 misses L2;
theorem :: EUCLIDLP:72
L is being_line implies ex L0 st x in L0 & L0 // L;
theorem :: EUCLIDLP:73
for x,L st (not x in L) & L is being_line holds ex L0 st x in L0 & L0
// L & L0 <> L;
theorem :: EUCLIDLP:74
for x0,x1,y0,y1,L1,L2 st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in
L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds x1 - x0 _|_ y1 - y0;
theorem :: EUCLIDLP:75
for L1,L2 st L1 _|_ L2 holds L1 <> L2;
theorem :: EUCLIDLP:76
for x1,x2,L st L is being_line & L = Line(x1,x2) holds x1 <> x2;
theorem :: EUCLIDLP:77
x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1
& L1 // L2 implies x1 - x0 // y1 - y0;
theorem :: EUCLIDLP:78
x2 - x1,x3 - x1 are_lindependent2 & y2 in Line(x1,x2) & y3 in Line(x1,
x3) & L1 = Line(x2,x3) & L2 = Line(y2,y3) implies (L1 // L2 iff ex a st a <> 0
& y2 - x1 = a*(x2 - x1) & y3 - x1 = a*(x3 - x1));
theorem :: EUCLIDLP:79
for L1,L2 st L1 is being_line & L2 is being_line & L1 <> L2
holds ex x st x in L1 & not x in L2;
theorem :: EUCLIDLP:80
for x,L1,L2 st L1 _|_ L2 holds ex L0 st x in L0 & L0 _|_ L2 & L0 // L1;
theorem :: EUCLIDLP:81
for x,L1,L2 st x in L2 & L1 _|_ L2 holds ex x0 st x <> x0 & x0
in L1 & not x0 in L2;
:: Planes
definition
let n be Nat,x1,x2,x3 be Element of REAL n;
func plane(x1,x2,x3) -> Subset of REAL n equals
:: EUCLIDLP:def 9
{x where x is Element of
REAL n: ex a1,a2,a3 being Real st a1+a2+a3=1 & x=a1*x1+a2*x2+a3*x3};
end;
registration
let n be Nat,x1,x2,x3 be Element of REAL n;
cluster plane(x1,x2,x3) -> non empty;
end;
definition
let n;
let A be Subset of REAL n;
attr A is being_plane means
:: EUCLIDLP:def 10
ex x1,x2,x3 st x2 - x1, x3 - x1 are_lindependent2 & A = plane(x1,x2,x3);
end;
theorem :: EUCLIDLP:82
x1 in plane(x1,x2,x3) & x2 in plane(x1,x2,x3) & x3 in plane(x1, x2,x3);
theorem :: EUCLIDLP:83
x1 in plane(y1,y2,y3) & x2 in plane(y1,y2,y3) & x3 in plane(y1,
y2,y3) implies plane(x1,x2,x3) c= plane(y1,y2,y3);
theorem :: EUCLIDLP:84
for A being Subset of REAL n,x,x1,x2,x3 st x in plane(x1,x2,x3) & ex
c1,c2,c3 being Real st c1 + c2 + c3 = 0 & x = c1*x1 + c2*x2 + c3*x3 holds 0*n
in plane(x1,x2,x3);
theorem :: EUCLIDLP:85
y1 in plane(x1,x2,x3) & y2 in plane(x1,x2,x3) implies Line(y1,y2
) c= plane(x1,x2,x3);
theorem :: EUCLIDLP:86
for A being Subset of REAL n,x st A is being_plane & x in A & ex a st
a<>1 & a*x in A holds 0*n in A;
theorem :: EUCLIDLP:87
x in plane(x1,x2,x3) & x = a1*x1+a2*x2+a3* x3 implies a1 + a2 + a3 = 1
or 0*n in plane(x1,x2,x3);
theorem :: EUCLIDLP:88
x in plane(x1,x2,x3) iff ex a1,a2,a3 st a1+a2+a3=1 & x = a1*x1+ a2*x2+a3*x3;
theorem :: EUCLIDLP:89
x2-x1,x3-x1 are_lindependent2 & a1 + a2 + a3 = 1 & x = a1*x1+a2*x2+a3*
x3 & b1 + b2 + b3 = 1 & x = b1*x1+b2*x2+b3*x3 implies a1 = b1 & a2 = b2 & a3 =
b3;
definition
let n;
func plane_of_REAL n -> Subset-Family of REAL n equals
:: EUCLIDLP:def 11
{P where P is Subset
of REAL n: ex x1,x2,x3 being Element of REAL n st P = plane(x1,x2,x3)};
end;
registration
let n;
cluster plane_of_REAL n -> non empty;
end;
theorem :: EUCLIDLP:90
plane(x1,x2,x3) in plane_of_REAL n;
reserve P,P0,P1,P2 for Element of plane_of_REAL n;
theorem :: EUCLIDLP:91
x1 in P & x2 in P & x3 in P implies plane(x1,x2,x3) c= P;
theorem :: EUCLIDLP:92
x1 in P & x2 in P & x3 in P & x2 - x1, x3 - x1 are_lindependent2
implies P = plane(x1,x2,x3);
theorem :: EUCLIDLP:93
P1 is being_plane & P1 c= P2 implies P1 = P2;
:: Lines in the planes
theorem :: EUCLIDLP:94
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 :: EUCLIDLP:95
x1 in P & x2 in P implies Line(x1,x2) c= P;
definition
let n be Nat,L1,L2 be Element of line_of_REAL n;
pred L1,L2 are_coplane means
:: EUCLIDLP:def 12
ex x1,x2,x3 being Element of REAL n st
L1 c= plane(x1,x2,x3) & L2 c= plane(x1,x2,x3);
end;
theorem :: EUCLIDLP:96
L1,L2 are_coplane iff ex P st L1 c= P & L2 c= P;
theorem :: EUCLIDLP:97
L1 // L2 implies L1,L2 are_coplane;
theorem :: EUCLIDLP:98
L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1
misses L2 implies ex P st L1 c= P & L2 c= P & P is being_plane;
theorem :: EUCLIDLP:99
ex P st x in P & L c= P;
theorem :: EUCLIDLP:100
(not x in L) & L is being_line implies ex P st x in P & L c= P
& P is being_plane;
theorem :: EUCLIDLP:101
x in P & L c= P & (not x in L) & L is being_line implies P is being_plane;
theorem :: EUCLIDLP:102
(not x in L) & L is being_line & x in P0 & L c= P0 & x in P1 &
L c= P1 implies P0 = P1;
theorem :: EUCLIDLP:103
L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2
implies ex P st L1 c= P & L2 c= P & P is being_plane;
theorem :: EUCLIDLP:104
for L1,L2 st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets
L2 holds ex P st L1 c= P & L2 c= P & P is being_plane;
theorem :: EUCLIDLP:105
L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 &
L1 c= P2 & L2 c= P2 implies P1 = P2;
theorem :: EUCLIDLP:106
L1 // L2 & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane;
theorem :: EUCLIDLP:107
L1 _|_ L2 & L1 meets L2 implies ex P st P is being_plane & L1 c= P & L2 c= P;
theorem :: EUCLIDLP:108
L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0
_|_ L2 & L1 _|_ L2 implies L0 = L1;
theorem :: EUCLIDLP:109
L1,L2 are_coplane & L1 _|_ L2 implies L1 meets L2;
theorem :: EUCLIDLP:110
L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0
implies L0 c= P & L0 _|_ L1;
theorem :: EUCLIDLP:111
L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2;
theorem :: EUCLIDLP:112
L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 &
L meets L0 & L meets L1 implies L meets L2;
theorem :: EUCLIDLP:113
L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1
misses L2 implies L1 // L2;
theorem :: EUCLIDLP:114
x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1, y2 - y1
are_lindependent2 implies Line(x1,x2) meets Line(y1,y2);