:: Lines in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received August 8, 2003
:: Copyright (c) 2003-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 REAL_1, NAT_1, SUBSET_1, NUMBERS, CARD_1, RELAT_1, ARYTM_3,
EUCLID, FINSEQ_2, COMPLEX1, ARYTM_1, INCSP_1, TARSKI, XBOOLE_0, AFF_1,
SQUARE_1, RVSUM_1, FINSEQ_1, XXREAL_0, PRE_TOPC, SEQ_4, XXREAL_2,
STRUCT_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_2, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, STRUCT_0, PRE_TOPC, FINSEQ_1, FINSEQ_2,
RVSUM_1, SQUARE_1, RLVECT_1, EUCLID, SEQ_4, XXREAL_0, RLTOPSP1;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_4, FINSEQOP, MONOID_0,
EUCLID, RELSET_1, BINOP_1;
registrations RELSET_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED, MONOID_0, EUCLID,
VALUED_0, VALUED_1, SQUARE_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_2;
equalities SQUARE_1, RVSUM_1, EUCLID, VALUED_1, RLTOPSP1;
expansions XBOOLE_0, RVSUM_1;
theorems EUCLID, SQUARE_1, SEQ_4, XCMPLX_1, RVSUM_1, EUCLID_2, XREAL_1,
FINSEQOP, CARD_1, RLTOPSP1;
begin
reserve a,b,s,t,u,lambda for Real,
n for Nat;
reserve x,x1,x2,x3,y1,y2 for Element of REAL n;
theorem Th1: :: EUCLID:31
0 * x + x = x & x + 0*n = x
proof
reconsider x9 = x as Element of n-tuples_on REAL;
0 *x + x = 0 *x9 + 1*x9 by RVSUM_1:52
.= (0+1)*x9 by RVSUM_1:50
.= x by RVSUM_1:52;
hence thesis by RVSUM_1:16;
end;
theorem Th2: :: EUCLID:32
a*(0*n) = 0*n
proof
|.a*(0*n).| = |.a.|*|.0*n.| by EUCLID:11
.= |.a.|*0 by EUCLID:7
.= 0;
hence thesis by EUCLID:8;
end;
theorem Th3: :: EUCLID:33
1*x = x & 0 * x = 0*n
proof
reconsider x9 = x as Element of n-tuples_on REAL;
(0)*x = (0)*x9 + x9 - x9 by RVSUM_1:42
.= x9 - x9 by Th1
.= 0*n by RVSUM_1:37;
hence thesis by RVSUM_1:52;
end;
theorem :: EUCLID:34
(a*b)*x = a*(b*x) by RVSUM_1:49;
theorem :: EUCLID:35
a*x = 0*n implies a = 0 or x = 0*n
proof
assume that
A1: a*x = 0*n and
A2: a <> 0;
thus x = 1*x by Th3
.= ((1/a)*a)*x by A2,XCMPLX_1:106
.= (1/a)*(a*x) by RVSUM_1:49
.= 0*n by A1,Th2;
end;
theorem :: EUCLID:36
a*(x1 + x2) = a*x1 + a*x2 by RVSUM_1:51;
theorem :: EUCLID:37
(a + b)*x = a*x + b*x by RVSUM_1:50;
theorem :: EUCLID:38
a*x1 = a*x2 implies a = 0 or x1 = x2
proof
assume that
A1: a*x1 = a*x2 and
A2: a <> 0;
((1/a)*a)*x1 = (1/a)*(a*x2) by A1,RVSUM_1:49;
then ((1/a)*a)*x1 = ((1/a)*a)*x2 by RVSUM_1:49;
then 1*x1 = ((1/a)*a)*x2 by A2,XCMPLX_1:106;
then 1*x1 = 1*x2 by A2,XCMPLX_1:106;
hence x1 = 1*x2 by Th3
.= x2 by Th3;
end;
definition
let n;
let x1,x2 be Element of REAL n;
func Line(x1,x2) -> Subset of REAL n equals
the set of all (1-lambda)*x1 + lambda*x2 ;
coherence
proof
set A = the set of all (1-lambda)*x1 + lambda*x2 ;
A c= REAL n
proof
let x be object;
assume x in A;
then ex lambda st x = (1-lambda)*x1 + lambda*x2;
hence thesis;
end;
hence thesis;
end;
end;
registration
let n;
let x1,x2 be Element of REAL n;
cluster Line(x1,x2) -> non empty;
coherence
proof
A1: 1 - 0 = 1 & 1 * x1 = x1 by Th3;
0 * x2 = 0*n & x1 + 0*n = x1 by Th1,Th3;
then x1 in Line(x1,x2) by A1;
hence thesis;
end;
end;
Lm1: Line(x1,x2) c= Line(x2,x1)
proof
let z be object;
assume z in Line(x1,x2);
then consider t such that
A1: z = (1-t)*x1 + t*x2;
z = (1-(1-t))*x2 + (1-t)*x1 by A1;
hence thesis;
end;
definition
let n;
let x1,x2 be Element of REAL n;
redefine func Line(x1,x2); :: redefines Line (EUCLID_4, definition)
commutativity
by Lm1;
end;
theorem Th9: :: AFF_1:26
x1 in Line(x1,x2) & x2 in Line(x1,x2)
proof
A1: 1 - 0 = 1 & 1*x1 = x1 by Th3;
A2: 1 - 1 = 0 & (0)*x1 = 0*n by Th3;
A3: 1*x2 = x2 & 0*n + x2 = x2 by Th1,Th3;
(0)*x2 = 0*n & x1 + 0*n = x1 by Th1,Th3;
hence thesis by A1,A2,A3;
end;
Lm2: x1 + (x2 + x3) = (x1 + x2) + x3 by FINSEQOP:28;
theorem Th10: :: AFF_1:27
y1 in Line(x1,x2) & y2 in Line(x1,x2) implies Line(y1,y2) c= Line(x1,x2)
proof
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;
let z be object;
assume z in Line(y1,y2);
then consider u such that
A3: z = (1-u)*y1 + u*y2;
z = ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+u*((1-s)*x1+s*x2) by A1,A2,A3,
RVSUM_1:51
.= ((1-u)*((1-t)*x1)+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2)) by RVSUM_1:51
.= (((1-u)*(1-t))*x1+(1-u)*(t*x2))+(u*((1-s)*x1)+u*(s*x2)) by RVSUM_1:49
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+(u*((1-s)*x1)+u*(s*x2)) by RVSUM_1:49
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+u*(s*x2)) by RVSUM_1:49
.= (((1-u)*(1-t))*x1+((1-u)*t)*x2)+((u*(1-s))*x1+(u*s)*x2) by RVSUM_1:49
.= ((1-u)*(1-t))*x1+(((1-u)*t)*x2+((u*(1-s))*x1+(u*s)*x2)) by FINSEQOP:28
.= ((1-u)*(1-t))*x1+((u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2)) by Lm2
.= (((1-u)*(1-t))*x1+(u*(1-s))*x1)+(((1-u)*t)*x2+(u*s)*x2) by FINSEQOP:28
.= ((1-u)*(1-t)+u*(1-s))*x1+(((1-u)*t)*x2+(u*s)*x2) by RVSUM_1:50
.= (1-(1*t-u*t+u*s))*x1+(1*t-u*t+u*s)*x2 by RVSUM_1:50;
hence z in Line(x1,x2);
end;
theorem Th11: :: AFF_1:28
y1 in Line(x1,x2) & y2 in Line(x1,x2) & y1<>y2 implies Line(x1,
x2) c= Line(y1,y2)
proof
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;
assume y1<>y2;
then
A3: t-s<>0 by A1,A2;
then
(1-((t-1)/(t-s)))*y1 + ((t-1)/(t-s))*y2 = ((1*(t-s)-(t-1))/(t-s))*y1 + (
(t-1)/(t-s))*y2 by XCMPLX_1:127
.= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + ((t-1)/(t-s))*(
(1-s)*x1 + s*x2) by A1,A2,RVSUM_1:51
.= (((-s+1)/(t-s))*((1-t)*x1) + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RVSUM_1:51
.= ((((-s+1)/(t-s))*(1-t))*x1 + ((-s+1)/(t-s))*(t*x2)) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + (((t-1)/(t-s))*
((1-s)*x1) + ((t-1)/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + ((t-1)/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s+1)/(t-s))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by RVSUM_1:49
.= ((((-s+1)*(1/(t-s)))*(1-t))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t
-s))*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))*(1/(t-s)))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t
-s))*(1-s))*x1 + (((t-1)/(t-s))*s)*x2)
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)/(t-s))*t)*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*(1/(t-s)))*t)*x2) + ((((t-1)/(t
-s))*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)*(1/(t-s)))*x2) + ((((t-1)/(t
-s))*(1-s))*x1 + (((t-1)/(t-s))*s)*x2)
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)/(t-s))
*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1/(t-
s)))*(1-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1-s))
*(1/(t-s)))*x1 + (((t-1)/(t-s))*s)*x2)
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1-s))
/(t-s))*x1 + (((t-1)/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1-s))
/(t-s))*x1 + (((t-1)*(1/(t-s)))*s)*x2) by XCMPLX_1:99
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1-s))
/(t-s))*x1 + (((t-1)*s)*(1/(t-s)))*x2)
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((-s+1)*t)/(t-s))*x2) + ((((t-1)*(1-s))
/(t-s))*x1 + (((t-1)*s)/(t-s))*x2) by XCMPLX_1:99
.= (((-s+1)*(1-t))/(t-s))*x1 + ((((-s+1)*t)/(t-s))*x2 + ((((t-1)*(1-s))/
(t-s))*x1 + (((t-1)*s)/(t-s))*x2)) by FINSEQOP:28
.= (((-s+1)*(1-t))/(t-s))*x1 + ((((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/
(t-s))*x2 + (((t-1)*s)/(t-s))*x2)) by Lm2
.= ((((-s+1)*(1-t))/(t-s))*x1 + (((t-1)*(1-s))/(t-s))*x1) + ((((-s+1)*t)
/(t-s))*x2 + (((t-1)*s)/(t-s))*x2) by FINSEQOP:28
.= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + ((((-s+1)*t)/(t-s))
*x2 + (((t-1)*s)/(t-s))*x2) by RVSUM_1:50
.= (((-s+1)*(1-t))/(t-s) + ((t-1)*(1-s))/(t-s))*x1 + (((-s+1)*t)/(t-s) +
((t-1)*s)/(t-s))*x2 by RVSUM_1:50
.= (((-s+1)*(1-t)+(t-1)*(1-s))/(t-s))*x1 + (((-s+1)*t)/(t-s) + ((t-1)*s)
/(t-s))*x2 by XCMPLX_1:62
.= (((1-t)*(1-s)+-(1-t)*(1-s))/(t-s))*x1 + (((-s+1)*t + (t-1)*s)/(t-s))*
x2 by XCMPLX_1:62
.= 0*n + (((-s+1)*t + (t-1)*s)/(t-s))*x2 by Th3
.= (1*(t-s)/(t-s))*x2 by Th1
.= 1*x2 by A3,XCMPLX_1:89
.= x2 by Th3;
then
A4: x2 in Line(y1,y2);
(1-(t/(t-s)))*y1 + (t/(t-s))*y2 = ((1*(t-s)-t)/(t-s))*y1 + (t/(t-s))*y2
by A3,XCMPLX_1:127
.= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + (t/(t-s))*((1-s)*x1
+ s*x2) by A1,A2,RVSUM_1:51
.= (((-s)/(t-s))*((1-t)*x1) + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RVSUM_1:51
.= ((((-s)/(t-s))*(1-t))*x1 + ((-s)/(t-s))*(t*x2)) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + ((t/(t-s))*((1-s)*
x1) + (t/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))*
x1 + (t/(t-s))*(s*x2)) by RVSUM_1:49
.= ((((-s)/(t-s))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))*
x1 + ((t/(t-s))*s)*x2) by RVSUM_1:49
.= ((((-s)*(1/(t-s)))*(1-t))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-
s))*x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))*(1/(t-s)))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-
s))*x1 + ((t/(t-s))*s)*x2)
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)/(t-s))*t)*x2) + (((t/(t-s))*(1-s))*
x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*(1/(t-s)))*t)*x2) + (((t/(t-s))*(1-
s))*x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)*(1/(t-s)))*x2) + (((t/(t-s))*(1-
s))*x1 + ((t/(t-s))*s)*x2)
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t/(t-s))*(1-s))*
x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1/(t-s)))*(1-
s))*x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1-s))*(1/(t-s
)))*x1 + ((t/(t-s))*s)*x2)
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1-s))/(t-s))*
x1 + ((t/(t-s))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1-s))/(t-s))*
x1 + ((t*(1/(t-s)))*s)*x2) by XCMPLX_1:99
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1-s))/(t-s))*
x1 + ((t*s)*(1/(t-s)))*x2)
.= ((((-s)*(1-t))/(t-s))*x1 + (((-s)*t)/(t-s))*x2) + (((t*(1-s))/(t-s))*
x1 + ((t*s)/(t-s))*x2) by XCMPLX_1:99
.= (((-s)*(1-t))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + (((t*(1-s))/(t-s))*
x1 + ((t*s)/(t-s))*x2)) by FINSEQOP:28
.= (((-s)*(1-t))/(t-s))*x1 + (((t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))*
x2 + ((t*s)/(t-s))*x2)) by Lm2
.= ((((-s)*(1-t))/(t-s))*x1 + ((t*(1-s))/(t-s))*x1) + ((((-s)*t)/(t-s))*
x2 + ((t*s)/(t-s))*x2) by FINSEQOP:28
.= (((-s)*(1-t))/(t-s) + (t*(1-s))/(t-s))*x1 + ((((-s)*t)/(t-s))*x2 + ((
t*s)/(t-s))*x2) by RVSUM_1:50
.= (((-s)*(1-t))/(t-s) + (t*(1-s))/(t-s))*x1 + (((-s)*t)/(t-s) + (t*s)/(
t-s))*x2 by RVSUM_1:50
.= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + (((-s)*t)/(t-s) + (t*s)/(t-s))*x2
by XCMPLX_1:62
.= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + (((-s)*t + t*s)/(t-s))*x2 by
XCMPLX_1:62
.= (((-s)*(1-t)+t*(1-s))/(t-s))*x1 + 0*n by Th3
.= ((1*(t-s))/(t-s))*x1 by Th1
.= 1*x1 by A3,XCMPLX_1:89
.= x1 by Th3;
then x1 in Line(y1,y2);
hence thesis by A4,Th10;
end;
definition
let n;
let A be Subset of REAL n;
attr A is being_line means :: AFF_1:def 3
ex x1,x2 st x1<>x2 & A=Line(x1,x2);
end;
Lm3: 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)
by Th10,Th11;
theorem :: AFF_1:30
for A,C be Subset of REAL n,x1,x2 holds A is being_line & C is
being_line & x1 in A & x2 in A & x1 in C & x2 in C implies x1=x2 or A=C
proof
let A,C be Subset of REAL n;
let x1,x2;
assume that
A1: A is being_line and
A2: C is being_line and
A3: x1 in A & x2 in A and
A4: x1 in C & x2 in C;
assume
A5: x1<>x2;
then A = Line(x1,x2) by A1,A3,Lm3;
hence thesis by A2,A4,A5,Lm3;
end;
theorem Th13: ::AFF_1:31
for A be Subset of REAL n st A is being_line holds ex x1,x2 st
x1 in A & x2 in A & x1<>x2
proof
let A be Subset of REAL n;
assume A is being_line;
then consider x1,x2 such that
A1: x1<>x2 and
A2: A = Line(x1,x2);
x1 in A & x2 in A by A2,Th9;
hence thesis by A1;
end;
theorem :: AFF_1:32
for A be Subset of REAL n st A is being_line holds ex x2 st x1<>x2 & x2 in A
proof
let A be Subset of REAL n;
assume A is being_line;
then consider y1,y2 such that
A1: y1 in A and
A2: y2 in A & y1<>y2 by Th13;
x1 = y1 implies x1<>y2 & y2 in A by A2;
hence thesis by A1;
end;
theorem :: EUCLID_2:13
for x being Element of REAL n holds |.x.| = sqrt |(x,x)|;
theorem :: EUCLID_2:16
for x being Element of REAL n holds |(x,x)| = 0 iff |.x.| = 0
proof
let x be Element of REAL n;
thus |(x,x)|=0 implies |.x.| = 0;
|.x.| = 0 implies |(x,x)| = 0^2 by EUCLID_2:4;
hence thesis;
end;
theorem Th17: :: EUCLID_2:15
for x being Element of REAL n holds |(x,x)|=0 iff x=0*n
proof
let x be Element of REAL n;
thus |(x,x)| = 0 implies x = 0*n
proof
assume |(x,x)| = 0;
then |.x.| = 0;
hence thesis by EUCLID:8;
end;
thus x = 0*n implies |(x,x)| = 0
proof
assume x = 0*n;
then |(x,x)| = 1/4*((|.(0*n+0*n).|)^2-(|.(0*n-0*n).|)^2) by EUCLID_2:3
.= 1/4*((|.(0*n).|)^2-(|.(0*n-0*n).|)^2) by Th1
.= 1/4*0 by RVSUM_1:32;
hence thesis;
end;
end;
theorem Th18: :: EUCLID_2:17
for x being Element of REAL n holds |(x, 0*n)| = 0
proof
let x be Element of REAL n;
|(x,0*n)| = 1/4*((|.(x+0*n).|)^2-(|.(x-0*n).|)^2) by EUCLID_2:3
.= 1/4*((|.x.|)^2-(|.(x-0*n).|)^2) by Th1
.= 1/4*((|.x.|)^2-(|.x.|)^2) by RVSUM_1:32
.= 1/4*0;
hence thesis;
end;
theorem :: EUCLID_2:18
for x being Element of REAL n holds |(0*n,x)| = 0 by Th18;
theorem Th20: :: EUCLID_2:19
for x1,x2,x3 being Element of REAL n holds |((x1+x2),x3)| = |(x1
,x3)| + |(x2,x3)|
proof
let x1,x2,x3 be Element of REAL n;
A1: len (x3) = n by CARD_1:def 7;
len x1 = n & len x2 = n by CARD_1:def 7;
hence thesis by A1,RVSUM_1:120;
end;
theorem Th21: ::EUCLID_2:20
for x1,x2 being Element of REAL n,a being Real holds |(a*
x1,x2)| = a*|(x1,x2)|
proof
let x1,x2 be Element of REAL n,a be Real;
len x1 = n & len x2 = n by CARD_1:def 7;
hence thesis by RVSUM_1:121;
end;
theorem :: EUCLID_2:21
for x1,x2 being Element of REAL n,a being Real holds |(x1,a*x2
)| = a*|(x1,x2)| by Th21;
theorem Th23: :: EUCLID_2:22
for x1,x2 being Element of REAL n holds |(-x1, x2)| = - |(x1, x2 )|
proof
let x1,x2 be Element of REAL n;
len x1 = n & len x2 = n by CARD_1:def 7;
hence thesis by RVSUM_1:122;
end;
theorem :: EUCLID_2:23
for x1,x2 being Element of REAL n holds |(x1, -x2)| = - |(x1, x2)| by Th23;
theorem :: EUCLID_2:24
for x1,x2 being Element of REAL n holds |(-x1, -x2)| = |(x1, x2)|
proof
let x1,x2 be Element of REAL n;
thus |(-x1, -x2)| = - |(x1, -x2)| by Th23
.= (-1)*|(x1, -x2)|
.= (-1)*(- |(x1, x2)|) by Th23
.= |(x1,x2)|;
end;
theorem Th26: :: EUCLID_2:25
for x1,x2,x3 being Element of REAL n holds |(x1-x2, x3)| = |(x1,
x3)| - |(x2, x3)|
proof
let x1,x2,x3 be Element of REAL n;
A1: len (x3) = n by CARD_1:def 7;
len x1 = n & len x2 = n by CARD_1:def 7;
hence thesis by A1,RVSUM_1:124;
end;
theorem :: EUCLID_2:26
for a,b being Real,x1,x2,x3 being Element of REAL n holds |( (a
*x1+b*x2), x3 )| = a*|(x1,x3)| + b*|(x2,x3)|
proof
let a,b be Real,x1,x2,x3 be Element of REAL n;
thus |( (a*x1+b*x2), x3 )| = |(a*x1,x3)|+|(b*x2,x3)| by Th20
.= a*|(x1,x3)|+|(b*x2,x3)| by Th21
.= a*|(x1,x3)| + b*|(x2,x3)| by Th21;
end;
theorem :: EUCLID_2:27
for x1,y1,y2 being Element of REAL n holds |(x1, y1+y2)| = |(x1, y1)|
+ |(x1, y2)| by Th20;
theorem :: EUCLID_2:28
for x1,y1,y2 being Element of REAL n holds |(x1, y1-y2)| = |(x1, y1)|
- |(x1, y2)| by Th26;
theorem Th30: :: EUCLID_2:29
for x1,x2,y1,y2 being Element of REAL n holds |(x1+x2, y1+y2)| =
|(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|
proof
let x1,x2,y1,y2 being Element of REAL n;
thus |(x1+x2, y1+y2)| = |(x1,y1+y2)|+|(x2,y1+y2)| by Th20
.= |(x1, y1)| + |(x1, y2)| + |(x2, y1+y2)| by Th20
.= |(x1, y1)| + |(x1, y2)| + (|(x2, y1)| + |(x2, y2)|) by Th20
.= |(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|;
end;
theorem Th31: :: EUCLID_2:30
for x1,x2,y1,y2 being Element of REAL n holds |(x1-x2, y1-y2)| =
|(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|
proof
let x1,x2,y1,y2 being Element of REAL n;
thus |(x1-x2, y1-y2)| = |(x1,y1-y2)| - |(x2,y1-y2)| by Th26
.= |(x1,y1)| - |(x1,y2)| - |(x2,y1-y2)| by Th26
.= |(x1,y1)| - |(x1,y2)| - (|(x2,y1)| - |(x2,y2)|) by Th26
.= |(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|;
end;
theorem Th32: :: EUCLID_2:31
for x,y being Element of REAL n holds |(x+y, x+y)| = |(x, x)| +
2*|(x, y)| + |(y, y)|
proof
let x,y be Element of REAL n;
thus |(x+y, x+y)| = |(x,x)|+|(x,y)|+|(y,x)|+|(y,y)| by Th30
.= |(x,x)|+2*|(x,y)|+|(y,y)|;
end;
theorem Th33: :: EUCLID_2:32
for x,y being Element of REAL n holds |(x-y, x-y)| = |(x, x)| -
2*|(x, y)| + |(y, y)|
proof
let x,y be Element of REAL n;
thus |(x-y, x-y)| = |(x,x)| - |(x,y)| - |(y,x)| + |(y,y)| by Th31
.= |(x, x)| - 2*|(x, y)| + |(y, y)|;
end;
theorem :: EUCLID_2:33
for x,y being Element of REAL n holds |.x+y.|^2 = |.x.|^2 + 2*|(x, y)|
+ |.y.|^2
proof
let x,y be Element of REAL n;
thus |.x+y.|^2 = |(x+y,x+y)| by EUCLID_2:4
.= |(x,x)|+2*|(x,y)|+|(y,y)| by Th32
.= |.x.|^2 + 2*|(x, y)| + |(y,y)| by EUCLID_2:4
.= |.x.|^2 + 2*|(x, y)| + |.y.|^2 by EUCLID_2:4;
end;
theorem :: EUCLID_2:34
for x,y being Element of REAL n holds |.x-y.|^2 = |.x.|^2 - 2*|(x, y)|
+ |.y.|^2
proof
let x,y be Element of REAL n;
thus |.x-y.|^2 = |(x-y,x-y)| by EUCLID_2:4
.= |(x,x)|-2*|(x,y)|+|(y,y)| by Th33
.= |.x.|^2 - 2*|(x, y)| + |(y,y)| by EUCLID_2:4
.= |.x.|^2 - 2*|(x, y)| + |.y.|^2 by EUCLID_2:4;
end;
theorem :: EUCLID_2:35
for x,y being Element of REAL n holds |.x+y.|^2 + |.x-y.|^2 = 2*(|.x.|
^2 + |.y.|^2)
proof
let x,y be Element of REAL n;
len x = n & len y = n by CARD_1:def 7;
hence thesis by EUCLID_2:13;
end;
theorem :: EUCLID_2:36
for x,y being Element of REAL n holds |.x+y.|^2 - |.x-y.|^2 = 4* |(x,y )|
proof
let x,y be Element of REAL n;
len x = n & len y = n by CARD_1:def 7;
hence thesis by EUCLID_2:14;
end;
theorem :: EUCLID_2:37 :: Schwartz
for x,y being Element of REAL n holds |.|(x,y)|.| <= |.x.|*|.y.|
proof
let x,y be Element of REAL n;
len x = n & len y = n by CARD_1:def 7;
hence thesis by EUCLID_2:15;
end;
Lm4: -a*x = (-a)*x & -a*x = a*(-x)
proof
reconsider p = x as Point of TOP-REAL n by EUCLID:22;
reconsider x9= p as Element of n-tuples_on REAL;
thus -a*x = ((-1)*a)*x9 by RVSUM_1:49
.= (-a)*x;
hence -a*x = (a*(-1))*x .= a*(-x) by RVSUM_1:49;
end;
Lm5: x1<>x2 implies |.x1-x2.|<>0
proof
now
assume that
A1: x1<>x2 and
A2: not |.x1-x2.| <> 0;
|(x1-x2,x1-x2)| = 0^2 by A2,EUCLID_2:4;
then x1 - x2 = 0*n by Th17;
then x1 = x1 - (x1 + -x2) by RVSUM_1:32
.= x1 - x1 -(-x2) by RVSUM_1:39
.= 0*n -(-x2) by RVSUM_1:37
.= x2 by RVSUM_1:33;
hence contradiction by A1;
end;
hence thesis;
end;
Lm6: for x1, x2 being Element of REAL n holds y1 in Line(x1,x2) & y2 in Line(
x1,x2) implies ex a st y1 - y2 =a*(x1 - x2)
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;
y1 - y2 = (1-t)*x1 + t*x2 - (1-s)*x1 - s*x2 by A1,A2,RVSUM_1:39
.= (1-t)*x1 + -(1-s)*x1 + t*x2 +- s*x2 by Lm2
.= (1-t)*x1 + -(1-s)*x1 + (t*x2 +- s*x2) by FINSEQOP:28
.= (1-t)*x1 + (-(1-s))*x1 + (t*x2 +- s*x2) by Lm4
.= (1-t)*x1 + (-(1-s))*x1 + (t*x2 +(- s)*x2) by Lm4
.= ((1-t)+(-(1-s)))*x1 + (t*x2 +(- s)*x2) by RVSUM_1:50
.= ((1-t)-(1-s))*x1 + (t + (-s))*x2 by RVSUM_1:50
.= (s-t)*x1 + (-(s +- t))*x2
.= (s-t)*x1 + -(s - t)*x2 by Lm4
.= (s-t)*x1 + (s - t)*(-x2) by Lm4
.= (s-t)*(x1 - x2) by RVSUM_1:51;
hence thesis;
end;
Lm7: for x1,x2,y1 being Element of REAL n ex y2 being Element of REAL n st y2
in Line(x1,x2) & x1-x2,y1-y2 are_orthogonal & for x being Element of REAL n st
x in Line(x1,x2) holds |.y1 - y2.| <= |.y1 - x.|
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,Lm5;
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 RVSUM_1:50
.= |(x1-x2,y1-1*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 RVSUM_1:39
.= |(x1-x2,(y1-x1)-((-mu)*x1+ (-(-mu)*x2)))| by Lm4
.= |(x1-x2,(y1-x1)-((-mu)*x1+ (-mu)*(-x2)))| by Lm4
.= |(x1-x2,(y1-x1)-(-mu)*(x1 -x2))| by RVSUM_1:51
.= |(x1-x2,y1-x1)| - |(x1-x2,(-mu)*(x1-x2))| by Th26
.= |(x1-x2,y1-x1)| - (-mu)*|(x1-x2,x1-x2)| by Th21
.= |(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;
end;
case
A3: x1=x2;
let mu be Real;
set y2 = (1-mu)*x1 + mu*x2;
take y2;
x1 - x2 = 0*n by A3,RVSUM_1:37;
then |(x1-x2,y1-y2)| = 0 by Th18;
hence y2 in Line(x1,x2) & x1-x2,y1-y2 are_orthogonal;
end;
end;
then consider y2 such that
A4: y2 in Line(x1,x2) and
A5: x1-x2,y1-y2 are_orthogonal;
A6: |(x1 - x2, y1 - y2)| = 0 by A5;
for x being Element of REAL n st x in Line(x1,x2) holds |.y1 - y2.| <=
|.y1 - x.|
proof
let x be Element of REAL n;
assume x in Line(x1,x2);
then consider a such that
A7: y2 - x =a*(x1 - x2) by A4,Lm6;
(y2 - x) + (y1 - y2) = (-x + y2) +(- y2) + y1 by Lm2
.= (-x + (y2 - y2)) + y1 by FINSEQOP:28
.= (-x + 0*n) + y1 by RVSUM_1:37
.= y1 - x by Th1;
then |.y1-x.|^2 = |(a*(x1 - x2) + (y1 - y2), a*(x1 - x2) + (y1 - y2))| by
A7,EUCLID_2:4
.= |(a*(x1 - x2), a*(x1 - x2))| + 2*|(a*(x1 - x2), y1 - y2)| + |(y1 -
y2, y1 - y2)| by Th32
.= a*|(x1 - x2, a*(x1 - x2))| + 2*|(a*(x1 - x2), y1 - y2)| + |(y1 - y2
, y1 - y2)| by Th21
.= a*(a*|(x1 - x2, x1 - x2)|) + 2*|(a*(x1 - x2), y1 - y2)| + |(y1 - y2
, y1 - y2)| by Th21
.= a^2*|(x1 - x2, x1 - x2)| + 2*|(a*(x1 - x2), y1 - y2)| + |(y1 - y2,
y1 - y2)|
.= a^2*|.x1 - x2.|^2 + 2*|(a*(x1 - x2), y1 - y2)| + |(y1 - y2, y1 - y2
)| by EUCLID_2:4
.= a^2*|.x1 - x2.|^2 + 2*(a*|(x1 - x2, y1 - y2)|) + |(y1 - y2, y1 - y2
)| by Th21
.= (a*|.x1 - x2.|)^2 + |.y1 - y2.|^2 by A6,EUCLID_2:4;
then 0 <= |.y1-x.|^2 - |.y1 - y2.|^2 by XREAL_1:63;
then
A8: |.y1 - y2.|^2 <= |.y1 - x.|^2 by XREAL_1:49;
0 <= |.y1 - y2.|^2 by XREAL_1:63;
then sqrt |.y1 - y2.|^2 <= sqrt |.y1 - x.|^2 by A8,SQUARE_1:26;
then |.y1 - y2.| <= sqrt |.y1 - x.|^2 by EUCLID:9,SQUARE_1:22;
hence thesis by EUCLID:9,SQUARE_1:22;
end;
hence thesis by A4,A5;
end;
::$CT
theorem
for R being Subset of REAL,x1,x2,y1 being Element of REAL n st
R={|.y1-x.| where x is Element of REAL n: x in Line(x1,x2)}
ex y2 being Element of REAL n
st y2 in Line(x1,x2) & |.y1-y2.|=lower_bound R & x1-x2,y1-y2 are_orthogonal
proof
let R being Subset of REAL,x1,x2,y1 being Element of REAL n;
consider y2 being Element of REAL n such that
A1: y2 in Line(x1,x2) and
A2: x1-x2,y1-y2 are_orthogonal and
A3: for x being Element of REAL n st x in Line(x1,x2) holds |.y1 - y2.|
<= |.y1 - x.| by Lm7;
assume
A4: R={|.y1-x.| where x is Element of REAL n: x in Line(x1,x2)};
A5: for s being Real st 0<s holds ex r being Real st r in R &
r < |.y1-y2.|+s
proof
let s be Real;
assume
A6: 0<s;
take |.y1- y2.|;
thus thesis by A4,A1,A6,XREAL_1:29;
end;
x1 in Line(x1,x2) by Th9;
then
A7: |.y1-x1.| in R by A4;
A8: for r being Real st r in R holds |.y1-y2.| <=r
proof
let r be Real;
assume r in R;
then ex x0 being Element of REAL n st r= |.y1-x0.| & x0 in Line(x1,x2) by
A4;
hence thesis by A3;
end;
R is bounded_below proof take |.y1-y2.|;
let r be ExtReal;
assume r in R;
then ex x0 being Element of REAL n st r= |.y1-x0.| & x0 in Line(x1,x2) by
A4;
hence thesis by A3;
end;
then |.y1-y2.| = lower_bound R by A7,A5,A8,SEQ_4:def 2;
hence thesis by A1,A2;
end;
definition
::$CD
end;
reserve p1,p2,q1,q2 for Point of TOP-REAL n;
Lm8: for p1,p2 being Point of TOP-REAL n ex x1,x2 being Element of REAL n st
p1=x1 & p2=x2 & Line(x1,x2)=Line(p1,p2)
proof
let p1,p2 be Point of TOP-REAL n;
reconsider x1=p1,x2=p2 as Element of REAL n by EUCLID:22;
take x1,x2;
thus p1=x1 & p2=x2;
thus Line(x1,x2) c= Line(p1,p2)
proof
let e be object;
assume e in Line(x1,x2);
then consider lambda such that
A1: e = (1-lambda)*x1 + lambda*x2;
e = (1-lambda)*p1 + lambda*p2 by A1;
hence e in Line(p1,p2);
end;
let e be object;
assume e in Line(p1,p2);
then consider lambda such that
A2: e = (1-lambda)*p1 + lambda*p2;
e = (1-lambda)*x1 + lambda*x2 by A2;
hence e in Line(x1,x2);
end;
theorem :::Th40: :: AFF_1:26
p1 in Line(p1,p2) & p2 in Line(p1,p2) by RLTOPSP1:72;
theorem :::Th41: :: AFF_1:27
q1 in Line(p1,p2) & q2 in Line(p1,p2) implies Line(q1,q2) c= Line(p1,p2)
by RLTOPSP1:74;
theorem :::Th42: :: AFF_1:28
q1 in Line(p1,p2) & q2 in Line(p1,p2) & q1<>q2 implies Line(p1,
p2) c= Line(q1,q2) by RLTOPSP1:75;
definition
let n;
let A be Subset of TOP-REAL n;
attr A is being_line means :: AFF_1:def 3
ex p1,p2 st p1<>p2 & A=Line(p1,p2);
end;
Lm9: for A be Subset of TOP-REAL n,p1,p2 holds A is being_line & p1 in A & p2
in A & p1<>p2 implies A=Line(p1,p2)
by RLTOPSP1:75;
theorem :: AFF_1:30
for A,C being Subset of TOP-REAL n holds A is being_line & C is
being_line & p1 in A & p2 in A & p1 in C & p2 in C implies p1=p2 or A=C
proof
let A,C be Subset of TOP-REAL n;
assume that
A1: A is being_line and
A2: C is being_line and
A3: p1 in A & p2 in A and
A4: p1 in C & p2 in C;
assume
A5: p1<>p2;
then A = Line(p1,p2) by A1,A3,Lm9;
hence thesis by A2,A4,A5,Lm9;
end;
theorem Th44: :: AFF_1:31
for A being Subset of TOP-REAL n st A is being_line holds ex p1,
p2 st p1 in A & p2 in A & p1<>p2
proof
let A be Subset of TOP-REAL n;
assume A is being_line;
then consider p1,p2 such that
A1: p1<>p2 and
A2: A = Line(p1,p2);
p1 in A & p2 in A by A2,RLTOPSP1:72;
hence thesis by A1;
end;
theorem :: AFF_1:32
for A being Subset of TOP-REAL n st A is being_line holds ex p2 st p1
<>p2 & p2 in A
proof
let A be Subset of TOP-REAL n;
assume A is being_line;
then consider q1,q2 such that
A1: q1 in A and
A2: q2 in A & q1<>q2 by Th44;
p1 = q1 implies p1<>q2 & q2 in A by A2;
hence thesis by A1;
end;
theorem
for R being Subset of REAL,p1,p2,q1 being Point of TOP-REAL n st R={|.
q1-p .| where p is Point of TOP-REAL n: p in Line(p1,p2)}
ex q2 being
Point of TOP-REAL n st q2 in Line(p1,p2) & |. q1-q2 .| =lower_bound R & p1-p2,
q1-q2 are_orthogonal
proof
let R being Subset of REAL,p1,p2,q1 being Point of TOP-REAL n;
reconsider y1 = q1 as Element of REAL n by EUCLID:22;
consider x1,x2 being Element of REAL n such that
A1: p1=x1 & p2=x2 and
A2: Line(x1,x2)=Line(p1,p2) by Lm8;
A3: x1-x2 = p1-p2 by A1;
consider y2 being Element of REAL n such that
A4: y2 in Line(x1,x2) and
A5: x1-x2,y1-y2 are_orthogonal and
A6: for x being Element of REAL n st x in Line(x1,x2) holds |.y1 - y2.|
<= |.y1 - x.| by Lm7;
reconsider q2 = y2 as Point of TOP-REAL n by EUCLID:22;
assume
A7: R={|. q1-p .| where p is Point of TOP-REAL n: p in Line(p1,p2)};
A8: for s being Real st 0<s holds ex r being Real st r in R &
r < |.q1-q2.|+s
proof
let s be Real;
assume
A9: 0<s;
take |.q1- q2.|;
thus thesis by A7,A2,A4,A9,XREAL_1:29;
end;
p1 in Line(p1,p2) by RLTOPSP1:72;
then
A10: |.q1-p1.| in R by A7;
A11: for r being Real st r in R holds |.q1-q2.| <=r
proof
let r be Real;
assume r in R;
then consider p0 being Point of TOP-REAL n such that
A12: r= |.q1-p0.| & p0 in Line(p1,p2) by A7;
the carrier of Euclid n = the carrier of TOP-REAL n by EUCLID:67;
then reconsider x = p0 as Element of REAL n;
thus |.q1-q2.| <=r by A2,A6,A12;
end;
R is bounded_below
proof
take |.q1-q2.|;
let r be ExtReal;
assume r in R;
then consider p0 being Point of TOP-REAL n such that
A13: r= |.q1-p0.| & p0 in Line(p1,p2) by A7;
the carrier of Euclid n = the carrier of TOP-REAL n by EUCLID:67;
then reconsider x = p0 as Element of REAL n;
thus |.q1-q2.| <=r by A2,A6,A13;
end;
then y1-y2 = q1-q2 & |.q1-q2.| = lower_bound R by A10,A8,A11,SEQ_4:def 2;
hence thesis by A2,A4,A5,A3;
end;