:: Angle and Triangle in {E}uclidian Topological Space
:: by Akihiro Kubo and Yatsuka Nakamura
::
:: Received May 29, 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 NUMBERS, XCMPLX_0, REAL_1, PRE_TOPC, EUCLID, COMPLEX1, RELAT_1,
SUBSET_1, MCART_1, ARYTM_3, ARYTM_1, SUPINF_2, CARD_1, SQUARE_1,
FINSEQ_1, FUNCT_1, RVSUM_1, CARD_3, ORDINAL4, COMPTRIG, SIN_COS,
XXREAL_0, XXREAL_1, COMPLEX2, PROB_2, RLTOPSP1, XBOOLE_0, TARSKI,
STRUCT_0, TOPMETR, EUCLID_3;
notations TARSKI, XBOOLE_0, SUBSET_1, SQUARE_1, RELAT_1, SIN_COS, FUNCT_1,
FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0,
REAL_1, FINSEQ_1, RVSUM_1, STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID,
COMPTRIG, COMPLEX2, RLVECT_1, TOPMETR, RCOMP_1;
constructors REAL_1, SQUARE_1, BINOP_2, RCOMP_1, SIN_COS, COMPTRIG, COMPLEX2,
MONOID_0, TOPMETR, TOPREAL1, COMPLEX1;
registrations RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, STRUCT_0, MONOID_0,
EUCLID, TOPMETR, VALUED_0, XREAL_0, ORDINAL1, SIN_COS, SQUARE_1;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
definitions XBOOLE_0, TARSKI;
equalities XBOOLE_0, EUCLID, COMPLEX1, ALGSTR_0, RLTOPSP1;
expansions XBOOLE_0, COMPLEX1;
theorems XCMPLX_1, SQUARE_1, FUNCT_1, TOPREAL3, COMPLEX1, XBOOLE_0, FUNCT_2,
RVSUM_1, FINSEQ_1, EUCLID, JGRAPH_3, COMPLEX2, XREAL_0, EUCLID_2,
XCMPLX_0, TOPMETR, XREAL_1, COMPTRIG, VALUED_1, RLTOPSP1, RLVECT_1,
RLVECT_4;
schemes DOMAIN_1, FUNCT_2;
begin
reserve z,z1,z2 for Complex;
reserve r,x1,x2 for Real;
reserve p0,p,p1,p2,p3,q for Point of TOP-REAL 2;
definition
let z be Complex;
func cpx2euc(z) -> Point of TOP-REAL 2 equals
|[Re z,Im z]|;
correctness;
end;
definition
let p be Point of TOP-REAL 2;
func euc2cpx(p) -> Element of COMPLEX equals
p`1 +p`2 *<i>;
correctness by XCMPLX_0:def 2;
end;
theorem Th1:
euc2cpx(cpx2euc(z))=z
proof
(|[Re z,Im z]|)`1=Re z & (|[Re z,Im z]|)`2=Im z by EUCLID:52;
hence thesis by COMPLEX1:13;
end;
theorem Th2:
cpx2euc(euc2cpx(p))=p
proof
Re (p`1+p`2*<i>) = p`1 & Im(p`1+p`2*<i>) = p`2 by COMPLEX1:12;
hence thesis by EUCLID:53;
end;
theorem
for z1,z2 st cpx2euc(z1)=cpx2euc(z2) holds z1=z2
proof
let z1,z2;
assume
A1: cpx2euc(z1)=cpx2euc(z2);
z2 = euc2cpx(cpx2euc(z2)) by Th1;
hence thesis by A1,Th1;
end;
theorem Th4:
for p1,p2 st euc2cpx(p1)=euc2cpx(p2) holds p1=p2
proof
let p1,p2;
assume
A1: euc2cpx(p1)=euc2cpx(p2);
p2 = cpx2euc(euc2cpx(p2)) by Th2;
hence thesis by A1,Th2;
end;
theorem Th5:
cpx2euc(x1+x2*<i>)= |[x1,x2]|
proof
Re (x1+x2*<i>)=x1 by COMPLEX1:12;
hence thesis by COMPLEX1:12;
end;
theorem Th6:
|[Re (z1+z2),Im (z1+z2)]|=|[Re z1 + Re z2, Im z1 + Im z2]|
proof
(|[Re (z1+z2),Im (z1+z2)]|)`2=Im (z1 + z2) by EUCLID:52;
then
A1: (|[Re (z1+z2),Im (z1+z2)]|)`2=Im z1 + Im z2 by COMPLEX1:8;
(|[Re (z1+z2),Im (z1+z2)]|)`1=Re (z1+z2) by EUCLID:52;
then (|[Re (z1+z2),Im (z1+z2)]|)`1=Re z1+Re z2 by COMPLEX1:8;
hence thesis by A1,EUCLID:53;
end;
theorem Th7:
cpx2euc(z1+z2)=cpx2euc(z1)+cpx2euc(z2)
proof
cpx2euc(z1)+cpx2euc(z2) =|[Re z1 + Re z2, Im z1 + Im z2]| by EUCLID:56;
hence thesis by Th6;
end;
theorem Th8:
(p1+p2)`1+(p1+p2)`2*<i> = p1`1+p2`1+(p1`2+p2`2)*<i>
proof
A1: (p1+p2)=|[p1`1+p2`1 , p1`2+p2`2]| by EUCLID:55;
A2: Im (p1`1+p2`1+(p1`2+p2`2)*<i>)=p1`2+p2`2 by COMPLEX1:12;
A3: Im((p1+p2)`1+(p1+p2)`2*<i>)=(p1+p2)`2 & Re (p1`1+p2`1+(p1`2+p2`2)*<i>)=
p1`1+ p2`1 by COMPLEX1:12;
Re((p1+p2)`1+(p1+p2)`2*<i>)=(p1+p2)`1 by COMPLEX1:12;
then Re((p1+p2)`1+(p1+p2)`2*<i>)=p1`1+p2`1 by A1,EUCLID:52;
hence thesis by A1,A3,A2,EUCLID:52;
end;
theorem Th9:
euc2cpx(p1+p2)=euc2cpx(p1)+euc2cpx(p2)
proof
euc2cpx(p1+p2)= p1`1+p2`1+(p1`2+p2`2)*<i> by Th8;
hence thesis;
end;
theorem Th10:
|[Re (-z),Im (-z)]|=|[-(Re z), -(Im z)]|
proof
(|[Re (-z),Im (-z)]|)`2=Im (-z) by EUCLID:52;
then
A1: (|[Re (-z),Im (-z)]|)`2=-(Im z) by COMPLEX1:17;
(|[Re (-z),Im (-z)]|)`1=Re (-z) by EUCLID:52;
then (|[Re (-z),Im (-z)]|)`1=-(Re z) by COMPLEX1:17;
hence thesis by A1,EUCLID:53;
end;
theorem Th11:
cpx2euc(-z)= -cpx2euc(z)
proof
-cpx2euc(z) =|[-(Re z), -(Im z)]| by EUCLID:60;
hence thesis by Th10;
end;
theorem Th12:
(-p)`1+(-p)`2*<i>= -(p`1)+(-(p`2))*<i>
proof
A1: -p=|[-p`1, -p`2]| by EUCLID:59;
-(p`1)+(-(p`2))*<i> = -(p`1)+(-(p`2))*<i>;
then
A2: Re(-(p`1)+-(p`2)*<i>)=-(p`1) & Im(-(p`1)+-(p`2)*<i>)=-(p`2) by COMPLEX1:12;
Re((-p)`1+(-p)`2*<i>)=(-p)`1 by COMPLEX1:12;
then Im((-p)`1+(-p)`2*<i>)=(-p)`2 & Re((-p)`1+(-p)`2*<i>)=-(p`1) by A1,
COMPLEX1:12,EUCLID:52;
hence thesis by A1,A2,EUCLID:52;
end;
theorem Th13:
euc2cpx(-p)= -euc2cpx(p)
proof
-euc2cpx(p) = -(p`1)+(-(p`2))*<i>;
hence thesis by Th12;
end;
theorem
cpx2euc(z1-z2)=cpx2euc(z1)-cpx2euc(z2)
proof
thus cpx2euc(z1-z2)=cpx2euc(z1+-z2) .=cpx2euc(z1)+cpx2euc(-z2) by Th7
.=cpx2euc(z1)-cpx2euc(z2) by Th11;
end;
theorem Th15:
euc2cpx(p1-p2)=euc2cpx(p1)-euc2cpx(p2)
proof
thus euc2cpx(p1-p2)=euc2cpx(p1)+euc2cpx(-p2) by Th9
.=euc2cpx(p1)+-euc2cpx(p2) by Th13
.=euc2cpx(p1)-euc2cpx(p2);
end;
theorem Th16:
cpx2euc(0c)= 0.TOP-REAL 2 by COMPLEX1:4,EUCLID:54;
theorem Th17:
euc2cpx(0.TOP-REAL 2)=0c by Th1,Th16;
theorem
euc2cpx(p)=0c implies p=0.TOP-REAL 2 by Th2,Th16;
theorem
cpx2euc(r*z)=r*(cpx2euc(z))
proof
A1: (cpx2euc(z))`1=Re z & (cpx2euc(z))`2=Im z by EUCLID:52;
r = r+0 *<i>;
then
A2: Re r = r & Im r = 0 by COMPLEX1:12;
then
A3: Im (r*z) = r * Im z + 0 * Re z by COMPLEX1:9
.= r * Im z;
Re (r*z) = r * Re z - 0 * Im z by A2,COMPLEX1:9
.= r * Re z;
hence thesis by A3,A1,EUCLID:57;
end;
theorem
euc2cpx(r*p)= r*euc2cpx(p)
proof
r*p = |[r*p`1,r*p`2]| by EUCLID:57;
then (r*p)`1=r*p`1 & (r*p)`2=r*p`2 by EUCLID:52;
hence thesis;
end;
theorem Th21:
|.euc2cpx(p).|=sqrt ((p`1)^2+(p`2)^2)
proof
Re euc2cpx(p)=p`1 by COMPLEX1:12;
hence thesis by COMPLEX1:12;
end;
theorem
for f being FinSequence of REAL st len f=2 holds |.f.| = sqrt ((f.1)^2
+(f.2)^2)
proof
let f being FinSequence of REAL;
A1: (sqr f).1=(f.1)^2 & (sqr f).2=(f.2)^2 by VALUED_1:11;
dom (sqr f)= dom f & Seg len (sqr f) = dom (sqr f) by FINSEQ_1:def 3
,VALUED_1:11;
then
A2: len (sqr f) = len f by FINSEQ_1:def 3;
reconsider f1 = (f.1)^2, f2 = (f.2)^2 as Element of REAL by XREAL_0:def 1;
assume len f=2;
then sqr f = <* (f.1)^2,(f.2)^2 *> by A1,A2,FINSEQ_1:44;
then Sum sqr f = Sum (<* f1 *>^<* f2*>) by FINSEQ_1:def 9
.=Sum <*f1*> + (f.2)^2 by RVSUM_1:74
.= (f.1)^2 + (f.2)^2 by RVSUM_1:73;
hence thesis;
end;
theorem
for f being FinSequence of REAL, p being Point of TOP-REAL 2 st len f
= 2 & p = f holds |.p.|=|.f.|;
theorem
|.cpx2euc(z).|=sqrt ((Re z)^2 + (Im z)^2)
proof
(|[ Re z,Im z ]|)`1=Re z & (|[ Re z,Im z ]|)`2=Im z by EUCLID:52;
hence thesis by JGRAPH_3:1;
end;
theorem Th25:
|.euc2cpx(p).|=|.p.|
proof
|.p.| = sqrt ((p`1)^2+(p`2)^2) by JGRAPH_3:1;
hence thesis by Th21;
end;
definition
let p;
func Arg(p) -> Real equals
Arg(euc2cpx(p));
correctness;
end;
theorem
for z being Element of COMPLEX, p st z=euc2cpx(p) or p=cpx2euc(z)
holds Arg(z)=Arg(p)
proof
let z be Element of COMPLEX, p;
assume
A1: z=euc2cpx(p) or p=cpx2euc(z);
per cases by A1;
suppose
z=euc2cpx(p);
hence thesis;
end;
suppose
p=cpx2euc(z);
hence thesis by Th1;
end;
end;
theorem
for x1,x2 being Real,p st x1= |.p.|*cos (Arg p) & x2=|.p.|*sin (Arg p)
holds p = |[ x1,x2 ]|
proof
let x1,x2 be Real,p;
assume x1= (|.p.|)*cos (Arg(p)) & x2=(|.p.|)*sin (Arg(p));
then x1= (|.euc2cpx(p).|)*cos (Arg(euc2cpx(p))) & x2=(|.euc2cpx(p).|)*sin (
Arg( euc2cpx(p))) by Th25;
then euc2cpx(p)= x1 +x2 *<i> by COMPTRIG:62;
then p=cpx2euc(x1 +x2 *<i>) by Th2;
hence thesis by Th5;
end;
theorem
Arg(0.TOP-REAL 2)=0 by Th17,COMPTRIG:35;
theorem
for p st p<>0.TOP-REAL 2 holds (Arg(p)<PI implies Arg(-p)=Arg(p)+PI)&
(Arg(p)>=PI implies Arg(-p)=Arg(p)-PI)
proof
let p;
assume p<>0.TOP-REAL 2;
then
A1: euc2cpx(p)<>0c by Th2,Th16;
Arg(-p)=Arg(-euc2cpx(p)) by Th13;
hence thesis by A1,COMPLEX2:13;
end;
theorem
for p st Arg p=0 holds p=|[ |.p.|,0 ]| & p`2=0
proof
let p;
assume Arg p=0;
then
A1: euc2cpx(p)=|.euc2cpx(p).|+0 *<i> & Im euc2cpx(p) =0 by COMPLEX2:15,21;
cpx2euc(|.euc2cpx(p).|+0 *<i>)=|[|.euc2cpx(p).|,0 ]| & |.euc2cpx(p).|=|.
p.| by Th5,Th25;
hence thesis by A1,Th2,COMPLEX1:12;
end;
theorem Th31:
for p st p<>0.TOP-REAL 2 holds (Arg(p)<PI iff Arg(-p)>=PI)
proof
let p;
assume p<>0.TOP-REAL 2;
then
A1: euc2cpx(p)<>0c by Th2,Th16;
Arg(-p)=Arg(-euc2cpx(p)) by Th13;
hence thesis by A1,COMPLEX2:16;
end;
theorem
for p1,p2 st p1<>p2 or p1-p2<>0.TOP-REAL 2 holds (Arg(p1-p2)<PI iff
Arg(p2-p1)>=PI)
proof
let p1,p2;
assume p1<>p2 or p1-p2<>0.TOP-REAL 2;
then
A1: p1-p2<>0.TOP-REAL 2 by RLVECT_1:21;
-(p1-p2)=p2-p1 by RLVECT_1:33;
hence thesis by A1,Th31;
end;
theorem
for p holds Arg p in ].0,PI.[ iff p`2 > 0
proof
let p;
Im euc2cpx(p)=p`2 by COMPLEX1:12;
hence thesis by COMPLEX2:18;
end;
theorem
for p1,p2 st Arg(p1)<PI & Arg(p2)<PI holds Arg(p1+p2)<PI
proof
let p1,p2;
assume Arg(p1)<PI & Arg(p2)<PI;
then Arg(euc2cpx(p1)+euc2cpx(p2))<PI by COMPLEX2:20;
hence thesis by Th9;
end;
definition
let p1,p2,p3;
func angle(p1,p2,p3) -> Real equals
angle(euc2cpx(p1),euc2cpx(p2),euc2cpx(p3));
correctness;
end;
theorem
for p1,p2,p3 holds angle(p1,p2,p3)=angle(p1-p2,0.TOP-REAL 2,p3-p2)
proof
let p1,p2,p3;
euc2cpx(p1)-euc2cpx(p2)=euc2cpx(p1-p2) & euc2cpx(p3)-euc2cpx(p2)=euc2cpx
(p3- p2) by Th15;
hence thesis by Th17,COMPLEX2:71;
end;
theorem
for p1,p2,p3 st angle(p1,p2,p3) =0 holds Arg(p1-p2)=Arg(p3-p2) & angle
(p3,p2,p1)=0
proof
let p1,p2,p3;
assume
A1: angle(p1,p2,p3) =0;
euc2cpx(p1)-euc2cpx(p2)=euc2cpx(p1-p2) & euc2cpx(p3)-euc2cpx(p2)=euc2cpx
(p3- p2) by Th15;
hence thesis by A1,COMPLEX2:74;
end;
theorem
for p1,p2,p3 st angle(p1,p2,p3) <>0 holds angle(p3,p2,p1)=2*PI-angle(
p1,p2,p3)
proof
let p1,p2,p3;
assume angle(p1,p2,p3) <>0;
then angle(p3,p2,p1)+angle(p1,p2,p3) = 2*PI by COMPLEX2:80;
hence thesis;
end;
theorem
for p1,p2,p3 st angle(p3,p2,p1) <>0 holds angle(p3,p2,p1)=2*PI-angle(
p1,p2,p3)
proof
let p1,p2,p3;
assume angle(p3,p2,p1) <>0;
then angle(p3,p2,p1)+angle(p1,p2,p3) = 2*PI by COMPLEX2:80;
hence thesis;
end;
theorem Th39:
for x,y being Element of COMPLEX holds Re (x .|. y) = (Re x)*(Re
y)+(Im x)*(Im y)
proof
let x,y be Element of COMPLEX;
x .|. y =(Re x)*(Re y)+(Im x)*(Im y)+(-((Re x)*(Im y))+(Im x)*(Re y))*
<i> by COMPLEX2:29;
hence thesis by COMPLEX1:12;
end;
theorem Th40:
for x,y being Element of COMPLEX holds Im (x .|. y) = -((Re x)*(
Im y))+(Im x)*(Re y)
proof
let x,y be Element of COMPLEX;
x .|. y = (Re x)*(Re y)+(Im x)*(Im y)+(-((Re x)*(Im y))+(Im x)*(Re y))*
<i> by COMPLEX2:29;
hence thesis by COMPLEX1:12;
end;
theorem Th41:
for p,q holds |(p,q)| = p`1*q`1+p`2*q`2
proof
let p,q;
(p+q)`1=p`1+q`1 by TOPREAL3:2;
then
A1: ((p+q)`1)^2=(p`1)^2+2*p`1*q`1+(q`1)^2 by SQUARE_1:4;
(p+q)`2=p`2+q`2 by TOPREAL3:2;
then
A2: ((p+q)`2)^2=(p`2)^2+2*p`2*q`2+(q`2)^2 by SQUARE_1:4;
(p-q)`2=p`2-q`2 by TOPREAL3:3;
then
A3: ((p-q)`2)^2=(p`2)^2-2*p`2*q`2+(q`2)^2 by SQUARE_1:5;
(p-q)`1=p`1-q`1 by TOPREAL3:3;
then
A4: ((p-q)`1)^2=(p`1)^2-2*p`1*q`1+(q`1)^2 by SQUARE_1:5;
|(p,q)|= (1/4)*(|.p+q.|^2 - |.p-q.|^2) by EUCLID_2:49
.= (1/4)*( ((p+q)`1)^2+((p+q)`2)^2 - |.p-q.|^2) by JGRAPH_3:1
.= (1/4)*( ((p+q)`1)^2+((p+q)`2)^2 - (((p-q)`1)^2+((p-q)`2)^2)) by
JGRAPH_3:1
.= (1/4)*( ((p+q)`1)^2 - ((p-q)`1)^2+(((p+q)`2)^2-((p-q)`2)^2));
hence thesis by A1,A2,A4,A3;
end;
theorem Th42:
for p1,p2 holds |(p1,p2)| = Re ((euc2cpx(p1)) .|. (euc2cpx(p2)))
proof
let p1,p2;
A1: p1`1=Re euc2cpx(p1) & p1`2= Im euc2cpx(p1) by COMPLEX1:12;
A2: p2`1=Re euc2cpx(p2) & p2`2= Im euc2cpx(p2) by COMPLEX1:12;
thus |(p1,p2)| = p1`1*p2`1+p1`2*p2`2 by Th41
.= Re ((euc2cpx(p1)) .|. (euc2cpx(p2))) by A1,A2,Th39;
end;
theorem
for p1,p2,p3 st p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2 holds ( |(p1,p2)|=
0 iff angle(p1,0.TOP-REAL 2,p2)=PI/2 or angle(p1,0.TOP-REAL 2,p2)=3/2*PI)
proof
let p1,p2,p3;
assume p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2;
then
A1: euc2cpx(p1)<> 0c & euc2cpx(p2)<> 0c by Th2,Th16;
|(p1,p2)| = Re ((euc2cpx(p1)) .|. (euc2cpx(p2))) by Th42;
hence thesis by A1,Th17,COMPLEX2:75;
end;
theorem
for p1,p2 st p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2 holds ( -(p1`1*p2`2)+
p1`2*p2`1= |.p1.|*|.p2.| or -(p1`1*p2`2)+p1`2*p2`1= -(|.p1.|*|.p2.|) iff angle(
p1,0.TOP-REAL 2,p2)=PI/2 or angle(p1,0.TOP-REAL 2,p2)=3/2*PI)
proof
let p1,p2;
A1: p2`1=Re euc2cpx(p2) & p2`2= Im euc2cpx(p2) by COMPLEX1:12;
p1`1=Re euc2cpx(p1) & p1`2= Im euc2cpx(p1) by COMPLEX1:12;
then
A2: Im ((euc2cpx(p1)) .|. (euc2cpx(p2))) = -(p1`1*p2`2)+p1`2*p2`1 by A1,Th40;
assume p1<>0.TOP-REAL 2 & p2<>0.TOP-REAL 2;
then
A3: euc2cpx(p1)<> 0c & euc2cpx(p2)<> 0c by Th2,Th16;
|.euc2cpx(p1).|=|.p1.| & |.euc2cpx(p2).|=|.p2.| by Th25;
hence thesis by A3,A2,Th17,COMPLEX2:76;
end;
theorem
for p1,p2,p3 st p1<>p2 & p3<>p2 holds ( |( p1-p2,p3-p2 )| = 0 iff
angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI)
proof
let p1,p2,p3;
assume that
A1: p1<>p2 and
A2: p3<>p2;
p1 - p2 <> 0.TOP-REAL 2 by A1,RLVECT_1:21;
then
A3: euc2cpx(p1-p2) <> 0c by Th2,Th16;
p3 - p2 <> 0.TOP-REAL 2 by A2,RLVECT_1:21;
then
A4: euc2cpx(p3-p2) <> 0c by Th2,Th16;
A5: euc2cpx(p1)-euc2cpx(p2)=euc2cpx(p1-p2) & euc2cpx(p3)-euc2cpx(p2)=euc2cpx
(p3- p2) by Th15;
hereby
assume |(p1-p2,p3-p2)| = 0;
then Re ((euc2cpx(p1-p2)) .|. (euc2cpx(p3-p2))) = 0 by Th42;
then
angle(euc2cpx(p1-p2),0c,euc2cpx(p3-p2))=PI/2 or angle(euc2cpx(p1-p2),
0c,euc2cpx(p3-p2))=3/2*PI by A3,A4,COMPLEX2:75;
hence angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI by A5,COMPLEX2:71;
end;
A6: |( p1-p2,p3-p2 )| = Re ((euc2cpx(p1-p2)) .|. (euc2cpx(p3-p2))) by Th42;
assume angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI;
then
angle(euc2cpx(p1-p2),0c,euc2cpx(p3-p2))=PI/2 or angle(euc2cpx(p1-p2),0c
,euc2cpx(p3-p2))=3/2*PI by A5,COMPLEX2:71;
hence thesis by A6,A3,A4,COMPLEX2:75;
end;
::$N Pythagorean Theorem
::$L https://en.wikipedia.org/wiki/Pythagorean_theorem Pythagorean Theorem
theorem
for p1,p2,p3 st p1<>p2 & p3<>p2 & (angle(p1,p2,p3)=PI/2 or angle(p1,p2
,p3)=3/2*PI) holds |.p1-p2.|^2+|.p3-p2.|^2=|.p1-p3.|^2
proof
let p1,p2,p3;
assume that
A1: p1<>p2 & p3<>p2 and
A2: angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI;
A3: euc2cpx(p1)-euc2cpx(p2)=euc2cpx(p1-p2) & euc2cpx(p3)-euc2cpx(p2)=euc2cpx
(p3- p2) by Th15;
A4: euc2cpx(p1)-euc2cpx(p3)=euc2cpx(p1-p3) & |.euc2cpx(p1-p2).|=|.p1-p2.| by
Th15,Th25;
A5: |.euc2cpx(p3-p2).|=|.p3-p2.| & |.euc2cpx(p1-p3).|=|.p1-p3.| by Th25;
euc2cpx(p1)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p2) by A1,Th4;
hence thesis by A2,A3,A4,A5,COMPLEX2:77;
end;
theorem :: Sum of inner angles of triangle
for p1,p2,p3 st p2<>p1 & p1<>p3 & p3<>p2 & angle(p2,p1,p3)<PI holds
angle(p2,p1,p3)+angle(p1,p3,p2)+angle(p3,p2,p1)=PI
proof
let p1,p2,p3;
assume that
A1: p2<>p1 & p1<>p3 and
A2: p3<>p2 and
A3: angle(p2,p1,p3)<PI;
A4: euc2cpx(p1)<> euc2cpx(p2) & euc2cpx(p1)<> euc2cpx(p3) by A1,Th4;
A5: euc2cpx(p3)<> euc2cpx(p2) by A2,Th4;
per cases by COMPLEX2:70;
suppose
A6: 0 = angle(euc2cpx(p2),euc2cpx(p1),euc2cpx(p3));
now
per cases by A4,A5,A6,COMPLEX2:87;
suppose
angle(euc2cpx(p1),euc2cpx(p3),euc2cpx(p2)) = 0 & angle(euc2cpx
(p3),euc2cpx(p2),euc2cpx(p1)) = PI;
hence thesis by A6;
end;
suppose
angle(euc2cpx(p1),euc2cpx(p3),euc2cpx(p2)) = PI & angle(
euc2cpx(p3),euc2cpx(p2),euc2cpx(p1)) = 0;
hence thesis by A6;
end;
end;
hence thesis;
end;
suppose
0 < angle(euc2cpx(p2),euc2cpx(p1),euc2cpx(p3));
hence thesis by A3,A4,COMPLEX2:84;
end;
end;
definition
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
func Triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
LSeg(p1,p2) \/ LSeg(p2,p3) \/ LSeg(p3,p1);
correctness;
end;
definition
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
func closed_inside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
{p where p is Point of TOP-REAL n:
ex a1,a2,a3 being Real st 0<=a1 & 0<=a2 & 0<=a3
& a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3};
correctness
proof
defpred P[set] means
ex a1,a2,a3 being Real st 0<=a1 & 0<=a2 & 0<=a3 & a1+
a2+a3=1 & $1=a1*p1+a2*p2+a3*p3;
{p where p is Element of TOP-REAL n: P[p]} is Subset of TOP-REAL n
from DOMAIN_1:sch 7;
hence thesis;
end;
end;
definition
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
func inside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
closed_inside_of_triangle(p1,p2,p3) \ Triangle(p1,p2,p3);
correctness;
end;
definition
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
func outside_of_triangle(p1,p2,p3) -> Subset of TOP-REAL n equals
{p where p
is Point of TOP-REAL n:
ex a1,a2,a3 being Real st (0>a1 or 0>a2 or 0>a3) & a1+
a2+a3=1 & p=a1*p1+a2*p2+a3*p3};
correctness
proof
defpred P[set] means
ex a1,a2,a3 being Real st (0>a1 or 0>a2 or 0>a3) & a1
+a2+a3=1 & $1=a1*p1+a2*p2+a3*p3;
{p where p is Point of TOP-REAL n: P[p]} is Subset of TOP-REAL n from
DOMAIN_1:sch 7;
hence thesis;
end;
end;
definition
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
func plane(p1,p2,p3) -> Subset of TOP-REAL n equals
outside_of_triangle(p1,
p2,p3) \/ closed_inside_of_triangle(p1,p2,p3);
correctness;
end;
theorem Th48:
for n being Element of NAT,p1,p2,p3,p being Point of TOP-REAL n
st p in plane(p1,p2,p3)
ex a1,a2,a3 being Real st a1+a2+a3=1 & p=a1*p1+a2
*p2+a3*p3
proof
let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
assume
A1: p in plane(p1,p2,p3);
now
per cases by A1,XBOOLE_0:def 3;
case
p in outside_of_triangle(p1,p2,p3);
then
ex p4 being Point of TOP-REAL n st p4=p &
ex a1,a2,a3 being Real st (
0>a1 or 0>a2 or 0>a3) & a1+a2+a3=1 & p4= a1*p1+a2*p2+a3*p3;
hence thesis;
end;
case
p in closed_inside_of_triangle(p1,p2,p3);
then
ex p4 being Point of TOP-REAL n st p4=p &
ex a1,a2,a3 being Real st 0
<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p4=a1 *p1+a2*p2+a3*p3;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for n being Element of NAT,p1,p2,p3 being Point of TOP-REAL n holds
Triangle(p1,p2,p3) c= closed_inside_of_triangle(p1,p2,p3)
proof
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
LSeg(p1,p2) \/ LSeg(p2,p3) \/ LSeg(p3,p1)
c= closed_inside_of_triangle(p1,p2,p3)
proof
let x be object;
assume
A1: x in LSeg(p1,p2) \/ LSeg(p2,p3) \/ LSeg(p3,p1);
then reconsider p0=x as Point of TOP-REAL n;
A2: x in LSeg(p1,p2) \/ LSeg(p2,p3) or x in LSeg(p3,p1) by A1,XBOOLE_0:def 3;
now
per cases by A2,XBOOLE_0:def 3;
case
x in LSeg(p1,p2);
then consider lambda being Real such that
A3: x=(1-lambda)*p1 + lambda*p2 and
A4: 0 <= lambda and
A5: lambda <= 1;
A6: p0=(1-lambda)*p1 + lambda*p2+0.TOP-REAL n by A3,RLVECT_1:4
.=(1-lambda)*p1 + lambda*p2+(0)*p3 by RLVECT_1:10;
A7: (1-lambda)+lambda+0=1;
1-lambda>=0 by A5,XREAL_1:48;
hence
ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p0
=a1*p1+a2*p2+a3*p3 by A4,A7,A6;
end;
case
x in LSeg(p2,p3);
then consider lambda being Real such that
A8: x=(1-lambda)*p2 + lambda*p3 and
A9: 0 <= lambda and
A10: lambda <= 1;
A11: p0=0.TOP-REAL n +(1-lambda)*p2 + lambda*p3 by A8,RLVECT_1:4
.=(0)*p1+(1-lambda)*p2 + lambda*p3 by RLVECT_1:10;
A12: 0+(1-lambda)+lambda=1;
1-lambda>=0 by A10,XREAL_1:48;
hence
ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p0
=a1*p1+a2*p2+a3*p3 by A9,A12,A11;
end;
case
x in LSeg(p3,p1);
then consider lambda being Real such that
A13: x=(1-lambda)*p3 + lambda*p1 and
A14: 0 <= lambda and
A15: lambda <= 1;
A16: p0=lambda*p1+0.TOP-REAL n+ (1-lambda)*p3 by A13,RLVECT_1:4
.=lambda*p1+(0)*p2+ (1-lambda)*p3 by RLVECT_1:10;
A17: lambda+0+(1-lambda)=1;
1-lambda>=0 by A15,XREAL_1:48;
hence
ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p0
=a1*p1+a2*p2+a3*p3 by A14,A17,A16;
end;
end;
hence thesis;
end;
hence thesis;
end;
definition
let n be Element of NAT,q1,q2 be Point of TOP-REAL n;
pred q1,q2 are_lindependent2 means
for a1,a2 being Real st a1*q1+a2* q2=0.TOP-REAL n holds a1=0 & a2=0;
end;
notation
let n be Element of NAT,q1,q2 be Point of TOP-REAL n;
antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2;
end;
theorem Th50:
for n being Element of NAT,q1,q2 being Point of TOP-REAL n st q1
,q2 are_lindependent2 holds q1<>q2 & q1<>0.TOP-REAL n & q2<>0.TOP-REAL n
proof
let n be Element of NAT,q1,q2 be Point of TOP-REAL n;
assume
A1: q1,q2 are_lindependent2;
assume
A2: q1=q2 or q1=0.TOP-REAL n or q2=0.TOP-REAL n;
now
per cases by A2;
case
A3: q1=q2;
1*q1+(-1)*q2=1*q1+(-q2) by RLVECT_1:16
.= q1+(-q2) by RLVECT_1:def 8
.=0.TOP-REAL n by A3,RLVECT_1:5;
hence contradiction by A1;
end;
case
q1=0.TOP-REAL n;
then 1*q1+(0)*q2=0.TOP-REAL n+(0)*q2 by RLVECT_1:10
.=0.TOP-REAL n+0.TOP-REAL n by RLVECT_1:10
.=0.TOP-REAL n by RLVECT_1:4;
hence contradiction by A1;
end;
case
q2=0.TOP-REAL n;
then (0)*q1+1*q2=(0)*q1+0.TOP-REAL n by RLVECT_1:10
.=0.TOP-REAL n+0.TOP-REAL n by RLVECT_1:10
.=0.TOP-REAL n by RLVECT_1:4;
hence contradiction by A1;
end;
end;
hence contradiction;
end;
theorem Th51:
for n being Element of NAT, p1,p2,p3,p0 being Point of TOP-REAL
n st p2-p1,p3-p1 are_lindependent2 & p0 in plane(p1,p2,p3)
ex a1,a2,a3 being Real
st p0=a1*p1+a2*p2+a3*p3 & a1+a2+a3=1 &
for b1,b2,b3 being Real st p0
=b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1=a1 & b2=a2 & b3=a3
proof
let n be Element of NAT,p1,p2,p3,p0 be Point of TOP-REAL n;
assume that
A1: p2-p1,p3-p1 are_lindependent2 and
A2: p0 in plane(p1,p2,p3);
set q2=p2-p1,q3=p3-p1;
consider a01,a02,a03 being Real such that
A3: a01+a02+a03=1 and
A4: p0=a01*p1+a02*p2+a03*p3 by A2,Th48;
for b1,b2,b3 being Real
st p0=b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1=
a01 & b2=a02 & b3=a03
proof
A5: p0+-p1=a01*p1+a02*p2+a03*p3+-(a01+a02+a03)*p1 by A3,A4,RLVECT_1:def 8
.=a01*p1+a02*p2+a03*p3+-((a01+a02)*p1+a03*p1) by RLVECT_1:def 6
.=a01*p1+a02*p2+a03*p3+-(a01*p1+a02*p1+a03*p1) by RLVECT_1:def 6
.=a01*p1+a02*p2+a03*p3+(-(a01*p1+a02*p1)-a03*p1) by RLVECT_1:30
.=a01*p1+a02*p2+a03*p3+(-a01*p1-a02*p1-a03*p1) by RLVECT_1:30
.=a01*p1+(a02*p2+a03*p3)+(-a01*p1+-a02*p1+-a03*p1) by RLVECT_1:def 3
.=a01*p1+(a02*p2+a03*p3)+(-a01*p1+(-a02*p1+-a03*p1)) by RLVECT_1:def 3
.=(a02*p2+a03*p3)+a01*p1-a01*p1+(-a02*p1+-a03*p1) by RLVECT_1:def 3
.=(a02*p2+a03*p3)+(-a02*p1+-a03*p1) by RLVECT_4:1
.=a02*p2+a03*p3+-a02*p1+-a03*p1 by RLVECT_1:def 3
.=a02*p2+-a02*p1+a03*p3+-a03*p1 by RLVECT_1:def 3
.=a02*p2+a02*(-p1)+a03*p3+-a03*p1 by RLVECT_1:25
.=a02*(p2+(-p1))+a03*p3+-a03*p1 by RLVECT_1:def 5
.=a02*(p2+(-p1))+(a03*p3+-a03*p1) by RLVECT_1:def 3
.=a02*(p2+(-p1))+(a03*p3+a03*(-p1)) by RLVECT_1:25
.=a02*q2+a03*q3 by RLVECT_1:def 5;
let b1,b2,b3 be Real;
assume that
A6: p0=b1*p1+b2*p2+b3*p3 and
A7: b1+b2+b3=1;
p0+-p1=b1*p1+b2*p2+b3*p3+-(b1+b2+b3)*p1 by A6,A7,RLVECT_1:def 8
.=b1*p1+b2*p2+b3*p3+-((b1+b2)*p1+b3*p1) by RLVECT_1:def 6
.=b1*p1+b2*p2+b3*p3+-(b1*p1+b2*p1+b3*p1) by RLVECT_1:def 6
.=b1*p1+b2*p2+b3*p3+(-(b1*p1+b2*p1)-b3*p1) by RLVECT_1:30
.=b1*p1+b2*p2+b3*p3+(-b1*p1-b2*p1-b3*p1) by RLVECT_1:30
.=b1*p1+(b2*p2+b3*p3)+(-b1*p1+-b2*p1+-b3*p1) by RLVECT_1:def 3
.=b1*p1+(b2*p2+b3*p3)+(-b1*p1+(-b2*p1+-b3*p1)) by RLVECT_1:def 3
.=(b2*p2+b3*p3)+b1*p1-b1*p1+(-b2*p1+-b3*p1) by RLVECT_1:def 3
.=(b2*p2+b3*p3)+(-b2*p1+-b3*p1) by RLVECT_4:1
.=b2*p2+b3*p3+-b2*p1+-b3*p1 by RLVECT_1:def 3
.=b2*p2+-b2*p1+b3*p3+-b3*p1 by RLVECT_1:def 3
.=b2*p2+b2*(-p1)+b3*p3+-b3*p1 by RLVECT_1:25
.=b2*(p2+(-p1))+b3*p3+-b3*p1 by RLVECT_1:def 5
.=b2*(p2+(-p1))+(b3*p3+-b3*p1) by RLVECT_1:def 3
.=b2*(p2+(-p1))+(b3*p3+b3*(-p1)) by RLVECT_1:25
.=b2*q2+b3*q3 by RLVECT_1:def 5;
then b2*q2+b3*q3+-(a02*q2+a03*q3)=0.TOP-REAL n by A5,RLVECT_1:5;
then b2*q2+b3*q3+(-a02*q2-a03*q3)=0.TOP-REAL n by RLVECT_1:30;
then b2*q2+b3*q3+-a02*q2+-a03*q3=0.TOP-REAL n by RLVECT_1:def 3;
then b2*q2+-a02*q2+b3*q3+-a03*q3=0.TOP-REAL n by RLVECT_1:def 3;
then b2*q2+(-a02)*q2+b3*q3+-a03*q3=0.TOP-REAL n by RLVECT_1:79;
then (b2+-a02)*q2+b3*q3+-a03*q3=0.TOP-REAL n by RLVECT_1:def 6;
then (b2+-a02)*q2+(b3*q3+-a03*q3)=0.TOP-REAL n by RLVECT_1:def 3;
then (b2+-a02)*q2+(b3*q3+(-a03)*q3)=0.TOP-REAL n by RLVECT_1:79;
then (b2+-a02)*q2+(b3+-a03)*q3=0.TOP-REAL n by RLVECT_1:def 6;
then b2-a02+a02=0+a02 & b3+-a03=0 by A1;
hence thesis by A3,A7;
end;
hence thesis by A3,A4;
end;
theorem Th52:
for n being Element of NAT, p1,p2,p3,p0 being Point of TOP-REAL
n st (ex a1,a2,a3 being Real
st p0=a1*p1+a2*p2+a3*p3 & a1+a2+a3=1) holds p0 in
plane(p1,p2,p3)
proof
let n be Element of NAT,p1,p2,p3,p0 be Point of TOP-REAL n;
given a1,a2,a3 being Real such that
A1: p0=a1*p1+a2*p2+a3*p3 & a1+a2+a3=1;
now
per cases;
case
0>a1 or 0>a2 or 0>a3;
then p0 in outside_of_triangle(p1,p2,p3) by A1;
hence thesis by XBOOLE_0:def 3;
end;
case
0<=a1 & 0<=a2 & 0<=a3;
then p0 in closed_inside_of_triangle(p1,p2,p3) by A1;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem
for n being Element of NAT,p1,p2,p3 being Point of TOP-REAL n holds
plane(p1,p2,p3)={p where p is Point of TOP-REAL n:
ex a1,a2,a3 being Real st a1
+a2+a3=1 & p=a1*p1+a2*p2+a3*p3}
proof
let n be Element of NAT,p1,p2,p3 be Point of TOP-REAL n;
thus plane(p1,p2,p3) c= {p where p is Point of TOP-REAL n: ex a1,a2,a3 being
Real st a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3}
proof
let x be object;
assume
A1: x in plane(p1,p2,p3);
then reconsider p0=x as Point of TOP-REAL n;
ex a1,a2,a3 being Real
st a1+a2+a3=1 & p0=a1*p1+a2*p2+a3 *p3 by A1,Th48;
hence thesis;
end;
let x be object;
assume x in {p where p is Point of TOP-REAL n:
ex a1,a2,a3 being Real st a1
+a2+a3=1 & p=a1*p1+a2*p2+a3*p3};
then
ex p being Point of TOP-REAL n st p=x &
ex a1,a2,a3 being Real st a1+a2+
a3=1 & p=a1*p1+a2*p2+a3*p3;
hence thesis by Th52;
end;
theorem Th54:
for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds plane(p1,p2, p3)=REAL 2
proof
let p1,p2,p3;
assume
A1: p2-p1,p3-p1 are_lindependent2;
the carrier of TOP-REAL 2=REAL 2 by EUCLID:22;
hence plane(p1,p2,p3) c= REAL 2;
let x be object;
assume x in REAL 2;
then reconsider p0=x as Point of TOP-REAL 2 by EUCLID:22;
set q2=p2-p1,q3=p3-p1,p=p0-p1;
A2: q3<>0.TOP-REAL 2 by A1,Th50;
now
per cases by A2,EUCLID:53,54;
case
A3: q3`1<>0;
A4: now
assume q2`2*q3`1-q2`1*q3`2=0;
then q2`2=q2`1*q3`2/q3`1 by A3,XCMPLX_1:89;
then q2 = |[q2`1,q2`1*q3`2/q3`1]| by EUCLID:53
.=|[q2`1*1,q2`1*q3`2*(q3`1)"]| by XCMPLX_0:def 9
.=|[q2`1*1,q2`1*(q3`2*(q3`1)")]|
.=(q2`1)*|[1,q3`2*(q3`1)"]| by EUCLID:58
.=(q2`1)*|[(q3`1)"*q3`1,(q3`1)"*q3`2]| by A3,XCMPLX_0:def 7
.=(q2`1)*((q3`1)"*|[q3`1,q3`2]|) by EUCLID:58
.=(q2`1)*((q3`1)"*q3) by EUCLID:53
.=(q2`1)*(q3`1)"*q3 by RLVECT_1:def 7;
then q2+-((q2`1)*(q3`1)"*q3)=0.TOP-REAL 2 by RLVECT_1:5;
then 1*q2+-((q2`1)*(q3`1)"*q3)=0.TOP-REAL 2 by RLVECT_1:def 8;
then 1*q2+(-((q2`1)*(q3`1)"))*q3=0.TOP-REAL 2 by RLVECT_1:79;
hence contradiction by A1;
end;
set a=(p`2*q3`1-q3`2*p`1)/(q2`2*q3`1-q2`1*q3`2);
set b=(p`1-a*q2`1)/q3`1;
A5: a*(q2`1)+b*(q3`1)=a*q2`1+(p`1-a*q2`1) by A3,XCMPLX_1:87
.=p`1;
A6: a*(q2`2)+b*(q3`2)=a*q2`2+(p`1/q3`1-a*q2`1/q3`1)*q3`2 by XCMPLX_1:120
.=a*q2`2-a*q2`1/q3`1*q3`2+p`1/q3`1*q3`2
.=a*q2`2-a*q2`1*(q3`1")*q3`2+p`1/q3`1*q3`2 by XCMPLX_0:def 9
.=a*(q2`2-q2`1*(q3`1)"*q3`2)+p`1/q3`1*q3`2
.=a*(q2`2-q2`1/(q3`1)*q3`2)+p`1/q3`1*q3`2 by XCMPLX_0:def 9
.=a*(q2`2/q3`1*q3`1-q2`1/q3`1*q3`2)+p`1/q3`1*q3`2 by A3,XCMPLX_1:87
.=a*((q3`1/q3`1)*q2`2-q2`1/q3`1*q3`2)+p`1/q3`1*q3`2 by XCMPLX_1:75
.=a*(q3`1*(q3`1)"*q2`2-q2`1/(q3`1)*q3`2)+p`1/q3`1*q3`2 by
XCMPLX_0:def 9
.=a*(q2`2*(q3`1*(q3`1)")-(q3`1)"*q2`1*q3`2)+p`1/q3`1*q3`2 by
XCMPLX_0:def 9
.=a*(q2`2*q3`1-q2`1*q3`2)*(q3`1)"+p`1/q3`1*q3`2
.=(p`2*q3`1-q3`2*p`1)*(q3`1)"+p`1/q3`1*q3`2 by A4,XCMPLX_1:87
.=(p`2*q3`1-q3`2*p`1)*(q3`1)"+(q3`1)"*p`1*q3`2 by XCMPLX_0:def 9
.=((p`2*q3`1-q3`2*p`1)+(q3`2*p`1))*(q3`1)"
.=(p`2*q3`1)/(q3`1) by XCMPLX_0:def 9
.=p`2 by A3,XCMPLX_1:89;
A7: a*q2+b*q3=a*p2-a*p1+b*(p3-p1) by RLVECT_1:34
.=a*p2+-a*p1+(b*p3-b*p1) by RLVECT_1:34
.=a*p2+-a*p1+(b*p3+(-b)*p1) by RLVECT_1:79
.=a*p2+(-a)*p1+((-b)*p1+b*p3) by RLVECT_1:79
.=a*p2+(-a)*p1+(-b)*p1+b*p3 by RLVECT_1:def 3
.=a*p2+((-a)*p1+(-b)*p1)+b*p3 by RLVECT_1:def 3
.=(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 6;
a*q2+b*q3=a*|[q2`1,q2`2]|+b*q3 by EUCLID:53
.= a*|[q2`1,q2`2]|+b*|[q3`1,q3`2]| by EUCLID:53
.= |[a*(q2`1),a*(q2`2)]|+b*|[q3`1,q3`2]| by EUCLID:58
.= |[a*(q2`1),a*(q2`2)]|+|[b*(q3`1),b*(q3`2)]| by EUCLID:58
.= |[a*(q2`1)+b*(q3`1),a*(q2`2)+b*(q3`2)]| by EUCLID:56
.= p by A5,A6,EUCLID:53;
then
A8: p0=p1+((-a+-b)*p1+a*p2+b*p3) by A7,RLVECT_4:1
.= p1+((-a+-b)*p1+a*p2)+b*p3 by RLVECT_1:def 3
.= p1+(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 3
.= 1*p1+(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 8
.=(1+(-a+-b))*p1+a*p2+b*p3 by RLVECT_1:def 6;
1+(-a+-b)+a+b=1;
hence thesis by A8,Th52;
end;
case
A9: q3`2<>0;
now
assume q2`2*q3`1-q2`1*q3`2=0;
then q2`1=q2`2*q3`1/q3`2 by A9,XCMPLX_1:89;
then q2 = |[q2`2*q3`1/q3`2,q2`2]| by EUCLID:53
.=|[q2`2*q3`1*(q3`2)",q2`2*1]| by XCMPLX_0:def 9
.=|[q2`2*(q3`1*(q3`2)"),q2`2*1]|
.=(q2`2)*|[q3`1*(q3`2)",1]| by EUCLID:58
.=(q2`2)*|[(q3`2)"*q3`1,(q3`2)"*q3`2]| by A9,XCMPLX_0:def 7
.=(q2`2)*((q3`2)"*|[q3`1,q3`2]|) by EUCLID:58
.=(q2`2)*((q3`2)"*q3) by EUCLID:53
.=(q2`2)*(q3`2)"*q3 by RLVECT_1:def 7;
then q2+-((q2`2)*(q3`2)"*q3)=0.TOP-REAL 2 by RLVECT_1:5;
then 1*q2+-((q2`2)*(q3`2)"*q3)=0.TOP-REAL 2 by RLVECT_1:def 8;
then 1*q2+(-((q2`2)*(q3`2)"))*q3=0.TOP-REAL 2 by RLVECT_1:79;
hence contradiction by A1;
end;
then
A10: -(q2`2*q3`1+-q2`1*q3`2)<> -0;
set a=(p`1*q3`2-q3`1*p`2)/(q2`1*q3`2-q2`2*q3`1);
set b=(p`2-a*q2`2)/q3`2;
A11: a*(q2`2)+b*(q3`2)=a*q2`2+(p`2-a*q2`2) by A9,XCMPLX_1:87
.=p`2;
A12: a*(q2`1)+b*(q3`1)=a*q2`1+(p`2/q3`2-a*q2`2/q3`2)*q3`1 by XCMPLX_1:120
.=a*q2`1-a*q2`2/q3`2*q3`1+p`2/q3`2*q3`1
.=a*q2`1-a*q2`2*(q3`2")*q3`1+p`2/q3`2*q3`1 by XCMPLX_0:def 9
.=a*(q2`1-q2`2*(q3`2)"*q3`1)+p`2/q3`2*q3`1
.=a*(q2`1-q2`2/(q3`2)*q3`1)+p`2/q3`2*q3`1 by XCMPLX_0:def 9
.=a*(q2`1/q3`2*q3`2-q2`2/q3`2*q3`1)+p`2/q3`2*q3`1 by A9,XCMPLX_1:87
.=a*((q3`2/q3`2)*q2`1-q2`2/q3`2*q3`1)+p`2/q3`2*q3`1 by XCMPLX_1:75
.=a*(q3`2*(q3`2)"*q2`1-q2`2/(q3`2)*q3`1)+p`2/q3`2*q3`1 by
XCMPLX_0:def 9
.=a*(q2`1*(q3`2*(q3`2)")-(q3`2)"*q2`2*q3`1)+p`2/q3`2*q3`1 by
XCMPLX_0:def 9
.=a*(q2`1*q3`2-q2`2*q3`1)*(q3`2)"+p`2/q3`2*q3`1
.=(p`1*q3`2-q3`1*p`2)*(q3`2)"+p`2/q3`2*q3`1 by A10,XCMPLX_1:87
.=(p`1*q3`2-q3`1*p`2)*(q3`2)"+(q3`2)"*p`2*q3`1 by XCMPLX_0:def 9
.=((p`1*q3`2-q3`1*p`2)+(q3`1*p`2))*(q3`2)"
.=(p`1*q3`2)/(q3`2) by XCMPLX_0:def 9
.=p`1 by A9,XCMPLX_1:89;
A13: a*q2+b*q3=a*p2-a*p1+b*(p3-p1) by RLVECT_1:34
.=a*p2+-a*p1+(b*p3-b*p1) by RLVECT_1:34
.=a*p2+-a*p1+(b*p3+(-b)*p1) by RLVECT_1:79
.=a*p2+(-a)*p1+((-b)*p1+b*p3) by RLVECT_1:79
.=a*p2+(-a)*p1+(-b)*p1+b*p3 by RLVECT_1:def 3
.=a*p2+((-a)*p1+(-b)*p1)+b*p3 by RLVECT_1:def 3
.=(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 6;
a*q2+b*q3=a*|[q2`1,q2`2]|+b*q3 by EUCLID:53
.= a*|[q2`1,q2`2]|+b*|[q3`1,q3`2]| by EUCLID:53
.= |[a*(q2`1),a*(q2`2)]|+b*|[q3`1,q3`2]| by EUCLID:58
.= |[a*(q2`1),a*(q2`2)]|+|[b*(q3`1),b*(q3`2)]| by EUCLID:58
.= |[a*(q2`1)+b*(q3`1),a*(q2`2)+b*(q3`2)]| by EUCLID:56
.= p by A11,A12,EUCLID:53;
then
A14: p0=p1+((-a+-b)*p1+a*p2+b*p3) by A13,RLVECT_4:1
.= p1+((-a+-b)*p1+a*p2)+b*p3 by RLVECT_1:def 3
.= p1+(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 3
.= 1*p1+(-a+-b)*p1+a*p2+b*p3 by RLVECT_1:def 8
.=(1+(-a+-b))*p1+a*p2+b*p3 by RLVECT_1:def 6;
1+(-a+-b)+a+b=1;
hence thesis by A14,Th52;
end;
end;
hence thesis;
end;
definition
let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
assume
A1: p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
func tricord1(p1,p2,p3,p) -> Real means
:Def11:
ex a2,a3 being Real st it+a2 +a3=1 & p=it*p1+a2*p2+a3*p3;
existence
proof
ex a01,a02,a03 being Real st
p=a01*p1+a02*p2+a03*p3 & a01+a02+a03=1 &
for b1,b2,b3 being Real
st p=b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1 =a01 & b2=a02 & b3=a03
by A1,Th51;
hence thesis;
end;
uniqueness
proof
let a1,b1 be Real;
assume that
A2: ex a2,a3 being Real st a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3 and
A3: ex a2,a3 being Real st b1+a2+a3=1 & p=b1*p1+a2*p2+a3*p3;
consider a001,a002,a003 being Real such that
p=a001*p1+a002*p2+a003*p3 and
a001+a002+a003=1 and
A4: for b01,b02,b03 being Real
st p=b01*p1+b02*p2+b03*p3 & b01+b02+b03
=1 holds b01=a001 & b02=a002 & b03=a003 by A1,Th51;
a1=a001 by A2,A4;
hence thesis by A3,A4;
end;
end;
definition
let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
assume
A1: p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
func tricord2(p1,p2,p3,p) -> Real means
:Def12:
ex a1,a3 being Real st a1+it +a3=1 & p=a1*p1+it*p2+a3*p3;
existence
proof
ex a01,a02,a03 being Real st
p=a01*p1+a02*p2+a03*p3 & a01+a02+a03=1 &
for b1,b2,b3 being Real
st p=b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1 =a01 & b2=a02 & b3=a03
by A1,Th51;
hence thesis;
end;
uniqueness
proof
let a2,b2 be Real;
assume that
A2: ex a1,a3 being Real st a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3 and
A3: ex a1,a3 being Real st a1+b2+a3=1 & p=a1*p1+b2*p2+a3*p3;
consider a001,a002,a003 being Real such that
p=a001*p1+a002*p2+a003*p3 and
a001+a002+a003=1 and
A4: for b01,b02,b03 being Real st p=b01*p1+b02*p2+b03*p3 & b01+b02+b03
=1 holds b01=a001 & b02=a002 & b03=a003 by A1,Th51;
a2=a002 by A2,A4;
hence thesis by A3,A4;
end;
end;
definition
let n be Element of NAT,p1,p2,p3,p be Point of TOP-REAL n;
assume
A1: p2-p1,p3-p1 are_lindependent2 & p in plane(p1,p2,p3);
func tricord3(p1,p2,p3,p) -> Real means
:Def13:
ex a1,a2 being Real st a1+a2 +it=1 & p=a1*p1+a2*p2+it*p3;
existence
proof
ex a01,a02,a03 being Real st
p=a01*p1+a02*p2+a03*p3 & a01+a02+a03=1 &
for b1,b2,b3 being Real
st p=b1*p1+b2*p2+b3*p3 & b1+b2+b3=1 holds b1 =a01 & b2=a02 & b3=a03
by A1,Th51;
hence thesis;
end;
uniqueness
proof
let a3,b3 be Real;
assume that
A2: ex a1,a2 being Real st a1+a2+a3=1 & p=a1*p1+a2*p2+a3*p3 and
A3: ex a1,a2 being Real st a1+a2+b3=1 & p=a1*p1+a2*p2+b3*p3;
consider a001,a002,a003 being Real such that
p=a001*p1+a002*p2+a003*p3 and
a001+a002+a003=1 and
A4: for b01,b02,b03 being Real
st p=b01*p1+b02*p2+b03*p3 & b01+b02+b03
=1 holds b01=a001 & b02=a002 & b03=a003 by A1,Th51;
a3=a003 by A2,A4;
hence thesis by A3,A4;
end;
end;
definition
let p1,p2,p3;
func trcmap1(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
for p holds it.p= tricord1(p1,p2,p3,p);
existence
proof
defpred P[object,object] means
for p st p=$1 holds $2=tricord1(p1,p2,p3,p);
set X=the carrier of TOP-REAL 2,Y=the carrier of R^1;
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume x in X;
then reconsider p0=x as Point of TOP-REAL 2;
A2: tricord1(p1,p2,p3,p0) in REAL by XREAL_0:def 1;
P[x,tricord1(p1,p2,p3,p0)];
hence thesis by A2,TOPMETR:17;
end;
ex f being Function of X,Y st
for x being object st x in X holds P[x,f.x]
from FUNCT_2:sch 1(A1);
then consider g being Function of X,Y such that
A3: for x being object st x in X holds for p st p=x holds g.x=tricord1(p1
,p2,p3,p);
reconsider f0=g as Function of TOP-REAL 2,R^1;
for p holds f0.p=tricord1(p1,p2,p3,p) by A3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of TOP-REAL 2,R^1;
assume that
A4: for p holds f1.p=tricord1(p1,p2,p3,p) and
A5: for p holds f2.p=tricord1(p1,p2,p3,p);
A6: for x being object st x in dom f1 holds f1.x=f2.x
proof
let x be object;
assume x in dom f1;
then reconsider p0=x as Point of TOP-REAL 2 by FUNCT_2:def 1;
f1.p0=tricord1(p1,p2,p3,p0) by A4;
hence thesis by A5;
end;
dom f1= the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then dom f1=dom f2 by FUNCT_2:def 1;
hence f1=f2 by A6,FUNCT_1:2;
end;
end;
definition
let p1,p2,p3;
func trcmap2(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
for p holds it.p= tricord2(p1,p2,p3,p);
existence
proof
defpred P[object,object] means
for p st p=$1 holds $2=tricord2(p1,p2,p3,p);
set X=the carrier of TOP-REAL 2,Y=the carrier of R^1;
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume x in X;
then reconsider p0=x as Point of TOP-REAL 2;
reconsider t = tricord2(p1,p2,p3,p0) as Element of REAL by XREAL_0:def 1;
P[x,t];
hence thesis by TOPMETR:17;
end;
ex f being Function of X,Y st
for x being object st x in X holds P[x,f.x]
from FUNCT_2:sch 1(A1);
then consider g being Function of X,Y such that
A2: for x being object st x in X holds for p st p=x holds g.x=tricord2(p1
,p2,p3,p);
reconsider f0=g as Function of TOP-REAL 2,R^1;
for p holds f0.p=tricord2(p1,p2,p3,p) by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of TOP-REAL 2,R^1;
assume that
A3: for p holds f1.p=tricord2(p1,p2,p3,p) and
A4: for p holds f2.p=tricord2(p1,p2,p3,p);
A5: for x being object st x in dom f1 holds f1.x=f2.x
proof
let x be object;
assume x in dom f1;
then reconsider p0=x as Point of TOP-REAL 2 by FUNCT_2:def 1;
f1.p0=tricord2(p1,p2,p3,p0) by A3;
hence thesis by A4;
end;
dom f1= the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then dom f1=dom f2 by FUNCT_2:def 1;
hence f1=f2 by A5,FUNCT_1:2;
end;
end;
definition
let p1,p2,p3;
func trcmap3(p1,p2,p3) -> Function of TOP-REAL 2,R^1 means
for p holds it.p= tricord3(p1,p2,p3,p);
existence
proof
defpred P[object,object] means
for p st p=$1 holds $2=tricord3(p1,p2,p3,p);
set X=the carrier of TOP-REAL 2,Y=the carrier of R^1;
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume x in X;
then reconsider p0=x as Point of TOP-REAL 2;
A2: tricord3(p1,p2,p3,p0) in REAL by XREAL_0:def 1;
P[x,tricord3(p1,p2,p3,p0)];
hence thesis by A2,TOPMETR:17;
end;
ex f being Function of X,Y st
for x being object st x in X holds P[x,f.x]
from FUNCT_2:sch 1(A1);
then consider g being Function of X,Y such that
A3: for x being object st x in X holds for p st p=x holds g.x=tricord3(p1
,p2,p3,p);
reconsider f0=g as Function of TOP-REAL 2,R^1;
for p holds f0.p=tricord3(p1,p2,p3,p) by A3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of TOP-REAL 2,R^1;
assume that
A4: for p holds f1.p=tricord3(p1,p2,p3,p) and
A5: for p holds f2.p=tricord3(p1,p2,p3,p);
A6: for x being object st x in dom f1 holds f1.x=f2.x
proof
let x be object;
assume x in dom f1;
then reconsider p0=x as Point of TOP-REAL 2 by FUNCT_2:def 1;
f1.p0=tricord3(p1,p2,p3,p0) by A4;
hence thesis by A5;
end;
dom f1= the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then dom f1=dom f2 by FUNCT_2:def 1;
hence f1=f2 by A6,FUNCT_1:2;
end;
end;
theorem
for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
outside_of_triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)<0 or tricord2(p1,p2,p3,p
)<0 or tricord3(p1,p2,p3,p)<0
proof
let p1,p2,p3,p;
set i1=tricord1(p1,p2,p3,p),i2=tricord2(p1,p2,p3,p), i3=tricord3(p1,p2,p3,p);
assume
A1: p2-p1,p3-p1 are_lindependent2;
thus p in outside_of_triangle(p1,p2,p3) implies tricord1(p1,p2,p3,p)<0 or
tricord2(p1,p2,p3,p)<0 or tricord3(p1,p2,p3,p)<0
proof assume
A2: p in outside_of_triangle(p1,p2,p3);
p in the carrier of TOP-REAL 2;
then p in REAL 2 by EUCLID:22;
then
A3: p in plane(p1,p2,p3) by A1,Th54;
consider p0 such that
A4: p0=p and
A5: ex a1,a2,a3 being Real st
(0>a1 or 0>a2 or 0>a3) & a1+a2+a3=1 & p0= a1*p1+a2*p2+a3*p3 by A2;
ex a1,a2,a3 being Real st
(0>a1 or 0>a2 or 0>a3) & a1+a2+a3=1 & p0= a1*p1+a2*p2+a3*p3 by A5;
hence thesis by A1,A3,Def11,Def12,Def13,A4;
end;
p in the carrier of TOP-REAL 2;
then p in REAL 2 by EUCLID:22;
then
A6: p in plane(p1,p2,p3) by A1,Th54;
then consider a2,a3 being Real such that
A7: i1+a2+a3=1 & p=i1*p1+a2*p2+a3*p3 by A1,Def11;
assume
A8: tricord1(p1,p2,p3,p)<0 or tricord2(p1,p2,p3,p)<0 or tricord3(p1,p2,
p3,p)<0;
a2=i2 & a3=i3 by A1,A6,A7,Def12,Def13;
hence thesis by A8,A7;
end;
theorem Th56:
for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
Triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)>=0 &
tricord3(p1,p2,p3,p)>=0 & (tricord1(p1,p2,p3,p)=0 or tricord2(p1,p2,p3,p)=0 or
tricord3(p1,p2,p3,p)=0)
proof
let p1,p2,p3,p;
assume
A1: p2-p1,p3-p1 are_lindependent2;
A2: for p0 holds p0 in Triangle(p1,p2,p3) iff p0 in LSeg(p1,p2) or p0 in
LSeg(p2,p3) or p0 in LSeg(p3,p1)
proof
let p0;
p0 in Triangle(p1,p2,p3) iff p0 in LSeg(p1,p2) \/ LSeg(p2,p3) or p0 in
LSeg(p3,p1) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
thus p in Triangle(p1,p2,p3) implies tricord1(p1,p2,p3,p)>=0 & tricord2(p1,
p2,p3,p)>=0 & tricord3(p1,p2,p3,p)>=0 & (tricord1(p1,p2,p3,p)=0 or tricord2(p1,
p2,p3,p)=0 or tricord3(p1,p2,p3,p)=0)
proof
set x=p;
assume
A3: p in Triangle(p1,p2,p3);
A4: now
per cases by A2,A3;
case
x in LSeg(p1,p2);
then consider lambda being Real such that
A5: x=(1-lambda)*p1 + lambda*p2 and
A6: 0 <= lambda and
A7: lambda <= 1;
A8: p=(1-lambda)*p1 + lambda*p2+0.TOP-REAL 2 by A5,RLVECT_1:4
.=(1-lambda)*p1 + lambda*p2+(0)*p3 by RLVECT_1:10;
A9: (1-lambda)+lambda+0=1;
1-lambda>=0 by A7,XREAL_1:48;
hence ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & (
a1=0 or a2=0 or a3=0) & p=a1*p1+a2*p2+a3*p3 by A6,A9,A8;
end;
case
x in LSeg(p2,p3);
then consider lambda being Real such that
A10: x=(1-lambda)*p2 + lambda*p3 and
A11: 0 <= lambda and
A12: lambda <= 1;
A13: p=0.TOP-REAL 2 +(1-lambda)*p2 + lambda*p3 by A10,RLVECT_1:4
.=(0)*p1+(1-lambda)*p2 + lambda*p3 by RLVECT_1:10;
A14: 0+(1-lambda)+lambda=1;
1-lambda>=0 by A12,XREAL_1:48;
hence ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & (
a1=0 or a2=0 or a3=0)& p=a1*p1+a2*p2+a3*p3 by A11,A14,A13;
end;
case
x in LSeg(p3,p1);
then consider lambda being Real such that
A15: x=(1-lambda)*p3 + lambda*p1 and
A16: 0 <= lambda and
A17: lambda <= 1;
A18: p=lambda*p1+0.TOP-REAL 2+ (1-lambda)*p3 by A15,RLVECT_1:4
.=lambda*p1+(0)*p2+ (1-lambda)*p3 by RLVECT_1:10;
A19: lambda+0+(1-lambda)=1;
1-lambda>=0 by A17,XREAL_1:48;
hence ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & (
a1=0 or a2=0 or a3=0)& p=a1*p1+a2*p2+a3*p3 by A16,A19,A18;
end;
end;
p in the carrier of TOP-REAL 2;
then p in REAL 2 by EUCLID:22;
then p in plane(p1,p2,p3) by A1,Th54;
hence thesis by A1,A4,Def11,Def12,Def13;
end;
thus tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)>=0 & tricord3(p1,p2,p3,p
)>=0 & (tricord1(p1,p2,p3,p)=0 or tricord2(p1,p2,p3,p)=0 or tricord3(p1,p2,p3,p
)=0) implies p in Triangle(p1,p2,p3)
proof
set p0=p;
assume that
A20: tricord1(p1,p2,p3,p)>=0 and
A21: tricord2(p1,p2,p3,p)>=0 and
A22: tricord3(p1,p2,p3,p)>=0 and
A23: tricord1(p1,p2,p3,p)=0 or tricord2(p1,p2,p3,p)=0 or tricord3(p1,
p2,p3,p)=0;
set i01=tricord1(p1,p2,p3,p0),i02=tricord2(p1,p2,p3,p0), i03=tricord3(p1,
p2,p3,p0);
p0 in the carrier of TOP-REAL 2;
then p0 in REAL 2 by EUCLID:22;
then
A24: p0 in plane(p1,p2,p3) by A1,Th54;
now
per cases by A23;
case
tricord1(p1,p2,p3,p)=0;
then consider a2,a3 being Real such that
A25: 0+a2+a3=1 and
A26: p=(0)*p1+a2*p2+a3*p3 by A1,A24,Def11;
a2=i02 by A1,A24,A25,A26,Def12;
then
A27: 1-a3+a3>=0+a3 by A21,A25,XREAL_1:7;
A28: p=0.TOP-REAL 2 + a2*p2+a3*p3 by A26,RLVECT_1:10
.=a2*p2+a3*p3 by RLVECT_1:4;
a3=i03 by A1,A24,A25,A26,Def13;
hence p in LSeg(p1,p2) or p in LSeg(p2,p3) or p in LSeg(p3,p1) by A22
,A25,A28,A27;
end;
case
tricord2(p1,p2,p3,p)=0;
then consider a1,a3 being Real such that
A29: a1+0+a3=1 and
A30: p=a1*p1+(0)*p2+a3*p3 by A1,A24,Def12;
a1=i01 by A1,A24,A29,A30,Def11;
then
A31: 1-a3+a3>=0+a3 by A20,A29,XREAL_1:7;
A32: p=a1*p1+0.TOP-REAL 2 +a3*p3 by A30,RLVECT_1:10
.=a1*p1+a3*p3 by RLVECT_1:4;
a3=i03 by A1,A24,A29,A30,Def13;
then p in { (1-lambda)*p1 + lambda*p3 where lambda is Real:
0<=lambda
& lambda<=1} by A22,A29,A32,A31;
hence p in LSeg(p1,p2) or p in LSeg(p2,p3) or p in LSeg(p3,p1) by
RLTOPSP1:def 2;
end;
case
tricord3(p1,p2,p3,p)=0;
then consider a1,a2 being Real such that
A33: a1+a2+0=1 and
A34: p=a1*p1+a2*p2+(0)*p3 by A1,A24,Def13;
a1=i01 by A1,A24,A33,A34,Def11;
then
A35: 1-a2+a2>=0+a2 by A20,A33,XREAL_1:7;
A36: p=a1*p1+a2*p2+0.TOP-REAL 2 by A34,RLVECT_1:10
.=a1*p1+a2*p2 by RLVECT_1:4;
a2=i02 by A1,A24,A33,A34,Def12;
hence p in LSeg(p1,p2) or p in LSeg(p2,p3) or p in LSeg(p3,p1) by A21
,A33,A36,A35;
end;
end;
hence thesis by A2;
end;
end;
theorem
for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in Triangle(p1
,p2,p3) iff tricord1(p1,p2,p3,p)=0 & tricord2(p1,p2,p3,p)>=0 & tricord3(p1,p2,
p3,p)>=0 or tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)=0 & tricord3(p1,p2,
p3,p)>=0 or tricord1(p1,p2,p3,p)>=0 & tricord2(p1,p2,p3,p)>=0 & tricord3(p1,p2,
p3,p)=0 by Th56;
theorem Th58:
for p1,p2,p3,p st p2-p1,p3-p1 are_lindependent2 holds p in
inside_of_triangle(p1,p2,p3) iff tricord1(p1,p2,p3,p)>0 & tricord2(p1,p2,p3,p)>
0 & tricord3(p1,p2,p3,p)>0
proof
let p1,p2,p3,p;
assume
A1: p2-p1,p3-p1 are_lindependent2;
A2: inside_of_triangle(p1,p2,p3) c= {p0 where p0 is Point of TOP-REAL 2: ex
a1,a2,a3 being Real st (0<a1 & 0<a2 & 0<a3) & a1+a2+a3=1 & p0=a1*p1+a2*p2+a3*p3
}
proof
let x be object;
assume
A3: x in inside_of_triangle(p1,p2,p3);
then
A4: not x in Triangle(p1,p2,p3) by XBOOLE_0:def 5;
x in closed_inside_of_triangle(p1,p2,p3) by A3,XBOOLE_0:def 5;
then consider p0 being Point of TOP-REAL 2 such that
A5: p0=x and
A6: ex a1,a2,a3 being Real
st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p0=
a1 *p1+a2*p2+a3*p3;
reconsider i01=tricord1(p1,p2,p3,p0),i02=tricord2(p1,p2,p3,p0),
i03=tricord3(p1,p2,p3,p0) as Real;
consider a1,a2,a3 being Real such that
A7: 0<=a1 and
A8: 0<=a2 and
A9: 0<=a3 and
A10: a1+a2+a3=1 & p0=a1*p1+a2*p2+a3*p3 by A6;
p0 in the carrier of TOP-REAL 2;
then p0 in REAL 2 by EUCLID:22;
then
A11: p0 in plane(p1,p2,p3) by A1,Th54;
then
A12: a1=i01 by A1,A10,Def11;
A13: a3=i03 by A1,A10,A11,Def13;
then
A14: i02<>0 by A1,A4,A5,A7,A9,A12,Th56;
A15: a2=i02 by A1,A10,A11,Def12;
then
A16: i03<>0 by A1,A4,A5,A7,A8,A12,Th56;
i01<>0 by A1,A4,A5,A8,A9,A15,A13,Th56;
hence thesis by A5,A7,A8,A9,A10,A12,A15,A13,A14,A16;
end;
thus p in inside_of_triangle(p1,p2,p3) implies tricord1(p1,p2,p3,p)>0 &
tricord2(p1,p2,p3,p)>0 & tricord3(p1,p2,p3,p)>0
proof
p in the carrier of TOP-REAL 2;
then p in REAL 2 by EUCLID:22;
then
A17: p in plane(p1,p2,p3) by A1,Th54;
assume
A18: p in inside_of_triangle(p1,p2,p3);
then p in closed_inside_of_triangle(p1,p2,p3) by XBOOLE_0:def 5;
then consider p0 being Point of TOP-REAL 2 such that
A19: p0=p and
A20: ex a1,a2,a3 being Real st 0<=a1 & 0<=a2 & 0<=a3 & a1+a2+a3=1 & p0
= a1*p1+a2*p2+a3*p3;
not p in Triangle(p1,p2,p3) by A18,XBOOLE_0:def 5;
then
not(tricord1(p1,p2,p3,p0)>=0 & tricord2(p1,p2,p3,p0)>=0 & tricord3(p1
,p2,p3,p0)>=0 & (tricord1(p1,p2,p3,p0)=0 or tricord2(p1,p2,p3,p0)=0 or tricord3
(p1,p2,p3,p0)=0)) by A1,A19,Th56;
hence thesis by A1,A19,A17,A20,Def11,Def12,Def13;
end;
{p0 where p0 is Point of TOP-REAL 2: ex a1,a2,a3 being Real st 0<a1 & 0
<a2 & 0<a3 & a1+a2+a3=1 & p0=a1*p1+a2*p2+a3*p3} c= inside_of_triangle(p1,p2,p3)
proof
let x be object;
assume x in {p0 where p0 is Point of TOP-REAL 2: ex a1,a2,a3 being Real
st (0<a1 & 0<a2 & 0<a3) & a1+a2+a3=1 & p0=a1*p1+a2*p2+a3*p3};
then consider p0 being Point of TOP-REAL 2 such that
A21: x=p0 and
A22: ex a1,a2,a3 being Real st 0<a1 & 0<a2 & 0<a3 & a1+a2+a3=1 & p0=a1
* p1+a2*p2+a3*p3;
A23: x in closed_inside_of_triangle(p1,p2,p3) by A21,A22;
set i01=tricord1(p1,p2,p3,p0),i02=tricord2(p1,p2,p3,p0), i03=tricord3(p1,
p2,p3,p0);
consider a01,a02,a03 being Real such that
A24: 0<a01 & 0<a02 & 0<a03 and
A25: a01+a02+a03=1 & p0=a01*p1+a02*p2+a03*p3 by A22;
p0 in the carrier of TOP-REAL 2;
then p0 in REAL 2 by EUCLID:22;
then
A26: p0 in plane(p1,p2,p3) by A1,Th54;
then
A27: a03=i03 by A1,A25,Def13;
a01=i01 & a02=i02 by A1,A25,A26,Def11,Def12;
then not x in Triangle(p1,p2,p3) by A1,A21,A24,A27,Th56;
hence thesis by A23,XBOOLE_0:def 5;
end;
then
A28: inside_of_triangle(p1,p2,p3)={p0 where p0 is Point of TOP-REAL 2: ex
a1,a2, a3 being Real st (0<a1 & 0<a2 & 0<a3) & a1+a2+a3=1 & p0=a1*p1+a2*p2+a3*
p3} by A2;
thus tricord1(p1,p2,p3,p)>0 & tricord2(p1,p2,p3,p)>0 & tricord3(p1,p2,p3,p)>
0 implies p in inside_of_triangle(p1,p2,p3)
proof
reconsider i1=tricord1(p1,p2,p3,p),i2=tricord2(p1,p2,p3,p),
i3=tricord3(p1,p2,p3,p) as Real;
assume
A29: tricord1(p1,p2,p3,p)>0 & tricord2(p1,p2,p3,p)>0 & tricord3(p1,p2, p3,p)>0;
p in the carrier of TOP-REAL 2;
then p in REAL 2 by EUCLID:22;
then
A30: p in plane(p1,p2,p3) by A1,Th54;
then consider a2,a3 being Real such that
A31: i1+a2+a3=1 & p=i1*p1+a2*p2+a3*p3 by A1,Def11;
a2=i2 & a3=i3 by A1,A30,A31,Def12,Def13;
hence thesis by A28,A29,A31;
end;
end;
theorem
for p1,p2,p3 st p2-p1,p3-p1 are_lindependent2 holds inside_of_triangle
(p1,p2,p3) is non empty
proof
let p1,p2,p3;
assume
A1: p2-p1,p3-p1 are_lindependent2;
set p0=(1/3)*p1+(1/3)*p2+(1/3)*p3;
set i01=tricord1(p1,p2,p3,p0),i02=tricord2(p1,p2,p3,p0), i03=tricord3(p1,p2,
p3,p0);
p0 in the carrier of TOP-REAL 2;
then p0 in REAL 2 by EUCLID:22;
then
A2: (1/3)+(1/3)+(1/3)=1 & p0 in plane(p1,p2,p3) by A1,Th54;
then
A3: 1/3=i03 by A1,Def13;
1/3=i01 & 1/3=i02 by A1,A2,Def11,Def12;
hence thesis by A1,A3,Th58;
end;