:: Lines on Planes in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received May 24, 2005
:: Copyright (c) 2005-2026 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;
definitions TARSKI, XXREAL_2;
equalities EUCLID, FINSEQ_2, EUCLID_4, VALUED_1;
expansions TARSKI, EUCLID_4;
theorems SQUARE_1, XBOOLE_0, XCMPLX_1, RVSUM_1, EUCLID_4, FINSEQ_1, SEQ_4,
XREAL_1, FUNCOP_1, EUCLID_2, XREAL_0;
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 Th1:
(s/t)*(u*x)=(s*u)/t*x & (1/t)*(u*x)= u/t*x
proof
thus (s/t)*(u*x) = ((s/t)*u)*x by EUCLID_4:4
.= (s*u)/t*x by XCMPLX_1:74;
thus (1/t)*(u*x) = ((1/t)*u)*x by EUCLID_4:4
.= u/t*x by XCMPLX_1:99;
end;
theorem Th2:
x - x = 0*n & x + -x = 0*n
proof
thus x - x = 0*n by RVSUM_1:37;
hence thesis;
end;
theorem Th3:
-a*x = (-a)*x & -a*x = a*(-x)
proof
thus -a*x = ((-1)*a)*x by EUCLID_4:4
.= (-a)*x;
hence -a*x = (a*(-1))*x .= a*(-x) by EUCLID_4:4;
end;
theorem Th4:
x1 - (x2 - x3) = x1 - x2 + x3
proof
thus x1 - (x2 - x3) = x1 - x2 - -x3 by RVSUM_1:39
.= x1 - x2 + x3;
end;
theorem Th5:
x1 + (x2 - x3) = x1 + x2 - x3
proof
thus x1 + (x2 - x3) = x1 + x2 + -x3 by RVSUM_1:15
.= x1 + x2 - x3;
end;
theorem Th6:
x1 = x2 + x3 iff x2 = x1 - x3
proof
thus x1 = x2 + x3 implies x2 = x1 - x3
proof
assume x1 = x2 + x3;
hence x1 - x3 = x2 + (x3 + -x3) by RVSUM_1:15
.= x2 + 0*n by Th2
.= x2 by EUCLID_4:1;
end;
now
assume x2 = x1 - x3;
hence x2 + x3 = x1 + (-x3 + x3) by RVSUM_1:15
.= x1 + 0*n by Th2
.= x1 by EUCLID_4:1;
end;
hence thesis;
end;
theorem Th7:
x=x1+x2+x3 iff x-x1=x2+x3
proof
thus x=x1+x2+x3 implies x-x1=x2+x3
proof
assume x=x1+x2+x3;
then x = x1 + (x2 + x3) by RVSUM_1:15;
hence thesis by Th6;
end;
now
assume x-x1=x2+x3;
hence x = x1 + (x2 + x3) by Th6
.= x1 + x2 + x3 by RVSUM_1:15;
end;
hence thesis;
end;
theorem Th8:
-(x1 + x2 + x3) = -x1 + -x2 + -x3
proof
thus -(x1+x2+x3) = 0*n -(x1+x2+x3) by RVSUM_1:33
.= 0*n - (x1+x2) - x3 by RVSUM_1:39
.= 0*n - x1 - x2 - x3 by RVSUM_1:39
.= -x1 + -x2 + -x3 by RVSUM_1:33;
end;
Lm1: x1<>x2 implies |.x1-x2.|<>0
proof
now
assume that
A1: x1<>x2 and
A2: not |.x1-x2.| <> 0;
|(x1-x2,x1-x2)| = 0 by A2,EUCLID_4:16;
then x1 - x2 = 0*n by EUCLID_4:17;
then x1 = x2 + 0*n by Th6
.= x2 by EUCLID_4:1;
hence contradiction by A1;
end;
hence thesis;
end;
theorem Th9:
x1=x2 iff x1-x2=0*n
proof
thus x1 = x2 implies x1 - x2 = 0*n by Th2;
assume x1 - x2 = 0*n;
hence x1 = x2 + 0*n by Th6
.= x2 by EUCLID_4:1;
end;
theorem Th10:
x1 - x0 = t*x & x1 <> x0 implies t <> 0
proof
assume that
A1: x1 - x0 = t*x and
A2: x1 <> x0;
assume not t <> 0;
then x1 - x0 = 0*n by A1,EUCLID_4:3;
hence contradiction by A2,Th9;
end;
theorem Th11:
(a - b)*x = a*x + (-b)*x & (a - b)*x = a*x + -b*x & (a - b)*x = a*x - b*x
proof
thus
A1: (a - b)*x = (a + -b)*x .= a*x + (-b)*x by EUCLID_4:7;
hence (a - b)*x = a*x + -b*x by Th3;
thus thesis by A1,Th3;
end;
theorem Th12:
a*(x - y) = a*x + -a*y & a*(x - y) = a*x + (-a)*y & a*(x - y) = a*x - a*y
proof
thus
A1: a*(x - y) = a*x + a*(-y) by EUCLID_4:6
.= a*x + -a*y by Th3;
hence a*(x - y) = a*x + (-a)*y by Th3;
thus thesis by A1;
end;
theorem Th13:
(s - t - u)*x = s*x - t*x - u*x
proof
thus (s - t - u)*x = (s - t)*x - u*x by Th11
.= s*x - t*x - u*x by Th11;
end;
theorem Th14:
x - (a1*x1+a2*x2+a3*x3) = x + ((-a1)*x1 + (-a2)*x2 + (-a3)*x3)
proof
thus x - (a1*x1+a2*x2+a3*x3) = x + (-a1*x1 + -a2*x2 + -a3*x3) by Th8
.= x + ((-a1)*x1 + -a2*x2 + -a3*x3) by Th3
.= x + ((-a1)*x1 + (-a2)*x2 + -a3*x3) by Th3
.= x + ((-a1)*x1 + (-a2)*x2 + (-a3)*x3) by Th3;
end;
theorem
x - (s+t+u)*y = x + (-s)*y + (-t)*y + (-u)*y
proof
thus x - (s+t+u)*y = x - ((s+t)*y + u*y) by EUCLID_4:7
.= x - (s*y + t*y + u*y) by EUCLID_4:7
.= x + ((-s)*y + (-t)*y + (-u)*y) by Th14
.= x + ((-s)*y + (-t)*y) + (-u)*y by RVSUM_1:15
.= x + (-s)*y + (-t)*y + (-u)*y by RVSUM_1:15;
end;
theorem Th16:
(x1+x2)+(y1+y2)=(x1+y1)+(x2+y2)
proof
thus (x1+x2)+(y1+y2) = (x1+x2)+y1+y2 by RVSUM_1:15
.= (x1+y1)+x2+y2 by RVSUM_1:15
.= (x1+y1)+(x2+y2) by RVSUM_1:15;
end;
theorem Th17:
(x1+x2+x3)+(y1+y2+y3)=(x1+y1)+(x2+y2)+(x3+y3)
proof
thus (x1+x2+x3)+(y1+y2+y3) = ((x1+x2)+(y1+y2))+(x3+y3) by Th16
.= (x1+y1)+(x2+y2)+(x3+y3) by Th16;
end;
theorem Th18:
(x1+x2)-(y1+y2)=(x1-y1)+(x2-y2)
proof
thus (x1+x2)-(y1+y2) = (x1 + x2) - y1 - y2 by RVSUM_1:39
.= (x1 + x2) + (-y1+ -y2) by RVSUM_1:15
.= (x1 - y1) + (x2 - y2) by Th16;
end;
theorem
(x1+x2+x3)-(y1+y2+y3)=(x1-y1)+(x2-y2)+(x3-y3)
proof
thus (x1+x2+x3)-(y1+y2+y3) = ((x1+x2) - (y1+y2))+ (x3 - y3) by Th18
.= (x1 - y1) + (x2 - y2) + (x3 - y3) by Th18;
end;
theorem Th20:
a*(x1+x2+x3)=a*x1+a*x2+a*x3
proof
thus a*(x1+x2+x3) = a*(x1+x2)+a*x3 by EUCLID_4:6
.= a*x1+a*x2+a*x3 by EUCLID_4:6;
end;
theorem Th21:
a*(b1*x1+b2*x2) = (a*b1)*x1+(a*b2)*x2
proof
thus a*(b1*x1+b2*x2) = a*(b1*x1)+a*(b2*x2) by EUCLID_4:6
.= (a*b1)*x1+a*(b2*x2) by EUCLID_4:4
.= (a*b1)*x1+(a*b2)*x2 by EUCLID_4:4;
end;
theorem Th22:
a*(b1*x1+b2*x2+b3*x3) = (a*b1)*x1+(a*b2)*x2+(a*b3)*x3
proof
thus a*(b1*x1+b2*x2+b3*x3) = a*(b1*x1)+a*(b2*x2)+a*(b3*x3) by Th20
.= (a*b1)*x1+a*(b2*x2)+a*(b3*x3) by EUCLID_4:4
.= (a*b1)*x1+(a*b2)*x2+a*(b3*x3) by EUCLID_4:4
.= (a*b1)*x1+(a*b2)*x2+(a*b3)*x3 by EUCLID_4:4;
end;
theorem Th23:
(a1*x1+a2*x2)+(b1*x1+b2*x2)=(a1+b1)*x1+(a2+b2)*x2
proof
thus (a1*x1+a2*x2)+(b1*x1+b2*x2) = (a1*x1+b1*x1)+(a2*x2+b2*x2) by Th16
.= (a1+b1)*x1+(a2*x2+b2*x2) by EUCLID_4:7
.= (a1+b1)*x1+(a2+b2)*x2 by EUCLID_4:7;
end;
theorem Th24:
(a1*x1+a2*x2+a3*x3)+(b1*x1+b2*x2+b3*x3)=(a1+b1)*x1+(a2+b2)*x2+( a3+b3)*x3
proof
thus (a1*x1+a2*x2+a3*x3)+(b1*x1+b2*x2+b3*x3) = ((a1*x1+a2*x2)+(b1*x1+b2*x2))
+(a3*x3+b3*x3) by Th16
.= (a1+b1)*x1+(a2+b2)*x2+(a3*x3+b3*x3) by Th23
.= (a1+b1)*x1+(a2+b2)*x2+(a3+b3)*x3 by EUCLID_4:7;
end;
theorem Th25:
(a1*x1+a2*x2)-(b1*x1+b2*x2)=(a1-b1)*x1+(a2-b2)*x2
proof
thus (a1*x1+a2*x2)-(b1*x1+b2*x2) = (a1*x1-b1*x1)+(a2*x2-b2*x2) by Th18
.= (a1-b1)*x1+(a2*x2-b2*x2) by Th11
.= (a1-b1)*x1+(a2-b2)*x2 by Th11;
end;
theorem Th26:
(a1*x1+a2*x2+a3*x3)-(b1*x1+b2*x2+b3*x3)=(a1-b1)*x1+(a2-b2)*x2+( a3-b3)*x3
proof
thus (a1*x1+a2*x2+a3*x3)-(b1*x1+b2*x2+b3*x3) = ((a1*x1+a2*x2)-(b1*x1+b2*x2))
+(a3*x3-b3*x3) by Th18
.= ((a1-b1)*x1+(a2-b2)*x2)+(a3*x3-b3*x3) by Th25
.= (a1-b1)*x1+(a2-b2)*x2+(a3-b3)*x3 by Th11;
end;
theorem Th27:
a1+a2+a3=1 implies a1*x1+a2*x2+a3*x3=x1+a2*(x2-x1)+a3*(x3-x1)
proof
assume a1+a2+a3=1;
then a1=1-a2-a3;
hence a1*x1+a2*x2+a3*x3 = 1 * x1 - a2*x1 - a3*x1 + a2*x2 + a3*x3 by Th13
.= x1 + -a2*x1 - a3*x1 + a2*x2 + a3*x3 by EUCLID_4:3
.= x1 + -a2*x1 + a2*x2 + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + (a3*x3 + -a3*x1) by RVSUM_1:15
.= x1 + a2*(x2-x1) + (a3*x3 + -a3*x1) by Th12
.= x1 + a2*(x2-x1) + a3*(x3-x1) by Th12;
end;
theorem Th28:
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
proof
assume
A1: x=x1+a2*(x2-x1)+a3*(x3-x1);
reconsider a1 = 1-a2-a3 as Real;
take a1;
a1*x1+a2*x2+a3*x3 = 1 * x1 - a2*x1 - a3*x1 + a2*x2 + a3*x3 by Th13
.= x1 + -a2*x1 - a3*x1 + a2*x2 + a3*x3 by EUCLID_4:3
.= x1 + -a2*x1 + a2*x2 + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + (a3*x3 + -a3*x1) by RVSUM_1:15
.= x1 + a2*(x2-x1) + (a3*x3 + -a3*x1) by Th12
.= x by A1,Th12;
hence thesis;
end;
theorem
for n being Nat st n >= 1 holds 1*n <> 0*n
proof
let n be Nat;
assume n >= 1;
then
A1: 1 in Seg n by FINSEQ_1:1;
assume
A2: 1*n = 0*n;
1*n = n|->1 & (n|->0).1 = 0 by A1,FUNCOP_1:7;
hence contradiction by A2,A1,FUNCOP_1:7;
end;
:: Lines
theorem Th30:
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)
proof
let A be Subset of REAL n;
let x1,x2;
assume that
A1: A is being_line and
A2: x1 in A & x2 in A & x1<>x2;
ex y1,y2 st y1<>y2 & A=Line(y1,y2) by A1;
then Line(x1,x2) c= A & A c= Line(x1,x2) by A2,EUCLID_4:10,11;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th31:
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)
proof
let x1, x2 be Element of REAL n;
assume y1 in Line(x1,x2);
then consider t such that
A1: y1 = (1-t)*x1 + t*x2;
assume y2 in Line(x1,x2);
then consider s such that
A2: y2 = (1-s)*x1 + s*x2;
take s - t;
y2 - y1 = (1-s)*x1 + s*x2 - (1-t)*x1 - t*x2 by A1,A2,RVSUM_1:39
.= s*x2 + (1-s)*x1 +- t*x2 +- (1-t)*x1 by RVSUM_1:15
.= s*x2 + - t*x2 + (1-s)*x1 +- (1-t)*x1 by RVSUM_1:15
.= (s - t)*x2 + (1-s)*x1 +- (1-t)*x1 by Th11
.= (s - t)*x2 + ((1-s)*x1 +- (1-t)*x1) by RVSUM_1:15
.= (s - t)*x2 + ((1-s)- (1-t))*x1 by Th11
.= (s - t)*x2 + (-(s - t))*x1
.= (s - t)*(x2 - x1) by Th12;
hence thesis;
end;
definition
let n;
let x1,x2 be Element of REAL n;
pred x1 // x2 means
:Def1:
x1 <> 0*n & x2 <> 0*n & ex r st x1 = r*x2;
end;
theorem Th32:
for x1,x2 be Element of REAL n st x1 // x2 holds ex a st a <> 0 & x1 = a*x2
proof
let x1,x2 being Element of REAL n;
assume
A1: x1 // x2;
then consider a such that
A2: x1 = a*x2;
x1 <> 0*n by A1;
then a <> 0 by A2,EUCLID_4:3;
hence thesis by A2;
end;
definition
let n;
let x1,x2 be Element of REAL n;
redefine pred x1 // x2; :: redefines // (EUCLIDLP, definition)
symmetry
proof
let x1,x2 being Element of REAL n;
assume
A1: x1 // x2;
then
A2: x1 <> 0*n & x2 <> 0*n;
consider a such that
A3: a <> 0 and
A4: x1 = a*x2 by A1,Th32;
(1/a)*x1 = (a/a)*x2 by A4,Th1
.= (1)*x2 by A3,XCMPLX_1:60
.= x2 by EUCLID_4:3;
hence thesis by A2;
end;
end;
theorem Th33:
x1 // x2 & x2 // x3 implies x1 // x3
proof
assume that
A1: x1 // x2 and
A2: x2 // x3;
A3: ex t st x1 = t*x3
proof
consider b such that
A4: x2 = b*x3 by A2;
consider a such that
A5: x1 = a*x2 by A1;
x1 = (a*b)*x3 by A5,A4,EUCLID_4:4;
hence thesis;
end;
x1 <> 0*n & x3 <> 0*n by A1,A2;
hence thesis by A3;
end;
definition
let n be Nat,x1,x2 be Element of REAL n;
pred x1,x2 are_lindependent2 means
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;
Lm2: x1,x2 are_lindependent2 implies x1<>0*n
proof
assume that
A1: x1,x2 are_lindependent2 and
A2: not x1<>0*n;
1 * x1 = 0*n by A2,EUCLID_4:2;
then 1 * x1 + 0 * x2 = 0*n + 0*n by EUCLID_4:3
.= 0*n by EUCLID_4:1;
hence contradiction by A1;
end;
theorem
x1,x2 are_lindependent2 implies x1<>0*n & x2<>0*n by Lm2;
theorem Th35:
for x1,x2 st x1,x2 are_lindependent2 holds a1*x1+a2*x2=b1*x1+b2*
x2 implies a1=b1 & a2=b2
proof
let x1,x2;
assume
A1: x1,x2 are_lindependent2;
assume
A2: a1*x1+a2*x2=b1*x1+b2*x2;
0*n = (a1*x1+a2*x2) - (a1*x1+a2*x2) by Th2
.= (a1-b1)*x1 + (a2-b2)*x2 by A2,Th25;
then a1 - b1 = 0 & a2 - b2 = 0 by A1;
hence thesis;
end;
theorem Th36:
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
proof
let x1,x2,y1,y1;
assume
A1: y1,y2 are_lindependent2;
assume that
A2: y1 = a1*x1+a2*x2 and
A3: y2=b1*x1+b2*x2;
A4: -b1*y1+a1*y2 = (-b1)*(a1*x1+a2*x2) + a1*(b1*x1+b2*x2) by A2,A3,Th3
.= ((-b1)*a1)*x1+((-b1)*a2)*x2 + a1*(b1*x1+b2*x2) by Th21
.= (-a1*b1)*x1+(-a2*b1)*x2 + ((a1*b1)*x1+(a1*b2)*x2) by Th21
.= (-a1*b1 + a1*b1)*x1+(-a2*b1 + a1*b2)*x2 by Th23
.= 0*n + (-a2*b1+a1*b2)*x2 by EUCLID_4:3
.= (a1*b2 - a2*b1)*x2 by EUCLID_4:1;
A5: b2*y1-a2*y2 = ((a1*b2)*x1+(a2*b2)*x2) - a2*(b1*x1+b2*x2) by A2,A3,Th21
.= ((a1*b2)*x1+(a2*b2)*x2) - ((a2*b1)*x1+(a2*b2)*x2) by Th21
.= (a1*b2-a2*b1)*x1+(a2*b2-a2*b2)*x2 by Th25
.= (a1*b2-a2*b1)*x1 + 0*n by EUCLID_4:3
.= (a1*b2-a2*b1)*x1 by EUCLID_4:1;
A6: a1*b2-a2*b1<>0
proof
assume not a1*b2-a2*b1<>0;
then
A7: b2*y1+(-a2)*y2 = 0 * x1 by A5,Th3
.= 0*n by EUCLID_4:3;
then
A8: y2 = b1*x1 + 0 * x2 by A1,A3
.= b1*x1 + 0*n by EUCLID_4:3
.= b1*x1 by EUCLID_4:1;
A9: -a2=0 by A1,A7;
then y1 = a1*x1 + 0*n by A2,EUCLID_4:3
.= a1*x1 by EUCLID_4:1;
then b1*y1+(-a1)*y2 = (a1*b1)*x1 + (-a1)*(b1*x1) by A8,EUCLID_4:4
.= (a1*b1)*x1 + ((-a1)*b1)*x1 by EUCLID_4:4
.= (a1*b1+(-a1)*b1)*x1 by EUCLID_4:7
.= 0*n by EUCLID_4:3;
then -a1=0 by A1;
then y1 = 0*n + 0 * x2 by A2,A9,EUCLID_4:3
.= 0*n + 0*n by EUCLID_4:3
.= 0*n by EUCLID_4:1;
hence contradiction by A1,Lm2;
end;
A10: x2 = 1 * x2 by EUCLID_4:3
.= (1/(a1*b2-a2*b1)*(a1*b2-a2*b1))*x2 by A6,XCMPLX_1:106
.= 1/(a1*b2-a2*b1)*((a1*b2-a2*b1)*x2) by EUCLID_4:4
.= 1/(a1*b2-a2*b1)*(-b1*y1)+1/(a1*b2-a2*b1)*(a1*y2) by A4,EUCLID_4:6
.= 1/(a1*b2-a2*b1)*((-b1)*y1)+1/(a1*b2-a2*b1)*(a1*y2) by Th3
.= (-b1)/(a1*b2-a2*b1)*y1+1/(a1*b2-a2*b1)*(a1*y2) by Th1
.= (-b1)/(a1*b2-a2*b1)*y1+a1/(a1*b2-a2*b1)*y2 by Th1;
set d2 = a1/(a1*b2-a2*b1);
set d1 = (-b1)/(a1*b2-a2*b1);
set c2 = (-a2)/(a1*b2-a2*b1);
set c1 = b2/(a1*b2-a2*b1);
take c1,c2,d1,d2;
x1 = 1 * x1 by EUCLID_4:3
.= (1/(a1*b2-a2*b1)*(a1*b2-a2*b1))*x1 by A6,XCMPLX_1:106
.= 1/(a1*b2-a2*b1)*((a1*b2-a2*b1)*x1) by EUCLID_4:4
.= 1/(a1*b2-a2*b1)*(b2*y1)-1/(a1*b2-a2*b1)*(a2*y2) by A5,Th12
.= b2/(a1*b2-a2*b1)*y1-1/(a1*b2-a2*b1)*(a2*y2) by Th1
.= b2/(a1*b2-a2*b1)*y1+-(1/(a1*b2-a2*b1)*a2)*y2 by EUCLID_4:4
.= b2/(a1*b2-a2*b1)*y1+(-1/(a1*b2-a2*b1)*a2)*y2 by Th3
.= b2/(a1*b2-a2*b1)*y1+(1/(a1*b2-a2*b1)*(-a2))*y2
.= b2/(a1*b2-a2*b1)*y1+(-a2)/(a1*b2-a2*b1)*y2 by XCMPLX_1:99;
hence thesis by A10;
end;
theorem Th37:
x1,x2 are_lindependent2 implies x1 <> x2
proof
assume
A1: x1,x2 are_lindependent2;
assume
A2: x1 = x2;
1 * x1 + (-1) * x2 = 1 * (x1 - x2) by Th12
.= 1 * 0*n by A2,Th2
.= 0*n by EUCLID_4:2;
hence contradiction by A1;
end;
theorem
x2 - x1,x3 - x1 are_lindependent2 implies x2 <> x3 by Th37;
theorem
x1,x2 are_lindependent2 implies x1+t*x2,x2 are_lindependent2
proof
assume
A1: x1,x2 are_lindependent2;
for a,b being Real st a*(x1+t*x2)+b*x2=0*n holds a=0 & b=0
proof
let a,b;
assume a*(x1+t*x2)+b*x2=0*n;
then
A2: 0*n = a*(1 *x1+t*x2)+b*x2 by EUCLID_4:3
.= (a*1)*x1+(a*t)*x2+b*x2 by Th21
.= a*x1+((a*t)*x2+b*x2) by RVSUM_1:15
.= a*x1+(a*t+b)*x2 by EUCLID_4:7;
then a= 0 by A1;
hence thesis by A1,A2;
end;
hence thesis;
end;
theorem Th40:
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
proof
assume that
A1: x1 - x0, x3 - x2 are_lindependent2 and
A2: y0 in Line(x0,x1) & y1 in Line(x0,x1) and
A3: y0 <> y1 and
A4: y2 in Line(x2,x3) & y3 in Line(x2,x3) and
A5: y2 <> y3;
consider s being Real such that
A6: y1 - y0 = s*(x1 - x0) by A2,Th31;
consider t being Real such that
A7: y3 - y2 = t*(x3 - x2) by A4,Th31;
for a,b st a*(y1 - y0)+b*(y3 - y2)=0*n holds a=0 & b=0
proof
let a,b;
assume a*(y1 - y0)+b*(y3 - y2)=0*n;
then
A8: 0*n = (a*s)*(x1 - x0)+b*(t*(x3 - x2)) by A6,A7,EUCLID_4:4
.= (a*s)*(x1 - x0)+(b*t)*(x3 - x2) by EUCLID_4:4;
then
A9: a*s= 0 by A1;
A10: b*t= 0 by A1,A8;
A11: b = b*t/t by A5,A7,Th10,XCMPLX_1:89
.= 0 by A10;
a = a*s/s by A3,A6,Th10,XCMPLX_1:89
.= 0 by A9;
hence thesis by A11;
end;
hence thesis;
end;
Lm3: x1 // x2 implies x1,x2 are_ldependent2
proof
assume x1 // x2;
then consider r being Real such that
A1: x1 = r*x2;
assume
A2: x1,x2 are_lindependent2;
0*n = x1 - x1 by Th2
.= 1 * x1 + -r*x2 by A1,EUCLID_4:3
.= 1 * x1 + (-r)*x2 by Th3;
hence contradiction by A2;
end;
theorem
x1 // x2 implies x1,x2 are_ldependent2 & x1 <> 0*n & x2 <> 0*n by Lm3;
Lm4: x1, x2 are_ldependent2 & x1 <> 0*n & x2 <> 0*n implies x1 // x2
proof
assume that
A1: x1, x2 are_ldependent2 and
A2: x1 <> 0*n & x2 <> 0*n;
consider a1,a2 being Real such that
A3: a1*x1+a2*x2=0*n and
A4: a1<>0 or a2<>0 by A1;
now
per cases by A4;
case
A5: a1<>0;
set t = (-a2)/a1;
take t;
A6: a1*x1 = 0*n - a2*x2 by A3,Th6
.= -a2*x2 by RVSUM_1:33;
x1 = 1 * x1 by EUCLID_4:3
.= (a1/a1)*x1 by A5,XCMPLX_1:60
.= 1/a1*(a1*x1) by Th1
.= 1/a1*((-a2)*x2) by A6,Th3
.= (-a2)/a1*x2 by Th1;
hence thesis by A2;
end;
case
A7: a2<>0;
set s = (-a1)/a2;
take s;
A8: a2*x2 = 0*n - a1*x1 by A3,Th6
.= -a1*x1 by RVSUM_1:33;
x2 = 1 * x2 by EUCLID_4:3
.= (a2/a2)*x2 by A7,XCMPLX_1:60
.= 1/a2*(a2*x2) by Th1
.= 1/a2*((-a1)*x1) by A8,Th3
.= (-a1)/a2*x1 by Th1;
hence thesis by A2,Def1;
end;
end;
hence thesis;
end;
theorem
x1, x2 are_ldependent2 implies x1 = 0*n or x2 = 0*n or x1 // x2 by Lm4;
theorem Th43:
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
proof
let x1,x2,y1 being Element of REAL n;
now
per cases;
case
A1: x1<>x2;
set mu = - |(x1-x2,y1-x1)|/|.x1-x2.|^2;
set y2 = (1-mu)*x1 + mu*x2;
|.x1-x2.|<>0 by A1,Lm1;
then
A2: |.x1-x2.|^2 <> 0 by SQUARE_1:12;
|(x1-x2,y1-y2)| = |(x1-x2,y1 - (1 + -mu)*x1 - mu*x2)| by RVSUM_1:39
.= |(x1-x2,y1 - (1 *x1 + (-mu)*x1) - mu*x2)| by EUCLID_4:7
.= |(x1-x2,y1-1 *x1-(-mu)*x1-mu*x2)| by RVSUM_1:39
.= |(x1-x2,(y1-x1)-(-mu)*x1-mu*x2)| by EUCLID_4:3
.= |(x1-x2,(y1-x1)-((-mu)*x1+mu*x2))| by RVSUM_1:39
.= |(x1-x2,(y1-x1)-((-mu)*x1+ (-(-mu)*x2)))| by Th3
.= |(x1-x2,(y1-x1)-((-mu)*x1+ (-mu)*(-x2)))| by Th3
.= |(x1-x2,(y1-x1)-(-mu)*(x1 -x2))| by EUCLID_4:6
.= |(x1-x2,y1-x1)| - |(x1-x2,(-mu)*(x1-x2))| by EUCLID_4:26
.= |(x1-x2,y1-x1)| - (-mu)*|(x1-x2,x1-x2)| by EUCLID_4:21
.= |(x1-x2,y1-x1)| + mu*|(x1-x2,x1-x2)|
.= |(x1-x2,y1-x1)| + mu*|.x1-x2.|^2 by EUCLID_2:4
.= |(x1-x2,y1-x1)| + (- |(x1-x2,y1-x1)|)/|.x1-x2.|^2*|.x1-x2.|^2 by
XCMPLX_1:187
.= |(x1-x2,y1-x1)| + (- |(x1-x2,y1-x1)|) by A2,XCMPLX_1:87
.= 0;
hence y2 in Line(x1,x2) & x1-x2,y1-y2 are_orthogonal by RVSUM_1:def 17;
end;
case
A3: x1=x2;
let mu be Real;
set y2 = (1-mu)*x1 + mu*x2;
take y2;
x1 - x2 = 0*n by A3,Th2;
then |(x1-x2,y1-y2)| = 0 by EUCLID_4:18;
hence y2 in Line(x1,x2) & x1-x2,y1-y2 are_orthogonal by RVSUM_1:def 17;
end;
end;
hence thesis;
end;
definition
let n;
let x1,x2 be Element of REAL n;
pred x1 _|_ x2 means
x1 <> 0*n & x2 <> 0*n & x1, x2 are_orthogonal;
symmetry;
end;
theorem Th44:
x _|_ y0 & y0 // y1 implies x _|_ y1
proof
assume that
A1: x _|_ y0 and
A2: y0 // y1;
A3: x,y0 are_orthogonal by A1;
consider r such that
A4: y1 = r * y0 by A2,Def1;
|(x,y1)| = r*|(x,y0)| by A4,EUCLID_4:22
.= r * 0 by A3,RVSUM_1:def 17
.= 0;
then
A5: x,y1 are_orthogonal by RVSUM_1:def 17;
x <> 0*n & y1 <> 0*n by A1,A2;
hence thesis by A5;
end;
theorem Th45:
x _|_ y implies x, y are_lindependent2
proof
assume
A1: x _|_ y;
then x, y are_orthogonal;
then
A2: |(x,y)|=0 by RVSUM_1:def 17;
x <> 0*n by A1;
then |(x,x)|<>0 by EUCLID_4:17;
then
A3: |(x,x)|>0 by RVSUM_1:119;
y <> 0*n by A1;
then
A4: |(y,y)|<>0 by EUCLID_4:17;
then
A5: |(y,y)|>0 by RVSUM_1:119;
for a,b st a*x+b*y=0*n holds a=0 & b=0
proof
let a,b;
assume a*x+b*y=0*n;
then
A6: 0 = |(a*x+b*y,a*x+b*y)| by EUCLID_4:17
.= |(a*x,a*x)|+2*|(a*x,b*y)|+|(b*y,b*y)| by EUCLID_4:32
.= a*|(x,a*x)|+2*|(a*x,b*y)|+|(b*y,b*y)| by EUCLID_4:21
.= a*|(x,a*x)|+2*(a*|(x,b*y)|)+|(b*y,b*y)| by EUCLID_4:21
.= a*|(x,a*x)|+2*a*|(x,b*y)|+b*|(y,b*y)| by EUCLID_4:21
.= a*(a*|(x,x)|)+2*a*|(x,b*y)|+b*|(y,b*y)| by EUCLID_4:22
.= a*a*|(x,x)|+2*a*(b*|(x,y)|)+b*|(y,b*y)| by EUCLID_4:22
.= a*a*|(x,x)|+2*a*b*|(x,y)|+b*(b*|(y,y)|) by EUCLID_4:22
.= a*a*|(x,x)| + b*b*|(y,y)| by A2;
A7: b*b >= 0 by XREAL_1:63;
A8: a*a = 0
proof
assume a*a <> 0;
then a*a > 0 by XREAL_1:63;
then a*a*|(x,x)| > 0 by A3,XREAL_1:129;
hence contradiction by A5,A6,A7;
end;
then b*b = 0 by A4,A6,XCMPLX_1:6;
hence thesis by A8,XCMPLX_1:6;
end;
hence thesis;
end;
theorem
x1 // x2 implies not x1 _|_ x2
proof
assume
A1: x1 // x2;
then consider r such that
A2: x1 = r * x2;
x2 <> 0*n by A1;
then
A3: |(x2,x2)| <> 0 by EUCLID_4:17;
x1 <> 0*n by A1;
then
A4: r <> 0 by A2,EUCLID_4:3;
|(x1,x2)| = r*|(x2,x2)| by A2,EUCLID_4:21;
then |(x1,x2)| <> 0 by A4,A3,XCMPLX_1:6;
then not x1,x2 are_orthogonal by RVSUM_1:def 17;
hence thesis;
end;
definition
let n;
func line_of_REAL n -> Subset-Family of REAL n equals
the set of all Line(x1,x2) where x1,x2 is Element of REAL n;
correctness
proof
set A = the set of all Line(x1,x2) where x1,x2 is Element of REAL n;
A c= bool REAL n
proof
let L be object;
assume L in A;
then ex x1,x2 being Element of REAL n st L = Line(x1,x2);
hence thesis;
end;
hence thesis;
end;
end;
registration
let n;
cluster line_of_REAL n -> non empty;
coherence
proof
reconsider L = Line(0*n,1*n) as Subset of REAL n;
L in line_of_REAL n;
hence thesis;
end;
end;
theorem Th47:
Line(x1,x2) in line_of_REAL n;
reserve L,L0,L1,L2 for Element of line_of_REAL n;
theorem Th48:
x1 in L & x2 in L implies Line(x1,x2) c= L
proof
L in line_of_REAL n;
then ex y1,y2 being Element of REAL n st L = Line(y1,y2);
hence thesis by EUCLID_4:10;
end;
theorem Th49:
L1 meets L2 iff ex x st x in L1 & x in L2
proof
thus L1 meets L2 implies ex x st x in L1 & x in L2
proof
assume L1 meets L2;
then consider x being object such that
A1: x in L1 and
A2: x in L2 by XBOOLE_0:3;
reconsider x as Element of REAL n by A1;
take x;
thus thesis by A1,A2;
end;
thus thesis by XBOOLE_0:3;
end;
theorem
L0 misses L1 & x in L0 implies not x in L1 by Th49;
theorem Th51:
ex x1,x2 st L = Line(x1,x2)
proof
L in line_of_REAL n;
then consider x1,x2 being Element of REAL n such that
A1: L = Line(x1,x2);
take x1, x2;
thus thesis by A1;
end;
theorem Th52:
ex x st x in L
proof
consider x1,x2 such that
A1: L = Line(x1,x2) by Th51;
take x1;
thus thesis by A1,EUCLID_4:9;
end;
theorem Th53:
L is being_line implies ex x1 st x1 <> x0 & x1 in L
proof
assume L is being_line;
then consider y1,y2 such that
A1: y1 in L and
A2: y2 in L & y1 <> y2 by EUCLID_4:13;
now
per cases;
case
A3: y1 = x0;
take y2;
thus y2 <> x0 & y2 in L by A2,A3;
end;
case
A4: y1 <> x0;
take y1;
thus y1 <> x0 & y1 in L by A1,A4;
end;
end;
hence thesis;
end;
theorem Th54:
(not x in L) & L is being_line implies ex x1,x2 st L = Line(x1,
x2) & x - x1 _|_ x2 - x1
proof
assume that
A1: not x in L and
A2: L is being_line;
consider y0,y1 such that
A3: y0 <> y1 and
A4: L = Line(y0,y1) by A2;
A5: y0 - y1 <> 0*n by A3,Th9;
consider x1 being Element of REAL n such that
A6: x1 in Line(y0,y1) and
A7: y0 - y1,x - x1 are_orthogonal by Th43;
x - x1 <> 0*n by A1,A4,A6,Th9;
then
A8: y0 - y1 _|_ x - x1 by A7,A5;
take x1;
consider x2 being Element of REAL n such that
A9: x1 <> x2 and
A10: x2 in L by A2,EUCLID_4:14;
take x2;
A11: x2 - x1 <> 0*n by A9,Th9;
ex a being Real st x2 - x1 = a*(y0 - y1) by A4,A6,A10,Th31;
then x2 - x1 // y0 - y1 by A5,A11;
hence thesis by A2,A4,A6,A8,A9,A10,Th30,Th44;
end;
theorem Th55:
(not x in L) & L is being_line implies ex x1,x2 st L = Line(x1,
x2) & x - x1,x2 - x1 are_lindependent2
proof
assume ( not x in L)& L is being_line;
then consider x1,x2 such that
A1: L = Line(x1,x2) & x - x1 _|_ x2 - x1 by Th54;
take x1;
take x2;
thus thesis by A1,Th45;
end;
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
{|.x-x0.| where x0 is Element of
REAL n : x0 in L};
correctness
proof
set A = {|.x-x0.| where x0 is Element of REAL n : x0 in L};
A c= REAL
proof
let r be object;
assume r in A;
then ex x0 be Element of REAL n st r = |.x - x0.| & x0 in L;
hence thesis by XREAL_0:def 1;
end;
hence thesis;
end;
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
lower_bound dist_v(x,L);
correctness;
end;
theorem
L = Line(x1,x2) implies {|.x-x0.| where x0 is Element of REAL n : x0
in Line(x1,x2)} = dist_v(x,L);
theorem Th57:
ex x0 st x0 in L & |.x-x0.|=dist(x,L)
proof
consider x1,x2 being Element of REAL n such that
A1: L = Line(x1,x2) by Th51;
{|.x-x9.| where x9 is Element of REAL n : x9 in Line(x1,x2)} = dist_v(x,
L) by A1;
then reconsider
R = {|.x-x9.| where x9 is Element of REAL n : x9 in Line(x1,x2)}
as Subset of REAL;
consider x0 being Element of REAL n such that
A2: x0 in Line(x1,x2) & |.x-x0.|=lower_bound R and
x1-x2,x-x0 are_orthogonal by EUCLID_4:40;
take x0;
thus thesis by A1,A2;
end;
theorem
dist(x,L) >= 0
proof
ex x0 being Element of REAL n st x0 in L & |.x-x0.| = dist(x,L) by Th57;
hence thesis;
end;
theorem
x in L iff dist(x,L) = 0
proof
thus x in L implies dist(x,L) = 0
proof
A1: for r being Real st r in dist_v(x,L) holds 0 <= r
proof
let r be Real;
assume r in dist_v(x,L);
then ex x0 being Element of REAL n st r= |.x-x0.| & x0 in L;
hence thesis;
end;
A2: dist_v(x,L) is bounded_below
proof
take 0;
let r be ExtReal;
assume r in dist_v(x,L);
then ex x0 being Element of REAL n st r= |.x-x0.| & x0 in L;
hence thesis;
end;
assume
A3: x in L;
|.x - x.| = |.0*n.| by Th9
.= sqrt |(0*n,0*n)| by EUCLID_4:15
.= 0 by EUCLID_4:17,SQUARE_1:17;
then
A4: 0 in dist_v(x,L) by A3;
then for s being Real st 0<s holds ex r being Real st r in
dist_v(x,L) & r < 0 + s;
hence thesis by A4,A1,A2,SEQ_4:def 2;
end;
now
consider x0 being Element of REAL n such that
A5: x0 in L and
A6: |.x-x0.| = dist(x,L) by Th57;
assume dist(x,L) = 0;
then |(x - x0, x - x0)| = 0 by A6,EUCLID_4:16;
then x - x0 = 0*n by EUCLID_4:17;
hence x in L by A5,Th9;
end;
hence thesis;
end;
definition
let n;
let L1,L2;
pred L1 // L2 means
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
L0 // L1 & L1 // L2 implies L0 // L2
proof
assume that
A1: L0 // L1 and
A2: L1 // L2;
consider x0, x1, x2, x3 being Element of REAL n such that
A3: L0 = Line(x0,x1) and
A4: L1 = Line(x2,x3) and
A5: (x1 - x0) // (x3 - x2) by A1;
A6: x3 - x2 <> 0*n by A5;
consider y0, y1, y2, y3 being Element of REAL n such that
A7: L1 = Line(y0,y1) and
A8: L2 = Line(y2,y3) and
A9: (y1 - y0) // (y3 - y2) by A2;
A10: y1 - y0 <> 0*n by A9;
x3 in Line(y1,y0) & x2 in Line(y1,y0) by A4,A7,EUCLID_4:9;
then ex a st x3 - x2 = a*(y1 - y0) by Th31;
then (x3 - x2) // (y1 - y0) by A6,A10;
then (x1 - x0) // (y1 - y0) by A5,Th33;
then (x1 - x0) // (y3 - y2) by A9,Th33;
hence thesis by A3,A8;
end;
definition
let n;
let L1,L2;
pred L1 _|_ L2 means
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 Th61:
L0 _|_ L1 & L1 // L2 implies L0 _|_ L2
proof
assume that
A1: L0 _|_ L1 and
A2: L1 // L2;
consider x0, x1, x2, x3 such that
A3: L0 = Line(x0,x1) and
A4: L1 = Line(x2,x3) and
A5: (x1 - x0) _|_ (x3 - x2) by A1;
A6: x3 - x2 <> 0*n by A5;
consider y0, y1, y2, y3 such that
A7: L1 = Line(y0,y1) and
A8: L2 = Line(y2,y3) and
A9: (y1 - y0) // (y3 - y2) by A2;
A10: y1 - y0 <> 0*n by A9;
x2 in Line(y0,y1) & x3 in Line(y0,y1) by A4,A7,EUCLID_4:9;
then ex a st x3 - x2 = a*(y1 - y0) by Th31;
then x3 - x2 // y1 - y0 by A6,A10;
then x1 - x0 _|_ y3 - y2 by A5,A9,Th33,Th44;
hence thesis by A3,A8;
end;
theorem Th62:
(not x in L) & L is being_line implies ex L0 st x in L0 & L0 _|_
L & L0 meets L
proof
assume ( not x in L)& L is being_line;
then consider x1,x2 such that
A1: L = Line(x1,x2) and
A2: (x - x1) _|_ (x2 - x1) by Th54;
reconsider L0 = Line(x1,x) as Subset of REAL n;
reconsider L0 as Element of line_of_REAL n by Th47;
x1 in L0 & x1 in L by A1,EUCLID_4:9;
then
A3: x in L0 & L0 meets L by Th49,EUCLID_4:9;
L0 _|_ L by A1,A2;
hence thesis by A3;
end;
theorem Th63:
L1 misses L2 implies ex x st x in L1 & not x in L2
proof
assume
A1: L1 misses L2;
consider x such that
A2: x in L1 by Th52;
take x;
thus thesis by A1,A2,Th49;
end;
theorem Th64:
x1 in L & x2 in L & x1 <> x2 implies Line(x1,x2) = L & L is being_line
proof
assume that
A1: x1 in L & x2 in L and
A2: x1 <> x2;
A3: Line(x1,x2) c= L by A1,Th48;
L in line_of_REAL n;
then ex y1,y2 being Element of REAL n st L = Line(y1,y2);
then L c= Line(x1,x2) by A1,A2,EUCLID_4:11;
then Line(x1,x2) = L by A3,XBOOLE_0:def 10;
hence thesis by A2;
end;
theorem Th65:
L1 is being_line & L1 = L2 implies L1 // L2
proof
assume L1 is being_line;
then consider x0,x1 such that
A1: x0 <> x1 and
A2: L1 = Line(x0,x1);
assume
A3: L1 = L2;
A4: x1 - x0 = 1 * (x1 - x0) by EUCLID_4:3;
x1 - x0 <> 0*n by A1,Th9;
then x1 - x0 // x1 - x0 by A4;
hence thesis by A3,A2;
end;
theorem Th66:
L1 // L2 implies L1 is being_line & L2 is being_line
proof
assume L1 // L2;
then consider x1,x2,y1,y2 such that
A1: L1 = Line(x1,x2) & L2 = Line(y1,y2) and
A2: x2 - x1 // y2 - y1;
y2 - y1 <> 0*n by A2;
then
A3: y2 <> y1 by Th9;
x2 - x1 <> 0*n by A2;
then x2 <> x1 by Th9;
hence thesis by A1,A3;
end;
theorem Th67:
L1 _|_ L2 implies L1 is being_line & L2 is being_line
proof
assume L1 _|_ L2;
then consider x1,x2,y1,y2 such that
A1: L1 = Line(x1,x2) & L2 = Line(y1,y2) and
A2: x2 - x1 _|_ y2 - y1;
y2 - y1 <> 0*n by A2;
then
A3: y2 <> y1 by Th9;
x2 - x1 <> 0*n by A2;
then x2 <> x1 by Th9;
hence thesis by A1,A3;
end;
theorem
x in L & a<>1 & a*x in L implies 0*n in L
proof
assume that
A1: x in L and
A2: a<>1 and
A3: a*x in L;
A4: 1-a<>0 by A2;
A5: 1-1/(1-a)+(1/(1-a))*a = 1-1/(1-a)+a/(1-a) by XCMPLX_1:99
.= 1 + (-1/(1-a) + a/(1-a))
.= 1 + ((-1)/(1-a) + a/(1-a)) by XCMPLX_1:187
.= 1 + (-1+a)/(1-a) by XCMPLX_1:62
.= 1 + (-(-a + 1))/(1-a)
.= 1 + - (1-a)/(1-a) by XCMPLX_1:187
.= 1 - (1-a)/(1-a)
.= 1 - 1 by A4,XCMPLX_1:60
.= 0;
0*n = 0 * x by EUCLID_4:3
.= (1-1/(1-a))*x +((1/(1-a))*a)*x by A5,EUCLID_4:7
.= (1-1/(1-a))*x +(1/(1-a))*(a*x) by EUCLID_4:4;
then
A6: 0*n in Line(x,a*x);
Line(x,a*x) c= L by A1,A3,Th48;
hence thesis by A6;
end;
theorem
x1 in L & x2 in L implies ex x3 st x3 in L & x3 - x1 = a*(x2 - x1)
proof
set x3 = (1-a)*x1 + a*x2;
assume x1 in L & x2 in L;
then
A1: Line(x1,x2) c= L by Th48;
x3 = 1 * x1 + -a*x1 + a*x2 by Th11
.= x1 + -a*x1 + a*x2 by EUCLID_4:3
.= x1 + (a*x2 + -a*x1) by RVSUM_1:15
.= x1 + a*(x2 - x1) by Th12;
then x3 in Line(x1,x2) & x3 - x1 = a*(x2 - x1) by Th6;
hence thesis by A1;
end;
theorem Th70:
x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a st x3 - x1 = a*(x2 - x1)
proof
assume x1 in L & x2 in L & x3 in L & x1 <> x2;
then x1 in Line(x1,x2) & x3 in Line(x1,x2) by Th64;
then consider a such that
A1: x3 - x1 = a*(x2 - x1) by Th31;
take a;
thus thesis by A1;
end;
theorem Th71:
L1 // L2 & L1<>L2 implies L1 misses L2
proof
assume that
A1: L1 // L2 and
A2: L1<>L2;
assume not L1 misses L2;
then consider x be object such that
A3: x in L1 and
A4: x in L2 by XBOOLE_0:3;
reconsider x as Element of REAL n by A3;
consider x1, x2, y1, y2 being Element of REAL n such that
A5: L1 = Line(x1,x2) and
A6: L2 = Line(y1,y2) and
A7: (x2 - x1) // (y2 - y1) by A1;
A8: x2 - x1 <> 0*n by A7;
then x1 <> x2 by Th9;
then
A9: L1 is being_line by A5;
then consider x0 such that
A10: x <> x0 and
A11: x0 in L1 by EUCLID_4:14;
A12: x0 - x <> 0*n by A10,Th9;
ex a st x0 - x = a*(x2 - x1) by A5,A3,A11,Th31;
then x0 - x // x2 - x1 by A8,A12;
then
A13: x0 - x // y2 - y1 by A7,Th33;
A14: y2 - y1 <> 0*n by A7;
then y1 <> y2 by Th9;
then
A15: L2 is being_line by A6;
then consider y0 such that
A16: x <> y0 and
A17: y0 in L2 by EUCLID_4:14;
A18: y0 - x <> 0*n by A16,Th9;
ex b st y0 - x = b*(y2 - y1) by A6,A4,A17,Th31;
then y0 - x // y2 - y1 by A14,A18;
then
A19: x0 - x // y0 - x by A13,Th33;
A20: Line(x,x0) c= Line(x,y0)
proof
let y be object;
assume y in Line(x,x0);
then consider t such that
A21: y = (1-t)*x + t*x0;
consider a such that
A22: x0 - x = a*(y0 - x) by A19;
y = 1 * x + -t*x + t*x0 by A21,Th11
.= x + -t*x + t*x0 by EUCLID_4:3
.= x + (t*x0 + -t*x) by RVSUM_1:15
.= x + t*(x0 - x) by Th12;
then y = x + (t*a)*(y0 - x) by A22,EUCLID_4:4
.= x + ((t*a)*y0 + -(t*a)*x) by Th12
.= x + -(t*a)*x + (t*a)*y0 by RVSUM_1:15
.= 1 * x + -(t*a)*x + (t*a)*y0 by EUCLID_4:3
.= (1 -(t*a))*x + (t*a)*y0 by Th11;
hence thesis;
end;
A23: Line(x,y0) c= Line(x,x0)
proof
let y be object;
assume y in Line(x,y0);
then consider t such that
A24: y = (1-t)*x + t*y0;
consider a such that
A25: y0 - x = a*(x0 - x) by A19,Def1;
y = 1 * x + -t*x + t*y0 by A24,Th11
.= x + -t*x + t*y0 by EUCLID_4:3
.= x + (t*y0 + -t*x) by RVSUM_1:15
.= x + t*(y0 - x) by Th12;
then y = x + (t*a)*(x0 - x) by A25,EUCLID_4:4
.= x + ((t*a)*x0 + -(t*a)*x) by Th12
.= x + -(t*a)*x + (t*a)*x0 by RVSUM_1:15
.= 1 * x + -(t*a)*x + (t*a)*x0 by EUCLID_4:3
.= (1 -(t*a))*x + (t*a)*x0 by Th11;
hence thesis;
end;
A26: L2 = Line(x,y0) by A4,A15,A16,A17,Th30;
L1 = Line(x,x0) by A3,A9,A10,A11,Th30;
hence contradiction by A2,A26,A20,A23,XBOOLE_0:def 10;
end;
theorem Th72:
L is being_line implies ex L0 st x in L0 & L0 // L
proof
assume L is being_line;
then consider y0,y1 such that
A1: y0 <> y1 and
A2: L = Line(y0,y1);
set x9 = x + (y1 - y0);
reconsider L0 = Line(x,x9) as Element of line_of_REAL n by Th47;
take L0;
A3: y1 - y0 <> 0*n by A1,Th9;
A4: x9 - x = y1 - y0 by Th6;
then x9 - x = 1 * (y1 - y0) by EUCLID_4:3;
then (x9 - x) // (y1 - y0) by A4,A3;
hence thesis by A2,EUCLID_4:9;
end;
theorem
for x,L st (not x in L) & L is being_line holds ex L0 st x in L0 & L0
// L & L0 <> L
proof
let x,L;
assume that
A1: not x in L and
A2: L is being_line;
ex L0 st x in L0 & L0 // L by A2,Th72;
hence thesis by A1;
end;
theorem Th74:
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
proof
let x0,x1,y0,y1,L1,L2;
assume that
A1: x0 in L1 & x1 in L1 and
A2: x0 <> x1 and
A3: y0 in L2 & y1 in L2 and
A4: y0 <> y1 and
A5: L1 _|_ L2;
consider x2,x3,y2,y3 such that
A6: L1 = Line(x2,x3) and
A7: L2 = Line(y2,y3) and
A8: x3 - x2 _|_ y3 - y2 by A5;
consider s such that
A9: x1 - x0 = s*(x3 - x2) by A1,A6,Th31;
x3 - x2,y3 - y2 are_orthogonal by A8;
then
A10: |(x3 - x2,y3 - y2)| = 0 by RVSUM_1:def 17;
consider t such that
A11: y1 - y0 = t*(y3 - y2) by A3,A7,Th31;
|(x1 - x0,y1 - y0)| = s * |(x3 - x2,y1 - y0)| by A9,EUCLID_4:21
.= s * (t * |(x3 - x2,y3 - y2)|) by A11,EUCLID_4:22
.= 0 by A10;
then
A12: x1 - x0,y1 - y0 are_orthogonal by RVSUM_1:def 17;
x1 - x0 <> 0*n & y1 - y0 <> 0*n by A2,A4,Th9;
hence thesis by A12;
end;
theorem Th75:
for L1,L2 st L1 _|_ L2 holds L1 <> L2
proof
let L1,L2;
assume
A1: L1 _|_ L2;
now
per cases;
case
A2: L1 misses L2;
ex x st x in L1 by Th52;
hence thesis by A2,Th49;
end;
case
L1 meets L2;
then consider x0 such that
A3: x0 in L1 and
A4: x0 in L2 by Th49;
L1 is being_line by A1,Th67;
then consider x1 such that
A5: x1 <> x0 and
A6: x1 in L1 by Th53;
A7: x1 - x0 <> 0*n by A5,Th9;
L2 is being_line by A1,Th67;
then consider x2 such that
A8: x2 <> x0 and
A9: x2 in L2 by Th53;
A10: x2 - x0 <> 0*n by A8,Th9;
A11: x1 - x0 _|_ x2 - x0 by A1,A3,A4,A5,A6,A8,A9,Th74;
not x1 in L2
proof
assume x1 in L2;
then ex a st x1 - x0 = a * (x2 - x0) by A4,A8,A9,Th70;
then x1 - x0 // x2 - x0 by A7,A10;
hence contradiction by A11,Lm3,Th45;
end;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem Th76:
for x1,x2,L st L is being_line & L = Line(x1,x2) holds x1 <> x2
proof
let x1,x2,L;
assume that
A1: L is being_line and
A2: L = Line(x1,x2);
consider y1, y2 such that
A3: y1 <> y2 and
A4: L = Line(y1,y2) by A1;
y1 in L & y2 in L by A4,EUCLID_4:9;
then consider a such that
A5: y2 - y1 = a*(x2 - x1) by A2,Th31;
thus x1 <> x2
proof
assume x1 = x2;
then y2 - y1 = a* 0*n by A5,Th2
.= 0*n by EUCLID_4:2;
hence contradiction by A3,Th9;
end;
end;
theorem Th77:
x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1
& L1 // L2 implies x1 - x0 // y1 - y0
proof
assume that
A1: x0 in L1 & x1 in L1 and
A2: x0 <> x1 and
A3: y0 in L2 & y1 in L2 and
A4: y0 <> y1 and
A5: L1 // L2;
consider x2,x3,y2,y3 such that
A6: L1 = Line(x2,x3) and
A7: L2 = Line(y2,y3) and
A8: x3 - x2 // y3 - y2 by A5;
consider t such that
A9: y1 - y0 = t*(y3 - y2) by A3,A7,Th31;
A10: x1 - x0 <> 0*n by A2,Th9;
A11: y1 - y0 <> 0*n by A4,Th9;
then
A12: t <> 0 by A9,EUCLID_4:3;
consider s such that
A13: x1 - x0 = s*(x3 - x2) by A1,A6,Th31;
consider a such that
A14: x3 - x2 = a*(y3 - y2) by A8;
x1 - x0 = (s*a)*(y3 - y2) by A13,A14,EUCLID_4:4
.= (s*a)*(1 * (y3 - y2)) by EUCLID_4:3
.= (s*a)*((1/t*t)*(y3 - y2)) by A12,XCMPLX_1:106
.= (s*a)*(1/t*(t*(y3 - y2))) by EUCLID_4:4
.= ((s*a)*(1/t))*(t*(y3 - y2)) by EUCLID_4:4
.= ((s*a)/t)*(y1 - y0) by A9,XCMPLX_1:99;
hence thesis by A10,A11;
end;
theorem
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))
proof
assume that
A1: x2 - x1,x3 - x1 are_lindependent2 and
A2: y2 in Line(x1,x2) and
A3: y3 in Line(x1,x3) and
A4: L1 = Line(x2,x3) and
A5: L2 = Line(y2,y3);
thus L1 // L2 implies ex a st a <> 0 & y2 - x1 = a*(x2 - x1) & y3 - x1 = a*(
x3 - x1)
proof
assume
A6: L1 // L2;
then L1 is being_line by Th66;
then
A7: x2 <> x3 by A4,Th76;
L2 is being_line by A6,Th66;
then
A8: y2 <> y3 by A5,Th76;
A9: y2 in L2 & y3 in L2 by A5,EUCLID_4:9;
consider t such that
A10: y3 = (1 - t)*x1 + t*x3 by A3;
x2 in L1 & x3 in L1 by A4,EUCLID_4:9;
then
A11: y3 - y2 // x3 - x2 by A6,A7,A8,A9,Th77;
then consider a such that
A12: y3 - y2 = a*(x3 - x2);
take a;
consider s such that
A13: y2 = (1 - s)*x1 + s*x2 by A2;
A14: 0*n = y3 - y2 - a*(x3 - x2) by A12,Th9
.= (1 - t)*x1 + t*x3 - (1 - s)*x1 - s*x2 - a*(x3 - x2) by A13,A10,
RVSUM_1:39
.= 1 * x1 + -t*x1 + t*x3 - (1 - s)*x1 - s*x2 - a*(x3 - x2) by Th11
.= 1 * x1 + -t*x1 + t*x3 - (1 * x1 + -s*x1)- s*x2- a*(x3 - x2) by Th11
.= 1 * x1 + -t*x1 + t*x3 - 1 * x1 - -s*x1 - s*x2- a*(x3 - x2) by
RVSUM_1:39
.= 1 * x1 + -t*x1 + -1 * x1 + t*x3 + s*x1 - s*x2- a*(x3 - x2) by
RVSUM_1:15
.= 1 * x1 + -1 * x1 + -t*x1 + t*x3 + s*x1 - s*x2- a*(x3 - x2) by
RVSUM_1:15
.= 0*n + -t*x1 + t*x3 + s*x1 - s*x2- a*(x3 - x2) by Th2
.= -t*x1 + t*x3 + s*x1 - s*x2- a*(x3 - x2) by EUCLID_4:1
.= t*(x3 - x1) + s*x1 + -s*x2 - a*(x3 - x2) by Th12
.= t*(x3 - x1) - s*x2 + s*x1 - a*(x3 - x2) by RVSUM_1:15
.= t*(x3 - x1) - (s*x2 - s*x1) - a*(x3 - x2) by Th4
.= t*(x3 - x1) - s*(x2 - x1) - a*(x3 - x2) by Th12
.= t*(x3 - x1) - s*(x2 - x1) - a*(x3 - 0*n - x2) by RVSUM_1:32
.= t*(x3 - x1) - s*(x2 - x1) - a*(x3 - (x1 - x1) - x2) by Th2
.= t*(x3 - x1) - s*(x2 - x1) - a*(x3 - x1 + x1 + -x2) by Th4
.= t*(x3 - x1) - s*(x2 - x1) - a*((x3 - x1) + (-x2 + x1)) by RVSUM_1:15
.= t*(x3 - x1) - s*(x2 - x1) - (a*(x3 - x1) + a*(-x2 + x1)) by EUCLID_4:6
.= t*(x3 - x1) - s*(x2 - x1) - a*(x3 - x1) - a*(-x2 + x1) by RVSUM_1:39
.= t*(x3 - x1) - (a*(x3 - x1) + s*(x2 - x1)) - a*(-x2 + x1) by RVSUM_1:39
.= t*(x3 - x1) - a*(x3 - x1) - s*(x2 - x1) - a*(-x2 + x1) by RVSUM_1:39
.= (t - a)*(x3 - x1) - s*(x2 - x1) - a*(-x2 + x1) by Th11
.= (t - a)*(x3 - x1) - s*(x2 - x1) - (a*(-x2) + a*x1) by EUCLID_4:6
.= (t - a)*(x3 - x1) - s*(x2 - x1) - (-a*x2 + a*x1) by Th3
.= (t - a)*(x3 - x1) - s*(x2 - x1) - -a*x2 - a*x1 by RVSUM_1:39
.= (t - a)*(x3 - x1) - s*(x2 - x1) + (a*x2 + - a*x1) by RVSUM_1:15
.= (t - a)*(x3 - x1) - s*(x2 - x1) + a*(x2 - x1) by Th12
.= (t - a)*(x3 - x1) - (s*(x2 - x1) - a*(x2 - x1)) by Th4
.= (t - a)*(x3 - x1) + -(s - a)*(x2 - x1) by Th11
.= (t - a)*(x3 - x1) + (-(s - a))*(x2 - x1) by Th3
.= (t - a)*(x3 - x1) + (a - s)*(x2 - x1);
then t - a = 0 by A1;
then
A15: y3 - x1 = 1 * x1 + -a*x1 + a*x3 - x1 by A10,Th11
.= x1 + -a*x1 + a*x3 - x1 by EUCLID_4:3
.= -a*x1 + a*x3 + x1 - x1 by RVSUM_1:15
.= -a*x1 + a*x3 + (x1 - x1) by Th5
.= -a*x1 + a*x3 + 0*n by Th2
.= -a*x1 + a*x3 by EUCLID_4:1
.= a*(x3 - x1) by Th12;
a - s = 0 by A1,A14;
then
A16: y2 - x1 = 1 * x1 + -a*x1 + a*x2 - x1 by A13,Th11
.= x1 + -a*x1 + a*x2 - x1 by EUCLID_4:3
.= -a*x1 + a*x2 + x1 - x1 by RVSUM_1:15
.= -a*x1 + a*x2 + (x1 - x1) by Th5
.= -a*x1 + a*x2 + 0*n by Th2
.= -a*x1 + a*x2 by EUCLID_4:1
.= a*(x2 - x1) by Th12;
y3 - y2 <> 0*n by A11;
hence thesis by A12,A16,A15,EUCLID_4:3;
end;
now
assume ex a st a <> 0 & y2 - x1 = a*(x2 - x1) & y3 - x1 = a*(x3 - x1);
then consider a such that
A17: a <> 0 and
A18: y2 - x1 = a*(x2 - x1) and
A19: y3 - x1 = a*(x3 - x1);
take a;
take x2;
take x3;
take y2;
take y3;
x2 <> x3 by A1,Th37;
then
A20: x3 - x2 <> 0*n by Th9;
A21: y3 - y2 = x1 + a*(x3 - x1) - y2 by A19,Th6
.= a*(x3 - x1) + x1 - (x1 + a*(x2 - x1)) by A18,Th6
.= a*(x3 - x1) + x1 - x1 - a*(x2 - x1) by RVSUM_1:39
.= a*(x3 - x1) + (x1 - x1) - a*(x2 - x1) by Th5
.= a*(x3 - x1) + 0*n - a*(x2 - x1) by Th2
.= a*(x3 - x1) - a*(x2 - x1) by EUCLID_4:1
.= a*x3 + -a*x1 - a*(x2 - x1) by Th12
.= a*x3 + -a*x1 - (-a*x1 + a*x2) by Th12
.= a*x3 + -a*x1 - -a*x1 - a*x2 by RVSUM_1:39
.= a*x3 + (-a*x1 - -a*x1) - a*x2 by Th5
.= a*x3 + 0*n - a*x2 by Th2
.= a*x3 - a*x2 by EUCLID_4:1
.= a*(x3 - x2) by Th12;
then y3 - y2 <> 0*n by A17,A20,EUCLID_4:5;
then y3 - y2 // x3 - x2 by A21,A20;
hence L1 // L2 by A4,A5;
end;
hence thesis;
end;
theorem Th79:
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
proof
let L1,L2;
assume that
A1: L1 is being_line and
A2: L2 is being_line;
consider x1,x2 such that
A3: x1 <> x2 and
A4: L1 = Line(x1,x2) by A1;
assume
A5: L1 <> L2;
now
per cases by A2,A3,A4,A5,Th30;
case
A6: not x1 in L2;
set x = x1;
thus x in L1 & not x in L2 by A4,A6,EUCLID_4:9;
end;
case
A7: not x2 in L2;
set x = x2;
thus x in L1 & not x in L2 by A4,A7,EUCLID_4:9;
end;
end;
hence thesis;
end;
theorem Th80:
for x,L1,L2 st L1 _|_ L2 holds ex L0 st x in L0 & L0 _|_ L2 & L0 // L1
proof
let x,L1,L2;
assume
A1: L1 _|_ L2;
then L1 is being_line by Th67;
then consider L0 such that
A2: x in L0 & L0 // L1 by Th72;
take L0;
thus thesis by A1,A2,Th61;
end;
theorem Th81:
for x,L1,L2 st x in L2 & L1 _|_ L2 holds ex x0 st x <> x0 & x0
in L1 & not x0 in L2
proof
let x,L1,L2;
assume that
A1: x in L2 and
A2: L1 _|_ L2;
L1 is being_line & L2 is being_line by A2,Th67;
then ex x0 st x0 in L1 & not x0 in L2 by A2,Th75,Th79;
hence thesis by A1;
end;
:: Planes
definition
let n be Nat,x1,x2,x3 be Element of REAL n;
func plane(x1,x2,x3) -> Subset of REAL n equals
{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};
correctness
proof
set A = {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};
A c= REAL n
proof
let x be object;
assume x in A;
then
ex x9 be Element of REAL n st x = x9 &
ex a1,a2,a3 being Real st a1+
a2+a3=1 & x9=a1*x1+a2*x2+a3*x3;
hence thesis;
end;
hence thesis;
end;
end;
registration
let n be Nat,x1,x2,x3 be Element of REAL n;
cluster plane(x1,x2,x3) -> non empty;
coherence
proof
A1: 0 * x3 = 0*n by EUCLID_4:3;
A2: 1+0+0=1;
1 * x1 = x1 & 0 * x2 = 0*n by EUCLID_4:3;
then 1 * x1 + 0 * x2 + 0 * x3 = x1 + 0*n by A1,EUCLID_4:1
.= x1 by EUCLID_4:1;
then x1 in plane(x1,x2,x3) by A2;
hence thesis;
end;
end;
definition
let n;
let A be Subset of REAL n;
attr A is being_plane means
ex x1,x2,x3 st x2 - x1, x3 - x1 are_lindependent2 & A = plane(x1,x2,x3);
end;
theorem Th82:
x1 in plane(x1,x2,x3) & x2 in plane(x1,x2,x3) & x3 in plane(x1, x2,x3)
proof
A1: 0 * x3 = 0*n by EUCLID_4:3;
1 * x1 = x1 & 0 * x2 = 0*n by EUCLID_4:3;
then
A2: 1 * x1 + 0 * x2 + 0 * x3 = x1 + 0*n by A1,EUCLID_4:1
.= x1 by EUCLID_4:1;
A3: 0 * x3 = 0*n by EUCLID_4:3;
A4: 1 * x3 = x3 by EUCLID_4:3;
0 * x1 = 0*n & 0 * x2 = 0*n by EUCLID_4:3;
then
A5: 0 * x1 + 0 * x2 + 1 * x3 = 0*n + x3 by A4,EUCLID_4:1
.= x3 by EUCLID_4:1;
0 * x1 = 0*n & 1 * x2 = x2 by EUCLID_4:3;
then
A6: 0 * x1 + 1 * x2 + 0 * x3 = x2 + 0*n by A3,EUCLID_4:1
.= x2 by EUCLID_4:1;
0+0+1=1;
hence thesis by A2,A6,A5;
end;
theorem Th83:
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)
proof
assume that
A1: x1 in plane(y1,y2,y3) and
A2: x2 in plane(y1,y2,y3) and
A3: x3 in plane(y1,y2,y3);
ex x29 be Element of REAL n st x2 = x29 &
ex a21,a22,a23 being Real st
a21 + a22 + a23 = 1 & x29 = a21 * y1 + a22 * y2 + a23 * y3 by A2;
then consider a21,a22,a23 being Real such that
A4: a21 + a22 + a23 = 1 and
A5: x2 = a21*y1 + a22*y2 + a23*y3;
ex x19 be Element of REAL n st x1 = x19 &
ex a11,a12,a13 being Real st
a11 + a12 + a13 = 1 & x19 = a11 * y1 + a12 * y2 + a13 * y3 by A1;
then consider a11,a12,a13 being Real such that
A6: a11 + a12 + a13 = 1 and
A7: x1 = a11*y1 + a12*y2 + a13*y3;
let x be object;
assume x in plane(x1,x2,x3);
then
ex x9 be Element of REAL n st x = x9 &
ex b1,b2,b3 being Real st b1 + b2
+ b3 = 1 & x9 = b1 * x1 + b2 * x2 + b3 * x3;
then consider b1,b2,b3 being Real such that
A8: b1 + b2 + b3 = 1 and
A9: x = b1*x1 + b2*x2 + b3*x3;
ex x39 be Element of REAL n st x3 = x39 &
ex a31,a32,a33 being Real st
a31 + a32 + a33 = 1 & x39 = a31 * y1 + a32 * y2 + a33 * y3 by A3;
then consider a31,a32,a33 being Real such that
A10: a31 + a32 + a33 = 1 and
A11: x3 = a31*y1 + a32*y2 + a33*y3;
A12: (b1*a11 + b2*a21 + b3*a31) + (b1*a12 + b2*a22 + b3*a32) + (b1*a13 + b2*
a23 + b3*a33) = b1*(a11 + a12 + a13) + b2*(a21 + a22 + a23)+ b3*(a31 + a32 +
a33)
.= 1 by A6,A4,A10,A8;
x = ((b1*a11) * y1 + (b1*a12) * y2 + (b1*a13) * y3) + b2*(a21 * y1 +
a22 * y2 + a23 * y3) + b3*(a31 * y1 + a32 * y2 + a33 * y3) by A7,A5,A11,A9
,Th22
.= ((b1*a11) * y1 + (b1*a12) * y2 + (b1*a13) * y3) + ((b2*a21) * y1 + (
b2*a22) * y2 + (b2*a23) * y3) + b3*(a31 * y1 + a32 * y2 + a33 * y3) by Th22
.= ((b1*a11) * y1 + (b1*a12) * y2 + (b1*a13) * y3) + ((b2*a21) * y1 + (
b2*a22) * y2 + (b2*a23) * y3) + ((b3*a31) * y1 + (b3*a32) * y2 + (b3*a33) * y3)
by Th22
.= ((b1*a11+b2*a21) * y1 + (b1*a12+b2*a22) * y2 + (b1*a13+b2*a23) * y3)
+ ((b3*a31) * y1 + (b3*a32) * y2 + (b3*a33) * y3) by Th24
.= (b1*a11 + b2*a21 + b3*a31)*y1 + (b1*a12 + b2*a22 + b3*a32)*y2 + (b1*
a13 + b2*a23 + b3*a33)*y3 by Th24;
hence thesis by A12;
end;
theorem
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)
proof
let A being Subset of REAL n,x,x1,x2,x3;
assume that
A1: x in plane(x1,x2,x3) and
A2: ex c1,c2,c3 being Real st c1 + c2 + c3 = 0 & x = c1*x1 + c2*x2 + c3* x3;
consider c1,c2,c3 being Real such that
A3: c1 + c2 + c3 = 0 and
A4: x = c1*x1 + c2*x2 + c3*x3 by A2;
ex x9 be Element of REAL n st x = x9 &
ex a1,a2,a3 being Real st a1 + a2
+ a3 = 1 & x9 = a1 * x1 + a2 * x2 + a3 * x3 by A1;
then consider a1,a2,a3 being Real such that
A5: a1 + a2 + a3 = 1 and
A6: x = a1 * x1 + a2 * x2 + a3 * x3;
A7: (a1+ -c1) + (a2 + -c2) + (a3 + -c3) = 1 by A5,A3;
0*n = x - x by Th2
.= (a1*x1 + a2*x2 + a3*x3) + ((-c1)*x1 + (-c2)*x2 + (-c3)*x3) by A6,A4,Th14
.= (a1 +-c1)*x1 + (a2+-c2)*x2 + (a3+-c3)*x3 by Th24;
hence thesis by A7;
end;
theorem Th85:
y1 in plane(x1,x2,x3) & y2 in plane(x1,x2,x3) implies Line(y1,y2
) c= plane(x1,x2,x3)
proof
assume that
A1: y1 in plane(x1,x2,x3) and
A2: y2 in plane(x1,x2,x3);
consider y29 be Element of REAL n such that
A3: y2 = y29 and
A4: ex a21,a22,a23 being Real st a21 + a22 + a23 = 1 & y29 = a21 * x1 +
a22 * x2 + a23 * x3 by A2;
consider y19 be Element of REAL n such that
A5: y1 = y19 and
A6: ex a11,a12,a13 being Real st a11 + a12 + a13 = 1 & y19 = a11 * x1 +
a12 * x2 + a13 * x3 by A1;
Line(y1,y2) c= plane(x1,x2,x3)
proof
let x be object;
assume x in Line(y1,y2);
then consider t such that
A7: x = (1-t)*y1 + t*y2;
consider a21,a22,a23 being Real such that
A8: a21 + a22 + a23 = 1 and
A9: y29 = a21 * x1 + a22 * x2 + a23 * x3 by A4;
consider a11,a12,a13 being Real such that
A10: a11 + a12 + a13 = 1 and
A11: y19 = a11 * x1 + a12 * x2 + a13 * x3 by A6;
A12: ((1-t)*a11+t*a21) + ((1-t)*a12+t*a22) + ((1-t)*a13+t*a23) = (1-t)*(
a11 + a12 + a13) + t*(a21 + a22 + a23)
.= (1-t) + t by A10,A8
.= 1;
x = (((1-t)*a11)*x1 + ((1-t)*a12)*x2 + ((1-t)*a13)*x3) + t*(a21 * x1
+ a22 * x2 + a23 * x3) by A5,A3,A7,A11,A9,Th22
.= (((1-t)*a11)*x1 + ((1-t)*a12)*x2 + ((1-t)*a13)*x3) + ((t*a21)*x1 +
(t*a22)*x2 + (t*a23)*x3) by Th22
.= ((1-t)*a11 + t*a21) * x1 + ((1-t)*a12 + t*a22) * x2 + ((1-t)*a13+t*
a23) * x3 by Th24;
hence thesis by A12;
end;
hence thesis;
end;
theorem
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
proof
let A be Subset of REAL n,x;
assume that
A1: A is being_plane and
A2: x in A and
A3: ex a st a<>1 & a*x in A;
consider a such that
A4: a<>1 and
A5: a*x in A by A3;
A6: 1-a<>0 by A4;
A7: 1-1/(1-a)+(1/(1-a))*a = 1-1/(1-a)+a/(1-a) by XCMPLX_1:99
.= 1 + (-1/(1-a) + a/(1-a))
.= 1 + ((-1)/(1-a) + a/(1-a)) by XCMPLX_1:187
.= 1 + (-1+a)/(1-a) by XCMPLX_1:62
.= 1 + (-(-a --1))/(1-a)
.= 1 + - (1-a)/(1-a) by XCMPLX_1:187
.= 1 - (1-a)/(1-a)
.= 1 - 1 by A6,XCMPLX_1:60
.= 0;
0*n = 0 * x by EUCLID_4:3
.= (1-1/(1-a))*x +((1/(1-a))*a)*x by A7,EUCLID_4:7
.= (1-1/(1-a))*x +(1/(1-a))*(a*x) by EUCLID_4:4;
then
A8: 0*n in Line(x,a*x);
ex x1,x2,x3 st x2-x1,x3-x1 are_lindependent2 & A = plane (x1,x2,x3) by A1;
then Line(x,a*x) c= A by A2,A5,Th85;
hence thesis by A8;
end;
theorem
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)
proof
assume that
A1: x in plane(x1,x2,x3) and
A2: x = a1*x1+a2*x2+a3*x3 and
A3: not a1+a2+a3 = 1;
ex x9 be Element of REAL n st x = x9 &
ex a19,a29,a39 being Real st a19+
a29+a39=1 & x9 = a19*x1+a29*x2+a39* x3 by A1;
then consider a19,a29,a39 being Real such that
A4: a19+a29+a39=1 and
A5: x = a19*x1+a29*x2+a39*x3;
A6: (a1-a19)+(a2-a29)+(a3-a39) <> 0 by A3,A4;
set t = (a1-a19)+(a2-a29)+(a3-a39);
A7: (a1-a19)/t+(a2-a29)/t+(a3-a39)/t = ((a1-a19)+(a2-a29)+(a3-a39))/t by
XCMPLX_1:63
.= 1 by A6,XCMPLX_1:60;
A8: 0*n = (a1*x1+a2*x2+a3*x3) - (a19*x1+a29*x2+a39*x3) by A2,A5,Th2
.= (a1-a19)*x1+(a2-a29)*x2+(a3-a39)*x3 by Th26;
0*n = (1/t) * 0*n by EUCLID_4:2
.= (1/t*(a1-a19))*x1+(1/t*(a2-a29))*x2+(1/t*(a3-a39))*x3 by A8,Th22
.= (a1-a19)/t*x1+(1/t*(a2-a29))*x2+(1/t*(a3-a39))*x3 by XCMPLX_1:99
.= (a1-a19)/t*x1+(a2-a29)/t*x2+(1/t*(a3-a39))*x3 by XCMPLX_1:99
.= (a1-a19)/t*x1+(a2-a29)/t*x2+(a3-a39)/t*x3 by XCMPLX_1:99;
hence thesis by A7;
end;
theorem Th88:
x in plane(x1,x2,x3) iff ex a1,a2,a3 st a1+a2+a3=1 & x = a1*x1+ a2*x2+a3*x3
proof
thus x in plane(x1,x2,x3)
implies ex a1,a2,a3 st a1+a2+a3=1 & x = a1*x1+a2*x2+a3*x3
proof
assume x in plane(x1,x2,x3);
then
ex x9 be Element of REAL n st x = x9 &
ex a19,a29,a39 being Real st a19
+a29+a39=1 & x9=a19*x1+a29*x2+a39*x3;
hence thesis;
end;
thus thesis;
end;
theorem
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
proof
assume
A1: x2-x1,x3-x1 are_lindependent2;
assume that
A2: a1 + a2 + a3 = 1 and
A3: x = a1*x1+a2*x2+a3*x3 and
A4: b1 + b2 + b3 = 1 and
A5: x = b1*x1+b2*x2+b3*x3;
a1 = 1 - a2 -a3 by A2;
then x = 1 * x1 - a2*x1 - a3*x1 + a2*x2 + a3*x3 by A3,Th13
.= x1 + -a2*x1 - a3*x1 + a2*x2 + a3*x3 by EUCLID_4:3
.= x1 + -a2*x1 + a2*x2 + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + -a3*x1 + a3*x3 by RVSUM_1:15
.= x1 + (a2*x2 + -a2*x1) + (a3*x3 + -a3*x1) by RVSUM_1:15
.= x1 + (a2*x2 + a2*(-x1)) + (a3*x3 + -a3*x1) by Th3
.= x1 + (a2*x2 + a2*(-x1)) + (a3*x3 + a3*(-x1)) by Th3
.= x1 + a2*(x2 + -x1) + (a3*x3 + a3*(-x1)) by EUCLID_4:6
.= x1 + a2*(x2 - x1) + a3*(x3 - x1) by EUCLID_4:6;
then
A6: x - x1 = a2*(x2 - x1) + a3*(x3 - x1) by Th7;
x = (1 - b2 -b3)*x1 + b2*x2 + b3*x3 by A4,A5
.= 1 * x1 - b2*x1 - b3*x1 + b2*x2 + b3*x3 by Th13
.= x1 + -b2*x1 - b3*x1 + b2*x2 + b3*x3 by EUCLID_4:3
.= x1 + -b2*x1 + b2*x2 + -b3*x1 + b3*x3 by RVSUM_1:15
.= x1 + (b2*x2 + -b2*x1) + -b3*x1 + b3*x3 by RVSUM_1:15
.= x1 + (b2*x2 + -b2*x1) + (b3*x3 + -b3*x1) by RVSUM_1:15
.= x1 + (b2*x2 + b2*(-x1)) + (b3*x3 + -b3*x1) by Th3
.= x1 + (b2*x2 + b2*(-x1)) + (b3*x3 + b3*(-x1)) by Th3
.= x1 + b2*(x2 + -x1) + (b3*x3 + b3*(-x1)) by EUCLID_4:6
.= x1 + b2*(x2 - x1) + b3*(x3 - x1) by EUCLID_4:6;
then a2*(x2 - x1) + a3*(x3 - x1) = b2*(x2 - x1) + b3*(x3 - x1) by A6,Th7;
then a2 = b2 & a3 = b3 by A1,Th35;
hence thesis by A2,A4;
end;
definition
let n;
func plane_of_REAL n -> Subset-Family of REAL n equals
{P where P is Subset
of REAL n: ex x1,x2,x3 being Element of REAL n st P = plane(x1,x2,x3)};
correctness
proof
set A = {P where P is Subset of REAL n: ex x1,x2,x3 being Element of REAL
n st P = plane(x1,x2,x3)};
A c= bool REAL n
proof
let P be object;
assume P in A;
then ex P9 be Subset of REAL n st P = P9 & ex x1,x2,x3 being Element of
REAL n st P9 = plane(x1,x2,x3);
hence thesis;
end;
hence thesis;
end;
end;
registration
let n;
cluster plane_of_REAL n -> non empty;
coherence
proof
reconsider P = plane(0*n,1*n,1*n) as Subset of REAL n;
P in plane_of_REAL n;
hence thesis;
end;
end;
theorem Th90:
plane(x1,x2,x3) in plane_of_REAL n;
reserve P,P0,P1,P2 for Element of plane_of_REAL n;
theorem Th91:
x1 in P & x2 in P & x3 in P implies plane(x1,x2,x3) c= P
proof
P in plane_of_REAL n;
then
A1: ex P9 being Subset of REAL n st P = P9 & ex y1,y2,y3 being Element of
REAL n st P9 = plane(y1,y2,y3);
assume x1 in P & x2 in P & x3 in P;
hence thesis by A1,Th83;
end;
theorem Th92:
x1 in P & x2 in P & x3 in P & x2 - x1, x3 - x1 are_lindependent2
implies P = plane(x1,x2,x3)
proof
assume that
A1: x1 in P and
A2: x2 in P and
A3: x3 in P and
A4: x2 - x1, x3 - x1 are_lindependent2;
P in plane_of_REAL n;
then
ex P9 being Subset of REAL n st P= P9 & ex y1,y2,y3 being Element of REAL
n st P9 = plane(y1,y2,y3);
then consider y1,y2,y3 being Element of REAL n such that
A5: P = plane(y1,y2,y3);
ex x9 be Element of REAL n st x2 = x9 &
ex a19,a29,a39 being Real st a19
+a29+a39=1 & x9 = a19*y1+a29*y2+a39* y3 by A2,A5;
then consider a21,a22,a23 being Real such that
A6: a21+a22+a23=1 & x2 = a21*y1+a22*y2+a23*y3;
ex x9 be Element of REAL n st x1 = x9 &
ex a19,a29,a39 being Real st a19+
a29+a39=1 & x9 = a19*y1+a29*y2+a39* y3 by A1,A5;
then consider a11,a12,a13 being Real such that
A7: a11+a12+a13=1 & x1 = a11*y1+a12*y2+a13*y3;
ex x9 be Element of REAL n st x3 = x9 &
ex a19,a29,a39 being Real st a19
+a29+a39=1 & x9 = a19*y1+a29*y2+a39 *y3 by A3,A5;
then consider a31,a32,a33 being Real such that
A8: a31+a32+a33=1 & x3 = a31*y1+a32*y2+a33*y3;
x3 = y1 + a32*(y2 - y1) + a33*(y3 - y1) by A8,Th27;
then
A9: x3 - x1 = y1 + a32*(y2 - y1) + a33*(y3 - y1) + -(y1 + a12*(y2 - y1) +
a13*(y3 - y1)) by A7,Th27
.= y1 + a32*(y2 - y1) + a33*(y3 - y1) + (-y1 + -a12*(y2 - y1) + -a13*(y3
- y1)) by Th8
.= (y1 + -y1) + (a32*(y2 - y1) + -a12*(y2 - y1)) + (a33*(y3 - y1) + -a13
*(y3 - y1)) by Th17
.= 0*n + (a32*(y2 - y1) + -a12*(y2 - y1)) + (a33*(y3 - y1) + -a13*(y3 -
y1)) by Th2
.= 0*n + (a32 - a12)*(y2 - y1) + (a33*(y3 - y1) + -a13*(y3 - y1)) by Th11
.= 0*n + (a32 - a12)*(y2 - y1) + (a33 - a13)*(y3 - y1) by Th11
.= (a32 - a12)*(y2 - y1) + (a33 - a13)*(y3 - y1) by EUCLID_4:1;
A10: x1 = y1 + a12*(y2 - y1) + a13*(y3 - y1) by A7,Th27;
then x2 - x1 = y1 + a22*(y2 - y1) + a23*(y3 - y1) + -(y1 + a12*(y2 - y1) +
a13*(y3 - y1)) by A6,Th27
.= y1 + a22*(y2 - y1) + a23*(y3 - y1) + (-y1 + -a12*(y2 - y1) + -a13*(y3
- y1)) by Th8
.= (y1 + -y1) + (a22*(y2 - y1) + -a12*(y2 - y1)) + (a23*(y3 - y1) + -a13
*(y3 - y1)) by Th17
.= 0*n + (a22*(y2 - y1) + -a12*(y2 - y1)) + (a23*(y3 - y1) + -a13*(y3 -
y1)) by Th2
.= 0*n + (a22 - a12)*(y2 - y1) + (a23*(y3 - y1) + -a13*(y3 - y1)) by Th11
.= 0*n + (a22 - a12)*(y2 - y1) + (a23 - a13)*(y3 - y1) by Th11
.= (a22 - a12)*(y2 - y1) + (a23 - a13)*(y3 - y1) by EUCLID_4:1;
then consider c1,c2,d1,d2 be Real such that
A11: y2 - y1 = c1*(x2 - x1) + c2*(x3 - x1) & y3 - y1 = d1*(x2 - x1) + d2
*(x3 - x1 ) by A4,A9,Th36;
A12: x1 = y1 + (a12*(y2 - y1) + a13*(y3 - y1)) by A10,RVSUM_1:15;
now
let y be object;
assume y in P;
then ex x9 be Element of REAL n st y = x9 &
ex a19,a29,a39 being Real st
a19+a29+a39=1 & x9 = a19*y1+a29*y2+a39 *y3 by A5;
then consider b1,b2,b3 being Real such that
A13: b1+b2+b3=1 & y = b1*y1+b2*y2+b3*y3;
y = y1 + b2*(y2 - y1) + b3*(y3 - y1) by A13,Th27
.= x1 - (a12*(y2 - y1) + a13*(y3 - y1)) + b2*(y2 - y1) + b3*(y3 - y1)
by A12,Th6
.= x1 - a12*(y2 - y1) - a13*(y3 - y1) + b2*(y2 - y1) + b3*(y3 - y1) by
RVSUM_1:39
.= x1 + -a12*(y2 - y1) + b2*(y2 - y1) + -a13*(y3 - y1) + b3*(y3 - y1)
by RVSUM_1:15
.= x1 + (-a12*(y2 - y1) + b2*(y2 - y1)) + -a13*(y3 - y1) + b3*(y3 - y1
) by RVSUM_1:15
.= x1 + (-a12*(y2 - y1) + b2*(y2 - y1)) + (-a13*(y3 - y1) + b3*(y3 -
y1)) by RVSUM_1:15
.= x1 + (b2-a12)*(y2 - y1) + (-a13*(y3 - y1) + b3*(y3 - y1)) by Th11
.= x1 + (b2-a12)*(y2 - y1) + (b3-a13)*(y3 - y1) by Th11
.= x1 + ((b2-a12)*(c1*(x2 - x1)) + (b2-a12)*(c2*(x3 - x1))) + (b3-a13)
*(d1*(x2 - x1) + d2*(x3 - x1)) by A11,EUCLID_4:6
.= x1 + ((b2-a12)*(c1*(x2 - x1)) + (b2-a12)*(c2*(x3 - x1))) + ((b3-a13
)*(d1*(x2 - x1)) + (b3-a13)*(d2*(x3 - x1))) by EUCLID_4:6
.= x1 + ((((b2-a12)*c1)*(x2 - x1)) + (b2-a12)*(c2*(x3 - x1))) + ((b3-
a13)*(d1*(x2 - x1)) + (b3-a13)*(d2*(x3 - x1))) by EUCLID_4:4
.= x1 + (((b2-a12)*c1)*(x2 - x1) + ((b2-a12)*c2)*(x3 - x1)) + ((b3-a13
)*(d1*(x2 - x1)) + (b3-a13)*(d2*(x3 - x1))) by EUCLID_4:4
.= x1 + (((b2-a12)*c1)*(x2 - x1) + ((b2-a12)*c2)*(x3 - x1)) + (((b3-
a13)*d1)*(x2 - x1) + (b3-a13)*(d2*(x3 - x1))) by EUCLID_4:4
.= x1 + (((b2-a12)*c1)*(x2 - x1) + ((b2-a12)*c2)*(x3 - x1)) + (((b3-
a13)*d1)*(x2 - x1) + ((b3-a13)*d2)*(x3 - x1)) by EUCLID_4:4
.= x1 + ((b2-a12)*c1)*(x2 - x1) + ((b2-a12)*c2)*(x3 - x1) + (((b3-a13)
*d1)*(x2 - x1) + ((b3-a13)*d2)*(x3 - x1)) by RVSUM_1:15
.= x1 + ((b2-a12)*c1)*(x2 - x1) + ((b2-a12)*c2)*(x3 - x1) + ((b3-a13)*
d1)*(x2 - x1) + ((b3-a13)*d2)*(x3 - x1) by RVSUM_1:15
.= x1 + ((b2-a12)*c1)*(x2 - x1) + ((b3-a13)*d1)*(x2 - x1) + ((b2-a12)*
c2)*(x3 - x1) + ((b3-a13)*d2)*(x3 - x1) by RVSUM_1:15
.= x1 + (((b2-a12)*c1)*(x2 - x1) + ((b3-a13)*d1)*(x2 - x1)) + ((b2-a12
)*c2)*(x3 - x1) + ((b3-a13)*d2)*(x3 - x1) by RVSUM_1:15
.= x1 + (((b2-a12)*c1)*(x2 - x1) + ((b3-a13)*d1)*(x2 - x1)) + (((b2-
a12)*c2)*(x3 - x1) + ((b3-a13)*d2)*(x3 - x1)) by RVSUM_1:15
.= x1 + ((b2-a12)*c1 + (b3-a13)*d1)*(x2 - x1) + (((b2-a12)*c2)*(x3 -
x1) + ((b3-a13)*d2)*(x3 - x1)) by EUCLID_4:7
.= x1 + ((b2-a12)*c1 + (b3-a13)*d1)*(x2 - x1) + ((b2-a12)*c2 + (b3-a13
)*d2)*(x3 - x1) by EUCLID_4:7;
then ex a be Real st y = a*x1 + ((b2-a12)*c1 + (b3-a13)*d1)*x2 +((b2-a12)*
c2 + (b3-a13)*d2)* x3 & a+((b2-a12)*c1 + (b3-a13)*d1)+((b2-a12)*c2 + (b3-a13)*
d2)=1 by Th28;
hence y in plane(x1,x2,x3);
end;
then
A14: P c= plane(x1,x2,x3);
plane(x1,x2,x3) c= P by A1,A2,A3,A5,Th83;
hence thesis by A14,XBOOLE_0:def 10;
end;
theorem
P1 is being_plane & P1 c= P2 implies P1 = P2
proof
assume that
A1: P1 is being_plane and
A2: P1 c= P2;
consider x1,x2,x3 be Element of REAL n such that
A3: x2 - x1, x3 - x1 are_lindependent2 & P1 = plane(x1,x2,x3) by A1;
A4: x3 in plane(x1,x2,x3) by Th82;
x1 in plane(x1,x2,x3) & x2 in plane(x1,x2,x3) by Th82;
hence thesis by A2,A3,A4,Th92;
end;
:: Lines in the planes
theorem
Line(x1,x2) c= plane(x1,x2,x3) & Line(x2,x3) c= plane(x1,x2,x3) & Line
(x3,x1) c= plane(x1,x2,x3)
proof
A1: x3 in plane(x1,x2,x3) by Th82;
x1 in plane(x1,x2,x3) & x2 in plane(x1,x2,x3) by Th82;
hence thesis by A1,Th85;
end;
theorem Th95:
x1 in P & x2 in P implies Line(x1,x2) c= P
proof
P in plane_of_REAL n;
then
A1: ex P9 being Subset of REAL n st P = P9 & ex y1,y2,y3 being Element of
REAL n st P9 = plane(y1,y2,y3);
assume x1 in P & x2 in P;
hence thesis by A1,Th85;
end;
definition
let n be Nat,L1,L2 be Element of line_of_REAL n;
pred L1,L2 are_coplane means
ex x1,x2,x3 being Element of REAL n st
L1 c= plane(x1,x2,x3) & L2 c= plane(x1,x2,x3);
end;
theorem Th96:
L1,L2 are_coplane iff ex P st L1 c= P & L2 c= P
proof
thus L1,L2 are_coplane implies ex P st L1 c= P & L2 c= P
proof
assume L1,L2 are_coplane;
then consider x1,x2,x3 being Element of REAL n such that
A1: L1 c= plane(x1,x2,x3) & L2 c= plane(x1,x2,x3);
set P = plane(x1,x2,x3);
take P;
thus thesis by A1,Th90;
end;
now
assume ex P st L1 c= P & L2 c= P;
then consider P such that
A2: L1 c= P & L2 c= P;
P in plane_of_REAL n;
then ex P9 being Subset of REAL n st P = P9 & ex x1,x2,x3 being Element of
REAL n st P9 = plane(x1,x2,x3);
hence L1,L2 are_coplane by A2;
end;
hence thesis;
end;
theorem Th97:
L1 // L2 implies L1,L2 are_coplane
proof
assume L1 // L2;
then consider x1, x2, y1, y2 being Element of REAL n such that
A1: L1 = Line(x1,x2) and
A2: L2 = Line(y1,y2) and
A3: (x2 - x1) // (y2 - y1);
consider a such that
a <> 0 and
A4: x2 - x1 = a * (y2 - y1) by A3,Th32;
A5: 1 + (-a) + a = 1;
y1 in plane(x1,y1,y2) & y2 in plane(x1,y1,y2) by Th82;
then
A6: L2 c= plane(x1,y1,y2) by A2,Th85;
x2 = x1 + a * (y2 - y1) by A4,Th6
.= 1 * x1 + a * (y2 - y1) by EUCLID_4:3
.= 1 * x1 + (a * y2 + (-a) * y1) by Th12
.= 1 * x1 + (-a) * y1 + a * y2 by RVSUM_1:15;
then
A7: x2 in plane(x1,y1,y2) by A5;
x1 in plane(x1,y1,y2) by Th82;
then L1 c= plane(x1,y1,y2) by A1,A7,Th85;
hence thesis by A6;
end;
theorem Th98:
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
proof
assume that
A1: L1 is being_line and
A2: L2 is being_line and
A3: L1,L2 are_coplane;
consider x1,x2,x3 being Element of REAL n such that
A4: L1 c= plane(x1,x2,x3) & L2 c= plane(x1,x2,x3) by A3;
consider y2,y3 such that
y2 <> y3 and
A5: L2 = Line(y2,y3) by A2;
consider y0,y1 such that
A6: y0 <> y1 and
A7: L1 = Line(y0,y1) by A1;
A8: y0 - y1 <> 0*n by A6,Th9;
set P = plane(x1,x2,x3);
A9: y2 in L2 by A5,EUCLID_4:9;
consider y being Element of REAL n such that
A10: y in Line(y0,y1) and
A11: y0 - y1,y2 - y are_orthogonal by Th43;
assume L1 misses L2;
then
A12: y <> y2 by A7,A9,A10,XBOOLE_0:3;
then y2 - y <> 0*n by Th9;
then
A13: y0 - y1 _|_ y2 - y by A11,A8;
consider y9 being Element of REAL n such that
A14: y <> y9 and
A15: y9 in L1 by A1,EUCLID_4:14;
take P;
y in Line(y,y2) & y2 in Line(y,y2) by EUCLID_4:9;
then
A16: P in plane_of_REAL n & y9 - y, y2 - y are_lindependent2 by A7,A10,A12,A13
,A14,A15,Th40,Th45;
then P = plane(y,y9,y2) by A4,A7,A9,A10,A15,Th92;
hence thesis by A4,A16;
end;
theorem Th99:
ex P st x in P & L c= P
proof
L in line_of_REAL n;
then consider x1,x2 being Element of REAL n such that
A1: L = Line(x1,x2);
take P = plane(x,x1,x2);
x1 in P & x2 in P by Th82;
hence thesis by A1,Th82,Th85,Th90;
end;
theorem Th100:
(not x in L) & L is being_line implies ex P st x in P & L c= P
& P is being_plane
proof
consider P being Element of plane_of_REAL n such that
A1: x in P & L c= P by Th99;
assume ( not x in L)& L is being_line;
then consider x1,x2 being Element of REAL n such that
A2: L = Line(x1,x2) and
A3: x - x1,x2 - x1 are_lindependent2 by Th55;
take P;
x1 in L & x2 in L by A2,EUCLID_4:9;
then P = plane(x1,x,x2) by A1,A3,Th92;
hence thesis by A1,A3;
end;
theorem Th101:
x in P & L c= P & (not x in L) & L is being_line implies P is being_plane
proof
assume
A1: x in P & L c= P;
assume ( not x in L)& L is being_line;
then consider x1,x2 being Element of REAL n such that
A2: L = Line(x1,x2) and
A3: x - x1,x2 - x1 are_lindependent2 by Th55;
x1 in L & x2 in L by A2,EUCLID_4:9;
then P = plane(x1,x,x2) by A1,A3,Th92;
hence thesis by A3;
end;
theorem Th102:
(not x in L) & L is being_line & x in P0 & L c= P0 & x in P1 &
L c= P1 implies P0 = P1
proof
assume that
A1: ( not x in L)& L is being_line and
A2: x in P0 & L c= P0 and
A3: x in P1 & L c= P1;
consider x1,x2 being Element of REAL n such that
A4: L = Line(x1,x2) and
A5: x - x1,x2 - x1 are_lindependent2 by A1,Th55;
A6: x1 in L & x2 in L by A4,EUCLID_4:9;
then P0 = plane(x1,x,x2) by A2,A5,Th92;
hence thesis by A3,A5,A6,Th92;
end;
theorem
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
proof
assume that
A1: L1 is being_line and
A2: L2 is being_line & L1,L2 are_coplane & L1 <> L2;
(ex P st L1 c= P & L2 c= P )& ex x st x in L2 & not x in L1 by A1,A2,Th79
,Th96;
hence thesis by A1,Th101;
end;
theorem
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
proof
let L1,L2;
assume that
A1: L1 is being_line and
A2: L2 is being_line and
A3: L1 <> L2 and
A4: L1 meets L2;
consider x such that
A5: x in L1 and
A6: not x in L2 by A1,A2,A3,Th79;
A7: ex P st x in P & L2 c= P & P is being_plane by A2,A6,Th100;
consider y such that
A8: y in L1 and
A9: y in L2 by A4,Th49;
L1 = Line(x,y) by A1,A5,A6,A8,A9,Th30;
hence thesis by A7,A9,Th95;
end;
theorem
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
proof
assume that
A1: L1 is being_line and
A2: L2 is being_line and
A3: L1 <> L2 and
A4: L1 c= P1 & L2 c= P1 and
A5: L1 c= P2 & L2 c= P2;
consider x such that
A6: x in L1 and
A7: not x in L2 by A1,A2,A3,Th79;
consider x1,x2 such that
A8: L2 = Line(x1,x2) and
A9: x - x1,x2 - x1 are_lindependent2 by A2,A7,Th55;
A10: x1 in L2 & x2 in L2 by A8,EUCLID_4:9;
then P2 = plane(x1,x,x2) by A5,A6,A9,Th92;
hence thesis by A4,A6,A9,A10,Th92;
end;
theorem Th106:
L1 // L2 & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane
proof
assume that
A1: L1 // L2 and
A2: L1 <> L2;
A3: L2 is being_line by A1,Th66;
L1,L2 are_coplane & L1 is being_line by A1,Th66,Th97;
hence thesis by A1,A2,A3,Th71,Th98;
end;
theorem Th107:
L1 _|_ L2 & L1 meets L2 implies ex P st P is being_plane & L1 c= P & L2 c= P
proof
assume that
A1: L1 _|_ L2 and
A2: L1 meets L2;
consider x1 such that
A3: x1 in L1 and
A4: x1 in L2 by A2,Th49;
L1 is being_line by A1,Th67;
then consider x2 such that
A5: x2 <> x1 & x2 in L1 by Th53;
A6: L1 = Line(x1,x2) by A3,A5,Th64;
L2 is being_line by A1,Th67;
then consider x3 such that
A7: x3 <> x1 & x3 in L2 by Th53;
reconsider P = plane(x1,x2,x3) as Subset of REAL n;
take P;
A8: x1 in P & x2 in P by Th82;
A9: x3 in P by Th82;
A10: L2 = Line(x1,x3) by A4,A7,Th64;
x2 - x1,x3 - x1 are_lindependent2 by A1,A3,A4,A5,A7,Th45,Th74;
hence thesis by A6,A10,A8,A9,Th85,Th90;
end;
theorem Th108:
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
proof
assume that
A1: L0 c= P and
A2: L1 c= P and
A3: L2 c= P and
A4: x in L0 and
A5: x in L1 and
A6: x in L2;
A7: L1 meets L0 by A4,A5,Th49;
assume that
A8: L0 _|_ L2 and
A9: L1 _|_ L2;
consider x0 such that
A10: x <> x0 and
A11: x0 in L0 and
not x0 in L2 by A6,A8,Th81;
L1 is being_line by A9,Th67;
then consider x1 such that
A12: x1 <> x and
A13: x1 in L1 by Th53;
consider x2 such that
A14: x <> x2 and
A15: x2 in L2 and
not x2 in L1 by A5,A9,Th81;
A16: x0 - x _|_ x2 - x by A4,A6,A8,A10,A11,A14,A15,Th74;
then P = plane(x,x0,x2) by A1,A3,A4,A11,A15,Th45,Th92;
then consider a1,a2,a3 such that
A17: a1 + a2 + a3 = 1 & x1 = a1 * x + a2 * x0 + a3 * x2 by A2,A13,Th88;
x0 - x,x2 - x are_orthogonal by A16;
then
A18: |(x0 - x,x2 - x)|=0 by RVSUM_1:def 17;
A19: x1 - x = -x + (x + a2*(x0 - x) + a3*(x2 - x)) by A17,Th27
.= -x + (x + (a2*(x0 - x) + a3*(x2 - x))) by RVSUM_1:15
.= (-x + x) + (a2*(x0 - x) + a3*(x2 - x)) by RVSUM_1:15
.= 0*n + (a2*(x0 - x) + a3*(x2 - x)) by Th2
.= a2*(x0 - x) + a3*(x2 - x) by EUCLID_4:1;
x2 - x <> 0*n by A14,Th9;
then
A20: |(x2 - x,x2 - x)| <> 0 by EUCLID_4:17;
x1 - x _|_ x2 - x by A5,A6,A9,A14,A15,A12,A13,Th74;
then x1 - x,x2 - x are_orthogonal;
then 0 = |(a2*(x0 - x) + a3*(x2 - x),x2 - x)| by A19,RVSUM_1:def 17
.= |(a2*(x0 - x),x2 - x)| + |(a3*(x2 - x),x2 - x)| by EUCLID_4:20
.= a2*|(x0 - x,x2 - x)| + |(a3*(x2 - x),x2 - x)| by EUCLID_4:21
.= a3*|(x2 - x,x2 - x)| by A18,EUCLID_4:21;
then
A21: x1 - x = a2*(x0 - x) + 0 * (x2 - x) by A19,A20,XCMPLX_1:6
.= a2*(x0 - x) + 0*n by EUCLID_4:3
.= a2*(x0 - x) by EUCLID_4:1;
A22: x0 - x <> 0*n by A10,Th9;
x1 - x <> 0*n by A12,Th9;
then
A23: x1 - x // x0 - x by A21,A22;
A24: L1 = Line(x,x1) by A5,A12,A13,Th64;
L0 = Line(x,x0) by A4,A10,A11,Th64;
then L1 // L0 by A24,A23;
hence thesis by A7,Th71;
end;
theorem Th109:
L1,L2 are_coplane & L1 _|_ L2 implies L1 meets L2
proof
assume
A1: L1,L2 are_coplane;
assume
A2: L1 _|_ L2;
then
A3: L2 is being_line by Th67;
L1 is being_line by A2,Th67;
then consider x0 such that
A4: x0 in L1 and
A5: not x0 in L2 by A2,A3,Th75,Th79;
consider L such that
A6: x0 in L and
A7: L _|_ L2 and
A8: L meets L2 by A3,A5,Th62;
consider x such that
A9: x in L and
A10: x in L2 by A8,Th49;
x in L1
proof
A11: L1 meets L by A4,A6,Th49;
consider P such that
P is being_plane and
A12: L c= P & L2 c= P by A7,A8,Th107;
consider P0 such that
A13: L1 c= P0 & L2 c= P0 by A1,Th96;
A14: P = P0 by A3,A4,A5,A6,A13,A12,Th102;
consider L0 such that
A15: x in L0 and
A16: L0 _|_ L2 and
A17: L0 // L1 by A2,Th80;
assume
A18: not x in L1;
then consider P1 such that
A19: L0 c= P1 and
A20: L1 c= P1 and
P1 is being_plane by A15,A17,Th106;
L1 is being_line by A17,Th66;
then P = P1 by A10,A18,A13,A14,A15,A19,A20,Th102;
then L = L0 by A7,A9,A10,A12,A15,A16,A19,Th108;
hence contradiction by A18,A15,A17,A11,Th71;
end;
hence thesis by A10,Th49;
end;
theorem Th110:
L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0
implies L0 c= P & L0 _|_ L1
proof
assume that
A1: L1 c= P & L2 c= P and
A2: L1 _|_ L2 and
A3: x in P;
L1,L2 are_coplane by A1,Th96;
then L1 meets L2 by A2,Th109;
then consider x0 such that
A4: x0 in L1 and
A5: x0 in L2 by Th49;
L2 is being_line by A2,Th67;
then consider x1 such that
A6: x1 <> x0 and
A7: x1 in L2 by Th53;
A8: plane(x,x1,x0) c= P by A1,A3,A4,A7,Th91;
assume that
A9: L0 // L2 and
A10: x in L0;
L0 is being_line by A9,Th66;
then consider x2 such that
A11: x2 <> x & x2 in L0 by Th53;
consider a such that
a <> 0 and
A12: x2 - x = a*(x1 - x0) by A9,A10,A5,A6,A7,A11,Th32,Th77;
A13: 1 + a + (-a) = 1;
x2 = x + a*(x1 - x0) by A12,Th6
.= 1 * x + a*(x1 - x0) by EUCLID_4:3
.= 1 * x + (a * x1 + (-a) * x0) by Th12
.= 1 * x + a * x1 + (-a) * x0 by RVSUM_1:15;
then
A14: x2 in plane(x,x1,x0) by A13;
L0 = Line(x2,x) by A10,A11,Th64;
hence thesis by A2,A3,A9,A14,A8,Th61,Th95;
end;
theorem Th111:
L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2
proof
assume that
A1: L c= P and
A2: L1 c= P and
A3: L2 c= P;
assume that
A4: L _|_ L1 and
A5: L _|_ L2;
L,L2 are_coplane by A1,A3,Th96;
then L meets L2 by A5,Th109;
then consider x2 such that
A6: x2 in L and
A7: x2 in L2 by Th49;
A8: L1 is being_line by A4,Th67;
L,L1 are_coplane by A1,A2,Th96;
then L meets L1 by A4,Th109;
then consider x1 such that
A9: x1 in L and
A10: x1 in L1 by Th49;
A11: L2 is being_line by A5,Th67;
now
per cases;
case
x1 = x2;
hence thesis by A1,A2,A3,A4,A5,A9,A10,A7,A8,Th65,Th108;
end;
case
A12: x1 <> x2;
then x1 - x2 <> 0*n by Th9;
then
A13: |(x1 - x2,x1 - x2)| <> 0 by EUCLID_4:17;
consider x such that
A14: x <> x2 and
A15: x in L2 by A11,Th53;
A16: L2 = Line(x2,x) by A7,A14,A15,Th64;
consider x0 such that
A17: x0 <> x1 and
A18: x0 in L1 by A8,Th53;
A19: L1 = Line(x0,x1) by A10,A17,A18,Th64;
A20: x0 - x1 _|_ x2 - x1 by A4,A9,A10,A6,A12,A17,A18,Th74;
then x0 - x1,x2 - x1 are_orthogonal;
then
A21: |(x0 - x1,x2 - x1)|=0 by RVSUM_1:def 17;
P = plane(x1,x0,x2) by A1,A2,A9,A6,A18,A20,Th45,Th92;
then consider a1,a3,a2 such that
A22: a1+a3+a2=1 and
A23: x = a1*x1+a3*x0+a2*x2 by A3,A15,Th88;
A24: a2+a1+a3=1 by A22;
A25: x - x2 = -x2 + (a2*x2+a1*x1+a3*x0) by A23,RVSUM_1:15
.= -x2 + (x2 + a1*(x1 - x2) + a3*(x0 - x2)) by A24,Th27
.= -x2 + (x2 + (a1*(x1 - x2) + a3*(x0 - x2))) by RVSUM_1:15
.= (-x2 + x2) + (a1*(x1 - x2) + a3*(x0 - x2)) by RVSUM_1:15
.= 0*n + (a1*(x1 - x2) + a3*(x0 - x2)) by Th2
.= a1*(x1 - x2) + a3*(x0 - x2) by EUCLID_4:1;
A26: |(x0 - x1,x1 - x2)| = |(x0 - x1,(-1)*x2 + --x1)|
.= |(x0 - x1,(-1)*(x2 + -x1))| by EUCLID_4:6
.= (-1)*|(x0 - x1,x2 - x1)| by EUCLID_4:22
.= 0 by A21;
A27: x0 - x2 = x0 - (0*n + x2) by EUCLID_4:1
.= x0 - ((x1 - x1) + x2) by Th2
.= x0 - (x1 - x1) - x2 by RVSUM_1:39
.= x0 - x1 + x1 - x2 by Th4
.= (x0 - x1) + (x1 - x2) by Th5;
x - x2 _|_ x1 - x2 by A5,A9,A6,A7,A12,A14,A15,Th74;
then x - x2,x1 - x2 are_orthogonal;
then 0 = |(a1*(x1 - x2) + a3*(x0 - x2),x1 - x2)| by A25,RVSUM_1:def 17
.= |(a1*(x1 - x2),x1 - x2)|+|(a3*(x0 - x2),x1 - x2)| by EUCLID_4:20
.= a1*|(x1 - x2,x1 - x2)|+|(a3*(x0 - x2),x1 - x2)| by EUCLID_4:21
.= a1*|(x1 - x2,x1 - x2)|+a3*|(x0 - x2,x1 - x2)| by EUCLID_4:21
.= a1*|(x1 - x2,x1 - x2)| +a3*(|(x0 - x1,x1 - x2)| + |(x1 - x2,x1 -
x2)|) by A27,EUCLID_4:20
.= (a1+a3)*|(x1 - x2,x1 - x2)| by A26;
then a1+a3 = 0 by A13,XCMPLX_1:6;
then a3 = -a1;
then
A28: x - x2 = a1*((x1 + -x2) - (x0 - x2)) by A25,Th12
.= a1*((x1 - x0) + (-x2 - -x2)) by Th18
.= a1*((x1 - x0) + 0*n) by Th2
.= a1*(x1 - x0) by EUCLID_4:1;
A29: x1 - x0 <> 0*n by A17,Th9;
x - x2 <> 0*n by A14,Th9;
then x - x2 // x1 - x0 by A28,A29;
hence thesis by A19,A16;
end;
end;
hence thesis;
end;
theorem Th112:
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
proof
assume that
A1: L0 c= P & L1 c= P and
A2: L2 c= P and
A3: L0 // L1 and
A4: L1 // L2 and
A5: L0 <> L1;
A6: L1 is being_line by A3,Th66;
assume that
A7: L meets L0 and
A8: L meets L1;
consider x0 such that
A9: x0 in L and
A10: x0 in L0 by A7,Th49;
A11: L0 misses L1 by A3,A5,Th71;
then not x0 in L1 by A10,Th49;
then consider L9 being Element of line_of_REAL n such that
A12: x0 in L9 and
A13: L9 _|_ L1 and
A14: L9 meets L1 by A6,Th62;
consider y1 such that
A15: y1 in L9 and
A16: y1 in L1 by A14,Th49;
A17: x0 <> y1 by A10,A11,A16,Th49;
then
A18: L9 = Line(x0,y1) by A12,A15,Th64;
then L9 c= P by A1,A10,A16,Th95;
then L9,L2 are_coplane by A2,Th96;
then
A19: L9 meets L2 by A4,A13,Th61,Th109;
then consider y2 such that
A20: y2 in L9 and
A21: y2 in L2 by Th49;
consider a such that
A22: y2 - x0 = a*(y1 - x0) by A12,A15,A17,A20,Th70;
L2 is being_line by A4,Th66;
then consider x2 such that
A23: x2 <> y2 & x2 in L2 by Th53;
consider x1 such that
A24: x1 in L and
A25: x1 in L1 by A8,Th49;
x0 <> x1 by A10,A25,A11,Th49;
then
A26: L = Line(x0,x1) by A9,A24,Th64;
A27: L2 = Line(y2,x2) by A21,A23,Th64;
now
per cases;
case
x1 = y1;
hence thesis by A9,A24,A17,A18,A19,Th64;
end;
case
A28: x1 <> y1;
set x = (1 - a)*x0 + a*x1;
consider b such that
A29: b <> 0 and
A30: x2 - y2 = b*(x1 - y1) by A4,A25,A16,A21,A23,A28,Th32,Th77;
A31: x1 - y1 = 1 * (x1 - y1) by EUCLID_4:3
.= (1/b*b)*(x1 - y1) by A29,XCMPLX_1:87
.= 1/b*(x2 - y2) by A30,EUCLID_4:4;
x = 1 * x0 + -a*x0 + a*x1 by Th11
.= x0 + -a*x0 + a*x1 by EUCLID_4:3
.= (a*x1 + -a*x0) + x0 by RVSUM_1:15
.= a*(x1 - x0) + x0 by Th12
.= a*(x1 + 0*n + -x0) + x0 by EUCLID_4:1
.= a*(x1 + (-y1 + y1) + -x0) + x0 by Th2
.= a*(x1 + -y1 + y1 + -x0) + x0 by RVSUM_1:15
.= a*(x1 - y1 + (y1 + -x0)) + x0 by RVSUM_1:15
.= a*((1/b)*(x2 - y2)) + a*(y1 - x0) + x0 by A31,EUCLID_4:6
.= (a*(1/b))*(x2 - y2) + a*(y1 - x0) + x0 by EUCLID_4:4
.= (a/b)*(x2 - y2) + a*(y1 - x0) + x0 by XCMPLX_1:99
.= (a/b)*(x2 - y2) + (y2 + -x0 + x0) by A22,RVSUM_1:15
.= (a/b)*(x2 - y2) + (y2 + (-x0 + x0)) by RVSUM_1:15
.= (a/b)*(x2 - y2) + (y2 + 0*n) by Th2
.= (a/b)*(x2 - y2) + y2 by EUCLID_4:1
.= (a/b)*x2 + -(a/b)*y2 + y2 by Th12
.= y2 + -(a/b)*y2 + (a/b)*x2 by RVSUM_1:15
.= 1 * y2 + -(a/b)*y2 + (a/b)*x2 by EUCLID_4:3
.= (1 - a/b)* y2 + (a/b)*x2 by Th11;
then
A32: x in L2 by A27;
x in L by A26;
hence thesis by A32,Th49;
end;
end;
hence thesis;
end;
theorem Th113:
L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1
misses L2 implies L1 // L2
proof
assume that
A1: L1,L2 are_coplane and
A2: L1 is being_line and
A3: L2 is being_line;
assume
A4: L1 misses L2;
then consider x such that
A5: x in L1 and
A6: not x in L2 by Th63;
consider P such that
A7: L1 c= P and
A8: L2 c= P by A1,Th96;
consider L9 being Element of line_of_REAL n such that
A9: x in L9 and
A10: L9 _|_ L2 and
A11: L9 meets L2 by A3,A6,Th62;
consider x2 such that
A12: x2 in L9 and
A13: x2 in L2 by A11,Th49;
consider L0 such that
A14: x in L0 and
A15: L0 _|_ L9 and
A16: L0 // L2 by A10,Th80;
L9 = Line(x2,x) by A6,A9,A12,A13,Th64;
then
A17: L9 c= P by A5,A7,A8,A13,Th95;
then
A18: L0 c= P by A8,A9,A10,A14,A16,Th110;
A19: L9 is being_line by A15,Th67;
consider x1 such that
A20: x1 <> x and
A21: x1 in L1 by A2,Th53;
A22: L1 = Line(x,x1) by A5,A20,A21,Th64;
A23: L0 meets L1 by A5,A14,Th49;
L1 = L0
proof
A24: not x1 in L9 by A4,A9,A11,A20,A22,Th64;
then consider L such that
A25: x1 in L and
A26: L9 _|_ L and
A27: L9 meets L by A19,Th62;
A28: L meets L1 by A21,A25,Th49;
assume L1 <> L0;
then
A29: L <> L0 by A14,A20,A22,A25,Th64;
consider x9 being Element of REAL n such that
A30: x9 in L9 and
A31: x9 in L by A27,Th49;
L = Line(x9,x1) by A24,A25,A30,A31,Th64;
then
A32: L c= P by A7,A17,A21,A30,Th95;
then L // L0 by A17,A15,A18,A26,Th111;
hence contradiction by A4,A8,A16,A18,A23,A32,A29,A28,Th112;
end;
hence thesis by A16;
end;
theorem
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)
proof
reconsider L1 = Line(x1,x2), L2 = Line(y1,y2) as Element of line_of_REAL n
by Th47;
assume that
A1: x1 in P & x2 in P & y1 in P & y2 in P and
A2: x2 - x1, y2 - y1 are_lindependent2;
A3: x1 in L1 & x2 in L1 by EUCLID_4:9;
L1 c= P & L2 c= P by A1,Th95;
then
A4: L1,L2 are_coplane by Th96;
A5: y1 in L2 & y2 in L2 by EUCLID_4:9;
y2 - y1 <> 0*n by A2,Lm2;
then
A6: y2 <> y1 by Th9;
then
A7: L2 is being_line;
x2 - x1 <> 0*n by A2,Lm2;
then
A8: x2 <> x1 by Th9;
then
A9: L1 is being_line;
L1 meets L2
proof
assume L1 misses L2;
then L1 // L2 by A4,A9,A7,Th113;
hence contradiction by A2,A8,A6,A3,A5,Lm3,Th77;
end;
hence thesis;
end;