:: Oriented Metric-Affine Plane - Part I
:: by Jaroslaw Zajkowski
::
:: Received October 24, 1991
:: Copyright (c) 1991-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, RLVECT_1, XBOOLE_0, SUBSET_1, ARYTM_3, REAL_1, RELAT_1,
ARYTM_1, ANALMETR, SUPINF_2, CARD_1, MCART_1, ANALOAF, SYMSP_1, ZFMISC_1,
STRUCT_0, ANALORT;
notations TARSKI, ZFMISC_1, XXREAL_0, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1,
RELSET_1, NUMBERS, STRUCT_0, ALGSTR_0, RLVECT_1, ANALOAF, ANALMETR,
GEOMTRAP;
constructors DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, TDGROUP, ANALMETR,
GEOMTRAP;
registrations RELSET_1, MEMBERED, STRUCT_0, XREAL_0, ANALMETR;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1;
theorems GEOMTRAP, RELAT_1, RLVECT_1, ANALOAF, ANALMETR, ZFMISC_1, XCMPLX_0,
XCMPLX_1, XREAL_1, XTUPLE_0;
schemes RELSET_1;
begin
reserve V for RealLinearSpace,
u,u1,u2,v,v1,v2,w,w1,x,y for VECTOR of V,
a,a1,a2,b,b1,b2,c1,c2,n,k1,k2 for Real;
Lm1: v1 = b1*x + b2*y & v2 = c1*x + c2*y implies
v1 + v2 = (b1 + c1)*x + (b2 + c2)*y & v1 - v2 = (b1 - c1)*x + (b2 - c2)*y
proof
assume that
A1: v1 = b1*x + b2*y and
A2: v2 = c1*x + c2*y;
thus v1 + v2 = ((b1*x + b2*y) + c1*x) + c2*y by A1,A2,RLVECT_1:def 3
.= ((b1*x + c1*x) + b2*y) + c2*y by RLVECT_1:def 3
.= ((b1 + c1)*x + b2*y) + c2*y by RLVECT_1:def 6
.= (b1 + c1)*x + (b2*y + c2*y) by RLVECT_1:def 3
.= (b1 + c1)*x + (b2 + c2)*y by RLVECT_1:def 6;
thus v1 - v2 = (b1*x + b2*y)+(-(c1*x) + -(c2*y)) by A1,A2,RLVECT_1:31
.= (b1*x + b2*y)+(c1*(-x) + -(c2*y)) by RLVECT_1:25
.= (b1*x + b2*y)+(c1*(-x) + c2*(-y)) by RLVECT_1:25
.= (b1*x + b2*y)+((-c1)*x + c2*(-y)) by RLVECT_1:24
.= (b1*x + b2*y)+((-c1)*x + (-c2)*y) by RLVECT_1:24
.= ((b1*x + b2*y) + (-c1)*x) + (-c2)*y by RLVECT_1:def 3
.= ((b1*x + (-c1)*x) + b2*y) + (-c2)*y by RLVECT_1:def 3
.= ((b1 + (-c1))*x + b2*y) + (-c2)*y by RLVECT_1:def 6
.= (b1 + (-c1))*x + (b2*y + (-c2)*y) by RLVECT_1:def 3
.= (b1 - c1)*x + (b2 + (-c2))*y by RLVECT_1:def 6
.= (b1 - c1)*x + (b2 - c2)*y;
end;
Lm2: v = b1*x + b2*y implies a*v = (a*b1)*x + (a*b2)*y
proof
assume v= b1*x + b2*y;
hence a*v = a*(b1*x) + a*(b2*y) by RLVECT_1:def 5
.= (a*b1)*x + a*(b2*y) by RLVECT_1:def 7
.= (a*b1)*x + (a*b2)*y by RLVECT_1:def 7;
end;
Lm3: Gen x,y & a1*x + a2*y = b1*x + b2*y implies a1=b1 & a2=b2
proof
assume that
A1: Gen x,y and
A2: a1*x+a2*y=b1*x+b2*y;
A3: 0.V = (a1*x+a2*y)-(b1*x+b2*y) by A2,RLVECT_1:15
.= (a1-b1)*x+(a2-b2)*y by Lm1;
then
A4: -b1 + a1 =0 by A1,ANALMETR:def 1;
-b2 + a2 = 0 by A1,A3,ANALMETR:def 1;
hence thesis by A4;
end;
Lm4: Gen x,y implies x<>0.V & y<>0.V
proof
assume
A1: Gen x,y;
A2: x<>0.V
proof
assume
A3: x=0.V;
consider a,b such that
A4: a=1 and
A5: b=0;
a*x+b*y=0.V+0*y by A3,A5,RLVECT_1:10
.=0.V+0.V by RLVECT_1:10
.=0.V by RLVECT_1:4;
hence contradiction by A1,A4,ANALMETR:def 1;
end;
y<>0.V
proof
assume
A6: y=0.V;
consider a,b such that
A7: a=0 and
A8: b=1;
a*x+b*y=0.V+1*0.V by A6,A7,A8,RLVECT_1:10
.=0.V+0.V by RLVECT_1:10
.=0.V by RLVECT_1:4;
hence thesis by A1,A8,ANALMETR:def 1;
end;
hence thesis by A2;
end;
Lm5: Gen x,y implies u = pr1(x,y,u)*x + pr2(x,y,u)*y
proof
assume
A1: Gen x,y;
then consider b such that
A2: u = (pr1(x,y,u))*x + b*y by GEOMTRAP:def 4;
thus thesis by A1,GEOMTRAP:def 5,A2;
end;
Lm6: Gen x,y & u=k1*x+k2*y implies k1=pr1(x,y,u) & k2=pr2(x,y,u)
proof
assume that
A1: Gen x,y and
A2: u=k1*x+k2*y;
u = pr1(x,y,u)*x + pr2(x,y,u)*y by A1,Lm5;
hence thesis by A1,A2,Lm3;
end;
Lm7: Gen x,y implies pr1(x,y,u+v) = pr1(x,y,u)+pr1(x,y,v) &
pr2(x,y,u+v) = pr2(x,y,u)+pr2(x,y,v) & pr1(x,y,u-v) = pr1(x,y,u)-pr1(x,y,v) &
pr2(x,y,u-v) = pr2(x,y,u)-pr2(x,y,v) & pr1(x,y,a*u) = a*pr1(x,y,u) &
pr2(x,y,a*u) = a*pr2(x,y,u)
proof
assume
A1: Gen x,y;
set p1u = pr1(x,y,u), p2u = pr2(x,y,u), p1v = pr1(x,y,v), p2v = pr2(x,y,v);
A2: u = p1u*x + p2u*y by A1,Lm5;
A3: v = p1v*x + p2v*y by A1,Lm5;
then u + v = (p1u*x + p2u*y + p1v*x) + p2v*y by A2,RLVECT_1:def 3
.= ((p1u*x + p1v*x) + p2u*y) + p2v*y by RLVECT_1:def 3
.= (p1u*x + p1v*x) + (p2u*y + p2v*y) by RLVECT_1:def 3
.= (p1u + p1v)*x + (p2u*y + p2v*y) by RLVECT_1:def 6
.= (p1u + p1v)*x + (p2u + p2v)*y by RLVECT_1:def 6;
hence pr1(x,y,u+v) = p1u + p1v & pr2(x,y,u+v) = p2u + p2v by A1,Lm6;
u - v = (p1u - p1v)*x + (p2u - p2v)*y by A2,A3,Lm1;
hence pr1(x,y,u-v) = p1u - p1v & pr2(x,y,u-v) = p2u - p2v by A1,Lm6;
a*u = (a*p1u)*x + (a*p2u)*y by A2,Lm2;
hence thesis by A1,Lm6;
end;
definition
let V,x,y;
let u;
func Ortm(x,y,u) -> VECTOR of V equals
pr1(x,y,u)*x + (-pr2(x,y,u))*y;
correctness;
end;
theorem Th1:
Gen x,y implies Ortm(x,y,u+v)=Ortm(x,y,u)+Ortm(x,y,v)
proof
assume
A1: Gen x,y;
hence Ortm(x,y,u+v)= (pr1(x,y,u)+pr1(x,y,v))*x + (-pr2(x,y,u+v))*y by Lm7
.=(pr1(x,y,u) + pr1(x,y,v))*x + (-(pr2(x,y,u) + pr2(x,y,v)))*y by A1,Lm7
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u) + pr2(x,y,v)))*y
by RLVECT_1:def 6
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (pr2(x,y,u) + pr2(x,y,v))*(-y)
by RLVECT_1:24
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-((pr2(x,y,u) + pr2(x,y,v))*y))
by RLVECT_1:25
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y +pr2(x,y,v)*y))
by RLVECT_1:def 6
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y) + (-(pr2(x,y,v)*y)))
by RLVECT_1:31
.=pr1(x,y,u)*x + (pr1(x,y,v)*x + (-(pr2(x,y,u)*y) + (-(pr2(x,y,v)*y))))
by RLVECT_1:def 3
.=pr1(x,y,u)*x + ((-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y)))
by RLVECT_1:def 3
.=pr1(x,y,u)*x + (-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
by RLVECT_1:def 3
.=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
by RLVECT_1:25
.=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
by RLVECT_1:25
.=pr1(x,y,u)*x + (-pr2(x,y,u))*y + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
by RLVECT_1:24
.=Ortm(x,y,u) + Ortm(x,y,v) by RLVECT_1:24;
end;
theorem Th2:
Gen x,y implies Ortm(x,y,n*u)= n*Ortm(x,y,u)
proof
assume
A1: Gen x,y;
hence Ortm(x,y,n*u)=n*pr1(x,y,u)*x + (-pr2(x,y,n*u))*y by Lm7
.=n*pr1(x,y,u)*x + (-(n*pr2(x,y,u)))*y by A1,Lm7
.=n*pr1(x,y,u)*x + (n*pr2(x,y,u)*(-y)) by RLVECT_1:24
.=n*pr1(x,y,u)*x + (-(n*pr2(x,y,u)*y)) by RLVECT_1:25
.=n*pr1(x,y,u)*x + (-(n*(pr2(x,y,u)*y))) by RLVECT_1:def 7
.=n*pr1(x,y,u)*x + n*(-pr2(x,y,u)*y) by RLVECT_1:25
.=n*(pr1(x,y,u)*x) + n*(-pr2(x,y,u)*y) by RLVECT_1:def 7
.=n*((pr1(x,y,u)*x) + (-pr2(x,y,u)*y)) by RLVECT_1:def 5
.=n*((pr1(x,y,u)*x) + (pr2(x,y,u)*(-y))) by RLVECT_1:25
.=n*Ortm(x,y,u) by RLVECT_1:24;
end;
theorem
Gen x,y implies Ortm(x,y,0.V) = 0.V
proof
assume
A1: Gen x,y;
set u = the VECTOR of V;
thus Ortm(x,y,0.V) = Ortm(x,y,0*u) by RLVECT_1:10
.= 0*Ortm(x,y,u) by A1,Th2
.= 0.V by RLVECT_1:10;
end;
theorem Th4:
Gen x,y implies Ortm(x,y,-u) = -Ortm(x,y,u)
proof
assume
A1: Gen x,y;
then
A2: -u=-(pr1(x,y,u)*x + pr2(x,y,u)*y) by Lm5
.=-(pr1(x,y,u)*x) + (-(pr2(x,y,u)*y)) by RLVECT_1:31
.=pr1(x,y,u)*(-x) + (-(pr2(x,y,u)*y)) by RLVECT_1:25
.=(-pr1(x,y,u))*x + (-(pr2(x,y,u)*y)) by RLVECT_1:24
.=(-pr1(x,y,u))*x + pr2(x,y,u)*(-y) by RLVECT_1:25
.=(-pr1(x,y,u))*x + (-pr2(x,y,u))*y by RLVECT_1:24;
hence Ortm(x,y,-u)=(-pr1(x,y,u))*x + (-pr2(x,y,-u))*y by A1,Lm6
.=(-pr1(x,y,u))*x + (-(-pr2(x,y,u)))*y by A1,A2,Lm6
.=pr1(x,y,u)*(-x) + (-(-pr2(x,y,u)))*y by RLVECT_1:24
.=-(pr1(x,y,u)*x) + (-(-pr2(x,y,u)))*y by RLVECT_1:25
.=-(pr1(x,y,u)*x) + (-pr2(x,y,u))*(-y) by RLVECT_1:24
.=-(pr1(x,y,u)*x) + (-((-pr2(x,y,u))*y)) by RLVECT_1:25
.=-Ortm(x,y,u) by RLVECT_1:31;
end;
theorem Th5:
Gen x,y implies Ortm(x,y,u-v)=Ortm(x,y,u)-Ortm(x,y,v)
proof
assume
A1: Gen x,y;
hence Ortm(x,y,u-v)=Ortm(x,y,u) + Ortm(x,y,(-v)) by Th1
.=Ortm(x,y,u) - Ortm(x,y,v) by A1,Th4;
end;
theorem Th6:
Gen x,y & Ortm(x,y,u)=Ortm(x,y,v) implies u=v
proof
assume that
A1: Gen x,y and
A2: Ortm(x,y,u)=Ortm(x,y,v);
pr1(x,y,u)*x + (-pr2(x,y,u))*y - (pr1(x,y,v)*x + (-pr2(x,y,v))*y)
=0.V by A2,RLVECT_1:15;
then pr1(x,y,u)*x + (-pr2(x,y,u))*y - (pr1(x,y,v)*x) - (-pr2(x,y,v))*y
=0.V by RLVECT_1:27;
then pr1(x,y,u)*x + (-(pr1(x,y,v))*x) + ((-pr2(x,y,u))*y) - (-pr2(x,y,v))*y
=0.V by RLVECT_1:def 3;
then pr1(x,y,u)*x - pr1(x,y,v)*x + ((-pr2(x,y,u))*y - (-pr2(x,y,v))*y)
=0.V by RLVECT_1:def 3;
then (pr1(x,y,u) - pr1(x,y,v))*x + ((-pr2(x,y,u))*y - (-pr2(x,y,v))*y)
=0.V by RLVECT_1:35;
then
A3: (pr1(x,y,u) - pr1(x,y,v))*x + ((-pr2(x,y,u)) - (-pr2(x,y,v)))*y
=0.V by RLVECT_1:35;
then
A4: pr1(x,y,u) - pr1(x,y,v)=0 by A1,ANALMETR:def 1;
(-pr2(x,y,u)) - (-pr2(x,y,v))=0 by A1,A3,ANALMETR:def 1;
hence u=pr1(x,y,v)*x + pr2(x,y,v)*y by A1,A4,Lm5
.=v by A1,Lm5;
end;
theorem Th7:
Gen x,y implies Ortm(x,y,Ortm(x,y,u))=u
proof
assume
A1: Gen x,y;
hence Ortm(x,y,Ortm(x,y,u))=
pr1(x,y,u)*x+(-pr2(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y))*y by GEOMTRAP:def 4
.=pr1(x,y,u)*x+(-(-pr2(x,y,u)))*y by A1,GEOMTRAP:def 5
.=u by A1,Lm5;
end;
theorem Th8:
Gen x,y implies ex v st u=Ortm(x,y,v)
proof
assume
A1: Gen x,y;
take Ortm(x,y,u);
thus thesis by A1,Th7;
end;
definition
let V,x,y;
let u;
func Orte(x,y,u) -> VECTOR of V equals
pr2(x,y,u)*x + (-pr1(x,y,u))*y;
correctness;
end;
theorem Th9:
Gen x,y implies Orte(x,y,-v)= -Orte(x,y,v)
proof
assume
A1: Gen x,y;
then
A2: -v=-(pr1(x,y,v)*x + pr2(x,y,v)*y) by Lm5
.=-(pr1(x,y,v)*x) + (-(pr2(x,y,v)*y)) by RLVECT_1:31
.=pr1(x,y,v)*(-x) + (-(pr2(x,y,v)*y)) by RLVECT_1:25
.=(-pr1(x,y,v))*x + (-(pr2(x,y,v)*y)) by RLVECT_1:24
.=(-pr1(x,y,v))*x + pr2(x,y,v)*(-y) by RLVECT_1:25
.=(-pr1(x,y,v))*x + (-pr2(x,y,v))*y by RLVECT_1:24;
hence Orte(x,y,-v)=(-pr2(x,y,v))*x + (-pr1(x,y,-v))*y by A1,Lm6
.=(-pr2(x,y,v))*x + (-(-pr1(x,y,v)))*y by A1,A2,Lm6
.=pr2(x,y,v)*(-x) + (-(-pr1(x,y,v)))*y by RLVECT_1:24
.=-(pr2(x,y,v)*x) + (-(-pr1(x,y,v)))*y by RLVECT_1:25
.=-(pr2(x,y,v)*x) + (-pr1(x,y,v))*(-y) by RLVECT_1:24
.=-(pr2(x,y,v)*x) + (-((-pr1(x,y,v))*y)) by RLVECT_1:25
.=-Orte(x,y,v) by RLVECT_1:31;
end;
theorem Th10:
Gen x,y implies Orte(x,y,u+v)=Orte(x,y,u) + Orte(x,y,v)
proof
assume
A1: Gen x,y;
hence Orte(x,y,u+v)=(pr2(x,y,u+v))*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y by Lm7
.=(pr2(x,y,u)+pr2(x,y,v))*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y by A1,Lm7
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y
by RLVECT_1:def 6
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (pr1(x,y,u)+pr1(x,y,v))*(-y)
by RLVECT_1:24
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-((pr1(x,y,u)+pr1(x,y,v))*y))
by RLVECT_1:25
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y +pr1(x,y,v)*y))
by RLVECT_1:def 6
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y) +(-(pr1(x,y,v)*y)))
by RLVECT_1:31
.=pr2(x,y,u)*x + (pr2(x,y,v)*x + (-(pr1(x,y,u)*y) +(-(pr1(x,y,v)*y))))
by RLVECT_1:def 3
.=pr2(x,y,u)*x + (-(pr1(x,y,u)*y) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y))))
by RLVECT_1:def 3
.=pr2(x,y,u)*x + (-(pr1(x,y,u)*y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
by RLVECT_1:def 3
.=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
by RLVECT_1:25
.=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
by RLVECT_1:25
.=pr2(x,y,u)*x + ((-pr1(x,y,u))*y) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
by RLVECT_1:24
.=Orte(x,y,u) + Orte(x,y,v) by RLVECT_1:24;
end;
theorem Th11:
Gen x,y implies Orte(x,y,u-v)=Orte(x,y,u)-Orte(x,y,v)
proof
assume
A1: Gen x,y;
hence Orte(x,y,u-v)=Orte(x,y,u) + Orte(x,y,(-v)) by Th10
.=Orte(x,y,u) - Orte(x,y,v) by A1,Th9;
end;
theorem Th12:
Gen x,y implies Orte(x,y,n*u)=n*Orte(x,y,u)
proof
assume
A1: Gen x,y;
hence Orte(x,y,n*u)=n*pr2(x,y,u)*x + (-pr1(x,y,n*u))*y by Lm7
.=n*pr2(x,y,u)*x + (-(n*pr1(x,y,u)))*y by A1,Lm7
.=n*pr2(x,y,u)*x + (n*pr1(x,y,u))*(-y) by RLVECT_1:24
.=n*pr2(x,y,u)*x + (-(n*pr1(x,y,u)*y)) by RLVECT_1:25
.=n*pr2(x,y,u)*x + (-(n*(pr1(x,y,u)*y))) by RLVECT_1:def 7
.=n*pr2(x,y,u)*x + n*(-(pr1(x,y,u)*y)) by RLVECT_1:25
.=n*(pr2(x,y,u)*x) + n*(-(pr1(x,y,u)*y)) by RLVECT_1:def 7
.=n*(pr2(x,y,u)*x + (-(pr1(x,y,u)*y))) by RLVECT_1:def 5
.=n*(pr2(x,y,u)*x + (pr1(x,y,u)*(-y))) by RLVECT_1:25
.=n*Orte(x,y,u) by RLVECT_1:24;
end;
theorem Th13:
Gen x,y & Orte(x,y,u)=Orte(x,y,v) implies u=v
proof
assume that
A1: Gen x,y and
A2: Orte(x,y,u)=Orte(x,y,v);
pr2(x,y,u)*x + (-pr1(x,y,u))*y - (pr2(x,y,v)*x + (-pr1(x,y,v))*y)
=0.V by A2,RLVECT_1:15;
then pr2(x,y,u)*x + (-pr1(x,y,u))*y - (pr2(x,y,v)*x) - (-pr1(x,y,v))*y
=0.V by RLVECT_1:27;
then pr2(x,y,u)*x + (-(pr2(x,y,v))*x) + ((-pr1(x,y,u))*y) - (-pr1(x,y,v))*y
=0.V by RLVECT_1:def 3;
then pr2(x,y,u)*x - pr2(x,y,v)*x + ((-pr1(x,y,u))*y - (-pr1(x,y,v))*y)
=0.V by RLVECT_1:def 3;
then (pr2(x,y,u) - pr2(x,y,v))*x + ((-pr1(x,y,u))*y - (-pr1(x,y,v))*y)
=0.V by RLVECT_1:35;
then
A3: (pr2(x,y,u) - pr2(x,y,v))*x + ((-pr1(x,y,u)) - (-pr1(x,y,v)))*y
=0.V by RLVECT_1:35;
then
A4: pr2(x,y,u) - pr2(x,y,v)=0 by A1,ANALMETR:def 1;
(-pr1(x,y,u)) - (-pr1(x,y,v))=0 by A1,A3,ANALMETR:def 1;
hence u=pr1(x,y,v)*x + pr2(x,y,v)*y by A1,A4,Lm5
.=v by A1,Lm5;
end;
theorem Th14:
Gen x,y implies Orte(x,y,Orte(x,y,u)) = -u
proof
assume
A1: Gen x,y;
hence Orte(x,y,Orte(x,y,u))=(-pr1(x,y,u))*x+
(-pr1(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y))*y by GEOMTRAP:def 5
.=(-pr1(x,y,u))*x+(-pr2(x,y,u))*y by A1,GEOMTRAP:def 4
.=pr1(x,y,u)*(-x)+(-pr2(x,y,u))*y by RLVECT_1:24
.=-(pr1(x,y,u)*x)+(-pr2(x,y,u))*y by RLVECT_1:25
.=-(pr1(x,y,u)*x)+pr2(x,y,u)*(-y) by RLVECT_1:24
.=-(pr1(x,y,u)*x)+(-(pr2(x,y,u)*y)) by RLVECT_1:25
.=-(pr1(x,y,u)*x+pr2(x,y,u)*y) by RLVECT_1:31
.=-u by A1,Lm5;
end;
theorem Th15:
Gen x,y implies ex v st Orte(x,y,v) = u
proof
assume
A1: Gen x,y;
take v= -Orte(x,y,u);
thus Orte(x,y,v) = -Orte(x,y,Orte(x,y,u)) by A1,Th9
.= -(-u) by A1,Th14
.= u by RLVECT_1:17;
end;
definition
let V;
let x,y,u,v,u1,v1;
pred u,v,u1,v1 are_COrte_wrt x,y means
Orte(x,y,u),Orte(x,y,v) // u1,v1;
pred u,v,u1,v1 are_COrtm_wrt x,y means
Ortm(x,y,u),Ortm(x,y,v) // u1,v1;
end;
theorem Th16:
Gen x,y implies (u,v // u1,v1 implies
Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u1),Orte(x,y,v1))
proof
assume
A1: Gen x,y;
assume
A2: u,v // u1,v1;
now
assume that
A3: u<>v and
A4: u1<>v1;
consider a,b such that
A5: 0<a and
A6: 0<b and
A7: a*(v-u)=b*(v1-u1) by A2,A3,A4,ANALOAF:def 1;
a*(Orte(x,y,v)-Orte(x,y,u)) = a*(Orte(x,y,v-u)) by A1,Th11
.= Orte(x,y,b*(v1-u1)) by A1,A7,Th12
.= b*(Orte(x,y,v1-u1)) by A1,Th12
.=b*(Orte(x,y,v1)-Orte(x,y,u1)) by A1,Th11;
hence thesis by A5,A6,ANALOAF:def 1;
end;
hence thesis by ANALOAF:9;
end;
theorem Th17:
Gen x,y implies (u,v // u1,v1 implies
Ortm(x,y,u),Ortm(x,y,v) // Ortm(x,y,u1),Ortm(x,y,v1))
proof
assume
A1: Gen x,y;
assume
A2: u,v // u1,v1;
now
assume
A3: u<>v;
now
assume u1<>v1;
then consider a,b such that
A4: 0<a and
A5: 0<b and
A6: a*(v-u)=b*(v1-u1) by A2,A3,ANALOAF:def 1;
a*(Ortm(x,y,v)-Ortm(x,y,u)) = a*(Ortm(x,y,v-u)) by A1,Th5
.= Ortm(x,y,b*(v1-u1)) by A1,A6,Th2
.= b*(Ortm(x,y,v1-u1)) by A1,Th2
.=b*(Ortm(x,y,v1)-Ortm(x,y,u1)) by A1,Th5;
hence thesis by A4,A5,ANALOAF:def 1;
end;
hence thesis by ANALOAF:9;
end;
hence thesis by ANALOAF:9;
end;
theorem Th18:
Gen x,y implies (u,u1,v,v1 are_COrte_wrt x,y implies
v,v1,u1,u are_COrte_wrt x,y)
proof
assume
A1: Gen x,y;
assume u,u1,v,v1 are_COrte_wrt x,y;
then Orte(x,y,u),Orte(x,y,u1) // v,v1;
then v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:12;
then Orte(x,y,v),Orte(x,y,v1) //
Orte(x,y,Orte(x,y,u)),Orte(x,y,Orte(x,y,u1)) by A1,Th16;
then Orte(x,y,v),Orte(x,y,v1) // -u,Orte(x,y,Orte(x,y,u1)) by A1,Th14;
then Orte(x,y,v),Orte(x,y,v1) // -u,-u1 by A1,Th14;
then
A2: -u,-u1 // Orte(x,y,v),Orte(x,y,v1) by ANALOAF:12;
-u1-(-u)=u+(-u1) by RLVECT_1:17
.=u-u1;
then
A3: -u,-u1 // u1,u by ANALOAF:15;
A4: -u<>-u1 implies thesis by A2,A3,ANALOAF:11;
now
assume -u=-u1;
then u=-(-u1) by RLVECT_1:17
.= u1 by RLVECT_1:17;
then Orte(x,y,v),Orte(x,y,v1) // u1,u by ANALOAF:9;
hence thesis;
end;
hence thesis by A4;
end;
theorem Th19:
Gen x,y implies (u,u1,v,v1 are_COrtm_wrt x,y implies
v,v1,u,u1 are_COrtm_wrt x,y)
proof
assume
A1: Gen x,y;
assume u,u1,v,v1 are_COrtm_wrt x,y;
then Ortm(x,y,u),Ortm(x,y,u1) // v,v1;
then v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:12;
then Ortm(x,y,v),Ortm(x,y,v1) //
Ortm(x,y,Ortm(x,y,u)),Ortm(x,y,Ortm(x,y,u1)) by A1,Th17;
then Ortm(x,y,v),Ortm(x,y,v1) // u,Ortm(x,y,Ortm(x,y,u1)) by A1,Th7;
then Ortm(x,y,v),Ortm(x,y,v1) // u,u1 by A1,Th7;
hence thesis;
end;
theorem Th20:
u,u,v,w are_COrte_wrt x,y
by ANALOAF:9;
theorem
u,u,v,w are_COrtm_wrt x,y
by ANALOAF:9;
theorem
u,v,w,w are_COrte_wrt x,y
by ANALOAF:9;
theorem
u,v,w,w are_COrtm_wrt x,y
by ANALOAF:9;
theorem Th24:
Gen x,y implies u,v,Orte(x,y,u),Orte(x,y,v) are_Ort_wrt x,y
proof
assume
A1: Gen x,y;
set w = Orte(x,y,v) - Orte(x,y,u);
A2: w = Orte(x,y,v-u) by A1,Th11
.= pr2(x,y,v-u)*x + (-pr1(x,y,v-u))*y;
PProJ(x,y,v-u,w) = pr1(x,y,v-u)*pr1(x,y,w) + pr2(x,y,v-u)*pr2(x,y,w)
by GEOMTRAP:def 6
.= pr1(x,y,v-u)*pr2(x,y,v-u) + pr2(x,y,v-u)*pr2(x,y,w)
by A1,A2,Lm6
.= pr1(x,y,v-u)*pr2(x,y,v-u) + (-pr1(x,y,v-u))*pr2(x,y,v-u) by A1,A2,Lm6
.= 0;
then v-u,w are_Ort_wrt x,y by A1,GEOMTRAP:32;
hence thesis by ANALMETR:def 3;
end;
theorem
u,v,Orte(x,y,u),Orte(x,y,v) are_COrte_wrt x,y by ANALOAF:8;
theorem
u,v,Ortm(x,y,u),Ortm(x,y,v) are_COrtm_wrt x,y by ANALOAF:8;
theorem
Gen x,y implies (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y)
proof
assume
A1: Gen x,y;
A2: u,v // u1,v1 implies ex u2,v2 st u2<>v2 &
u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y
proof
assume
A3: u,v // u1,v1;
A4: now
assume that
A5: u=v and
A6: u1=v1;
take u2=0.V,v2=x;
A7: Orte(x,y,u2),Orte(x,y,v2) // u,v by A5,ANALOAF:9;
Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A6,ANALOAF:9;
then
A8: u2,v2,u1,v1 are_COrte_wrt x,y;
A9: u2,v2,u,v are_COrte_wrt x,y by A7;
u2<>v2 by A1,Lm4;
hence thesis by A8,A9;
end;
A10: now
assume
A11: u<>v;
consider u2 such that
A12: Orte(x,y,u2)=u by A1,Th15;
consider v2 such that
A13: Orte(x,y,v2)=v by A1,Th15;
Orte(x,y,u2),Orte(x,y,v2) // u,v by A12,A13,ANALOAF:8;
then
A14: u2,v2,u,v are_COrte_wrt x,y;
u2,v2,u1,v1 are_COrte_wrt x,y by A3,A12,A13;
hence thesis by A11,A12,A13,A14;
end;
now
assume
A15: u1<>v1;
consider u2 such that
A16: Orte(x,y,u2)=u1 by A1,Th15;
consider v2 such that
A17: Orte(x,y,v2)=v1 by A1,Th15;
Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A16,A17,ANALOAF:8;
then
A18: u2,v2,u1,v1 are_COrte_wrt x,y;
Orte(x,y,u2),Orte(x,y,v2) // u,v by A3,A16,A17,ANALOAF:12;
then u2,v2,u,v are_COrte_wrt x,y;
hence thesis by A15,A16,A17,A18;
end;
hence thesis by A4,A10;
end;
(ex u2,v2 st u2<>v2 & u2,v2,u,v are_COrte_wrt x,y &
u2,v2,u1,v1 are_COrte_wrt x,y) implies u,v // u1,v1
by A1,Th13,ANALOAF:11;
hence thesis by A2;
end;
theorem
Gen x,y implies (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y)
proof
assume
A1: Gen x,y;
A2: u,v // u1,v1 implies ex u2,v2 st u2<>v2 &
u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y
proof
assume
A3: u,v // u1,v1;
A4: now
assume that
A5: u=v and
A6: u1=v1;
take u2=0.V,v2=x;
A7: Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A5,ANALOAF:9;
Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A6,ANALOAF:9;
then
A8: u2,v2,u1,v1 are_COrtm_wrt x,y;
A9: u2,v2,u,v are_COrtm_wrt x,y by A7;
u2<>v2 by A1,Lm4;
hence thesis by A8,A9;
end;
A10: now
assume
A11: u<>v;
consider u2 such that
A12: Ortm(x,y,u2)=u by A1,Th8;
consider v2 such that
A13: Ortm(x,y,v2)=v by A1,Th8;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A12,A13,ANALOAF:8;
then
A14: u2,v2,u,v are_COrtm_wrt x,y;
u2,v2,u1,v1 are_COrtm_wrt x,y by A3,A12,A13;
hence thesis by A11,A12,A13,A14;
end;
now
assume
A15: u1<>v1;
consider u2 such that
A16: Ortm(x,y,u2)=u1 by A1,Th8;
consider v2 such that
A17: Ortm(x,y,v2)=v1 by A1,Th8;
Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A16,A17,ANALOAF:8;
then
A18: u2,v2,u1,v1 are_COrtm_wrt x,y;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A3,A16,A17,ANALOAF:12;
then u2,v2,u,v are_COrtm_wrt x,y;
hence thesis by A15,A16,A17,A18;
end;
hence thesis by A4,A10;
end;
(ex u2,v2 st u2<>v2 & u2,v2,u,v are_COrtm_wrt x,y &
u2,v2,u1,v1 are_COrtm_wrt x,y) implies u,v // u1,v1
by A1,Th6,ANALOAF:11;
hence thesis by A2;
end;
theorem
Gen x,y implies (u,v,u1,v1 are_Ort_wrt x,y iff
u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y)
proof
assume
A1: Gen x,y;
A2: now
assume u=v;
then v-u=0.V by RLVECT_1:15;
then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:5;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
end;
now
assume
A3: u<>v;
set u2=Orte(x,y,u),v2=Orte(x,y,v);
A4: v-u<>0.V by A3,RLVECT_1:21;
u,v,u2,v2 are_Ort_wrt x,y by A1,Th24;
then
A5: v-u,v2-u2 are_Ort_wrt x,y by ANALMETR:def 3;
A6: now
assume u,v,u1,v1 are_Ort_wrt x,y;
then v-u,v1-u1 are_Ort_wrt x,y by ANALMETR:def 3;
then ex a,b st
a*(v2-u2)=b*(v1-u1) & (a<>0 or b<>0) by A1,A4,A5,ANALMETR:9;
then u2,v2 // u1,v1 or u2,v2 // v1,u1 by ANALMETR:14;
hence u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y;
end;
now
assume u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y;
then u2,v2 // u1,v1 or u2,v2 // v1,u1;
then consider a,b such that
A7: a*(v2-u2)=b*(v1-u1) and
A8: a<>0 or b<>0 by ANALMETR:14;
A9: now
assume
A10: b=0;
then 0.V = a*(v2-u2) by A7,RLVECT_1:10;
then v2-u2=0.V by A8,A10,RLVECT_1:11;
then v2=u2 by RLVECT_1:21;
then u=v by A1,Th13;
then v-u=0.V by RLVECT_1:15;
then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:5;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
end;
now
assume
A11: b<>0;
((b")*a)*(v2-u2)=(b")*(b*(v1-u1)) by A7,RLVECT_1:def 7;
then ((b")*a)*(v2-u2)=((b")*b)*(v1-u1) by RLVECT_1:def 7;
then ((b")*a)*(v2-u2)=1*(v1-u1) by A11,XCMPLX_0:def 7;
then v1-u1=((b")*a)*(v2-u2) by RLVECT_1:def 8;
then v-u,v1-u1 are_Ort_wrt x,y by A5,ANALMETR:7;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
end;
hence u,v,u1,v1 are_Ort_wrt x,y by A9;
end;
hence thesis by A6;
end;
hence thesis by A2,Th20;
end;
theorem
Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y
implies u=v or u1=v1
proof
assume
A1: Gen x,y;
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,u1 are_COrte_wrt x,y;
assume that
A4: u<>v and
A5: u1<>v1;
A6: Orte(x,y,u),Orte(x,y,v) // u1,v1 by A2;
A7: Orte(x,y,u),Orte(x,y,v) // v1,u1 by A3;
Orte(x,y,u) <> Orte(x,y,v) by A1,A4,Th13;
hence contradiction by A5,A6,A7,ANALOAF:10,11;
end;
theorem
Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y
implies u=v or u1=v1
proof
assume
A1: Gen x,y;
assume that
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,v1,u1 are_COrtm_wrt x,y;
assume that
A4: u<>v and
A5: u1<>v1;
A6: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 by A2;
A7: Ortm(x,y,u),Ortm(x,y,v) // v1,u1 by A3;
Ortm(x,y,u) <> Ortm(x,y,v) by A1,A4,Th6;
hence contradiction by A5,A6,A7,ANALOAF:10,11;
end;
theorem
Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y
implies u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y
proof
assume that
A1: Gen x,y and
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,u1,w are_COrte_wrt x,y;
A4: Orte(x,y,u),Orte(x,y,v) // u1,v1 by A2;
A5: Orte(x,y,u),Orte(x,y,v) // u1,w by A3;
now
assume
A6: u<>v;
now
assume that
A7: u1<>v1 and
A8: u1<>w;
A9: u1,v1 // u1,w by A1,A4,A5,A6,Th13,ANALOAF:11;
A10: now
assume
A11: u1,v1 // v1,w;
u1,v1 // Orte(x,y,u),Orte(x,y,v) by A4,ANALOAF:12;
then Orte(x,y,u),Orte(x,y,v) // v1,w by A7,A11,ANALOAF:11;
hence thesis;
end;
now
assume
A12: u1,w // w,v1;
u1,w // Orte(x,y,u),Orte(x,y,v) by A5,ANALOAF:12;
then Orte(x,y,u),Orte(x,y,v) // w,v1 by A8,A12,ANALOAF:11;
hence thesis;
end;
hence thesis by A9,A10,ANALOAF:14;
end;
hence thesis by A2,A3;
end;
hence thesis by Th20;
end;
theorem
Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y
implies u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y
proof
assume that
A1: Gen x,y and
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,u1,w are_COrtm_wrt x,y;
A4: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 by A2;
A5: Ortm(x,y,u),Ortm(x,y,v) // u1,w by A3;
A6: now
assume that
A7: u<>v and
A8: u1<>v1;
u1,v1 // u1,w by A1,A4,A5,A7,Th6,ANALOAF:11;
then
A9: u1,v1 // v1,w or u1,w // w,v1 by ANALOAF:14;
now
assume
A10: u1<>w;
A11: u1,v1 // Ortm(x,y,u),Ortm(x,y,v) by A4,ANALOAF:12;
u1,w // Ortm(x,y,u),Ortm(x,y,v) by A5,ANALOAF:12;
then Ortm(x,y,u),Ortm(x,y,v) // v1,w or
Ortm(x,y,u),Ortm(x,y,v) // w,v1 by A8,A9,A10,A11,ANALOAF:11;
hence thesis;
end;
hence thesis by A2;
end;
u=v implies thesis by ANALOAF:9;
hence thesis by A3,A6;
end;
theorem
u,v,u1,v1 are_COrte_wrt x,y implies v,u,v1,u1 are_COrte_wrt x,y
by ANALOAF:12;
theorem
u,v,u1,v1 are_COrtm_wrt x,y implies v,u,v1,u1 are_COrtm_wrt x,y
by ANALOAF:12;
theorem
Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y
implies u,v,u1,w are_COrte_wrt x,y
proof
assume
A1: Gen x,y;
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,w are_COrte_wrt x,y;
A4: Orte(x,y,u),Orte(x,y,v) // u1,v1 by A2;
A5: Orte(x,y,u),Orte(x,y,v) // v1,w by A3;
A6: u1,v1 // Orte(x,y,u),Orte(x,y,v) by A4,ANALOAF:12;
A7: now
assume u<>v;
then u1,v1 // v1,w by A1,A4,A5,Th13,ANALOAF:11;
then
A8: u1,v1 // u1,w by ANALOAF:13;
u1<>v1 implies thesis by A6,A8,ANALOAF:11;
hence thesis by A3;
end;
u=v implies thesis by ANALOAF:9;
hence thesis by A7;
end;
theorem
Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y
implies u,v,u1,w are_COrtm_wrt x,y
proof
assume
A1: Gen x,y;
assume that
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,v1,w are_COrtm_wrt x,y;
A4: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 by A2;
A5: Ortm(x,y,u),Ortm(x,y,v) // v1,w by A3;
A6: u1,v1 // Ortm(x,y,u),Ortm(x,y,v) by A4,ANALOAF:12;
A7: now
assume u<>v;
then u1,v1 // v1,w by A1,A4,A5,Th6,ANALOAF:11;
then
A8: u1,v1 // u1,w by ANALOAF:13;
u1<>v1 implies thesis by A6,A8,ANALOAF:11;
hence thesis by A3;
end;
u=v implies thesis by ANALOAF:9;
hence thesis by A7;
end;
theorem
Gen x,y implies for u,v,w ex u1 st w<>u1 & w,u1,u,v are_COrte_wrt x,y
proof
assume
A1: Gen x,y;
let u,v,w;
A2: now
assume
A3: u=v;
take u1=w+x;
Orte(x,y,w),Orte(x,y,u1) // u,v by A3,ANALOAF:9;
then
A4: w,u1,u,v are_COrte_wrt x,y;
now
assume w=u1;
then x=0.V by RLVECT_1:9;
hence contradiction by A1,Lm4;
end;
hence thesis by A4;
end;
now
assume
A5: u<>v;
consider u2 such that
A6: Orte(x,y,u2)=u by A1,Th15;
consider v2 such that
A7: Orte(x,y,v2)=v by A1,Th15;
take u1= (v2+w)-u2;
u2,v2 // w,u1 by ANALOAF:16;
then w,u1 // u2,v2 by ANALOAF:12;
then Orte(x,y,w),Orte(x,y,u1) // Orte(x,y,u2),Orte(x,y,v2) by A1,Th16;
then
A8: w,u1,u,v are_COrte_wrt x,y by A6,A7;
now
assume w=u1;
then w= w+(v2-u2) by RLVECT_1:def 3;
then v2-u2=0.V by RLVECT_1:9;
hence contradiction by A5,A6,A7,RLVECT_1:21;
end;
hence thesis by A8;
end;
hence thesis by A2;
end;
theorem
Gen x,y implies for u,v,w ex u1 st w<>u1 & w,u1,u,v are_COrtm_wrt x,y
proof
assume
A1: Gen x,y;
let u,v,w;
A2: now
assume
A3: u=v;
take u1=w+x;
Ortm(x,y,w),Ortm(x,y,u1) // u,v by A3,ANALOAF:9;
then
A4: w,u1,u,v are_COrtm_wrt x,y;
now
assume w=u1;
then x=0.V by RLVECT_1:9;
hence contradiction by A1,Lm4;
end;
hence thesis by A4;
end;
now
assume
A5: u<>v;
consider u2 such that
A6: Ortm(x,y,u2)=u by A1,Th8;
consider v2 such that
A7: Ortm(x,y,v2)=v by A1,Th8;
take u1= (v2+w)-u2;
u2,v2 // w,u1 by ANALOAF:16;
then w,u1 // u2,v2 by ANALOAF:12;
then Ortm(x,y,w),Ortm(x,y,u1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
then
A8: w,u1,u,v are_COrtm_wrt x,y by A6,A7;
now
assume w=u1;
then w= w+(v2-u2) by RLVECT_1:def 3;
then v2-u2=0.V by RLVECT_1:9;
hence contradiction by A5,A6,A7,RLVECT_1:21;
end;
hence thesis by A8;
end;
hence thesis by A2;
end;
theorem Th40:
Gen x,y implies for u,v,w ex u1 st w<>u1 & u,v,w,u1 are_COrte_wrt x,y
proof
assume
A1: Gen x,y;
let u,v,w;
A2: now
assume
A3: u=v;
take u1=w+x;
Orte(x,y,u),Orte(x,y,v) // w,u1 by A3,ANALOAF:9;
then
A4: u,v,w,u1 are_COrte_wrt x,y;
now
assume w=u1;
then x=0.V by RLVECT_1:9;
hence contradiction by A1,Lm4;
end;
hence thesis by A4;
end;
now
assume
A5: u<>v;
consider u2 such that
A6: Orte(x,y,u2)=u by A1,Th15;
consider v2 such that
A7: Orte(x,y,v2)=v by A1,Th15;
take u1= (u2+w)-v2;
v2,u2 // w,u1 by ANALOAF:16;
then Orte(x,y,v2),Orte(x,y,u2) // Orte(x,y,w),Orte(x,y,u1) by A1,Th16;
then Orte(x,y,w),Orte(x,y,u1) // v,u by A6,A7,ANALOAF:12;
then Orte(x,y,u1),Orte(x,y,w) // u,v by ANALOAF:12;
then
A8: u1,w,u,v are_COrte_wrt x,y;
now
assume w=u1;
then w= w+(u2-v2) by RLVECT_1:def 3;
then u2-v2=0.V by RLVECT_1:9;
hence contradiction by A5,A6,A7,RLVECT_1:21;
end;
hence thesis by A1,A8,Th18;
end;
hence thesis by A2;
end;
theorem Th41:
Gen x,y implies for u,v,w ex u1 st w<>u1 & u,v,w,u1 are_COrtm_wrt x,y
proof
assume
A1: Gen x,y;
let u,v,w;
A2: now
assume
A3: u=v;
take u1=w+x;
Ortm(x,y,w),Ortm(x,y,u1) // u,v by A3,ANALOAF:9;
then
A4: w,u1,u,v are_COrtm_wrt x,y;
w<>u1
proof
assume w=u1;
then x=0.V by RLVECT_1:9;
hence contradiction by A1,Lm4;
end;
hence thesis by A1,A4,Th19;
end;
now
assume
A5: u<>v;
consider u2 such that
A6: Ortm(x,y,u2)=u by A1,Th8;
consider v2 such that
A7: Ortm(x,y,v2)=v by A1,Th8;
take u1= (v2+w)-u2;
u2,v2 // w,u1 by ANALOAF:16;
then w,u1 // u2,v2 by ANALOAF:12;
then Ortm(x,y,w),Ortm(x,y,u1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
then
A8: w,u1,u,v are_COrtm_wrt x,y by A6,A7;
w<>u1
proof
assume w=u1;
then w= w+(v2-u2) by RLVECT_1:def 3;
then v2-u2=0.V by RLVECT_1:9;
hence contradiction by A5,A6,A7,RLVECT_1:21;
end;
hence thesis by A1,A8,Th19;
end;
hence thesis by A2;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y &
w,w1,u2,v2 are_COrte_wrt x,y implies
w=w1 or v=v1 or u,u1,u2,v2 are_COrte_wrt x,y
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: w,w1,v,v1 are_COrte_wrt x,y and
A4: w,w1,u2,v2 are_COrte_wrt x,y;
Orte(x,y,u),Orte(x,y,u1) // v,v1 by A2;
then
A5: v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:12;
Orte(x,y,w),Orte(x,y,w1) // v,v1 by A3;
then
A6: v,v1 // Orte(x,y,w),Orte(x,y,w1) by ANALOAF:12;
A7: Orte(x,y,w),Orte(x,y,w1) // u2,v2 by A4;
now
assume that
A8: w<>w1 and
A9: v<>v1;
Orte(x,y,w),Orte(x,y,w1) // Orte(x,y,u),Orte(x,y,u1)
by A5,A6,A9,ANALOAF:11;
then Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A1,A7,A8,Th13,ANALOAF:11;
hence u,u1,u2,v2 are_COrte_wrt x,y;
end;
hence thesis;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y &
w,w1,u2,v2 are_COrtm_wrt x,y implies
w=w1 or v=v1 or u,u1,u2,v2 are_COrtm_wrt x,y
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: w,w1,v,v1 are_COrtm_wrt x,y and
A4: w,w1,u2,v2 are_COrtm_wrt x,y;
Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by A2;
then
A5: v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:12;
Ortm(x,y,w),Ortm(x,y,w1) // v,v1 by A3;
then
A6: v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:12;
A7: Ortm(x,y,w),Ortm(x,y,w1) // u2,v2 by A4;
now
assume that
A8: w<>w1 and
A9: v<>v1;
Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
by A5,A6,A9,ANALOAF:11;
then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A1,A7,A8,Th6,ANALOAF:11;
hence u,u1,u2,v2 are_COrtm_wrt x,y;
end;
hence thesis;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y
& u2,v2,w,w1 are_COrte_wrt x,y implies
u,u1,u2,v2 are_COrte_wrt x,y or v=v1 or w=w1
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: v,v1,w,w1 are_COrte_wrt x,y and
A4: u2,v2,w,w1 are_COrte_wrt x,y;
v,v1,u1,u are_COrte_wrt x,y by A1,A2,Th18;
then
A5: Orte(x,y,v),Orte(x,y,v1) // u1,u;
Orte(x,y,v),Orte(x,y,v1) // w,w1 by A3;
then
A6: w,w1 // Orte(x,y,v),Orte(x,y,v1) by ANALOAF:12;
Orte(x,y,u2),Orte(x,y,v2) // w,w1 by A4;
then
A7: w,w1 // Orte(x,y,u2),Orte(x,y,v2) by ANALOAF:12;
now
assume that
A8: w<>w1 and
A9: v<>v1;
Orte(x,y,v),Orte(x,y,v1) // Orte(x,y,u2),Orte(x,y,v2)
by A6,A7,A8,ANALOAF:11;
then Orte(x,y,u2),Orte(x,y,v2) // u1,u by A1,A5,A9,Th13,ANALOAF:11;
then Orte(x,y,v2),Orte(x,y,u2) // u,u1 by ANALOAF:12;
then v2,u2,u,u1 are_COrte_wrt x,y;
hence thesis by A1,Th18;
end;
hence thesis;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y
& u2,v2,w,w1 are_COrtm_wrt x,y implies
u,u1,u2,v2 are_COrtm_wrt x,y or v=v1 or w=w1
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: u2,v2,w,w1 are_COrtm_wrt x,y;
Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by A2;
then
A5: v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:12;
w,w1,v,v1 are_COrtm_wrt x,y by A1,A3,Th19;
then Ortm(x,y,w),Ortm(x,y,w1) // v,v1;
then
A6: v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:12;
w,w1,u2,v2 are_COrtm_wrt x,y by A1,A4,Th19;
then
A7: Ortm(x,y,w),Ortm(x,y,w1) // u2,v2;
now
assume that
A8: w<>w1 and
A9: v<>v1;
Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
by A5,A6,A9,ANALOAF:11;
then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A1,A7,A8,Th6,ANALOAF:11;
hence thesis;
end;
hence thesis;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y
& u,u1,u2,v2 are_COrte_wrt x,y implies
u2,v2,w,w1 are_COrte_wrt x,y or v=v1 or u=u1
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: v,v1,w,w1 are_COrte_wrt x,y and
A4: u,u1,u2,v2 are_COrte_wrt x,y;
A5: Orte(x,y,u),Orte(x,y,u1) // v,v1 by A2;
A6: Orte(x,y,v),Orte(x,y,v1) // w,w1 by A3;
A7: Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A4;
now
assume that
A8: u<>u1 and
A9: v<>v1;
v,v1 // u2,v2 by A1,A5,A7,A8,Th13,ANALOAF:11;
then Orte(x,y,v),Orte(x,y,v1) // Orte(x,y,u2),Orte(x,y,v2) by A1,Th16;
then Orte(x,y,u2),Orte(x,y,v2) // w,w1 by A1,A6,A9,Th13,ANALOAF:11;
hence thesis;
end;
hence thesis;
end;
theorem
Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y
& u,u1,u2,v2 are_COrtm_wrt x,y implies
u2,v2,w,w1 are_COrtm_wrt x,y or v=v1 or u=u1
proof
assume
A1: Gen x,y;
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: u,u1,u2,v2 are_COrtm_wrt x,y;
A5: Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by A2;
A6: Ortm(x,y,v),Ortm(x,y,v1) // w,w1 by A3;
A7: Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A4;
now
assume that
A8: u<>u1 and
A9: v<>v1;
v,v1 // u2,v2 by A1,A5,A7,A8,Th6,ANALOAF:11;
then Ortm(x,y,v),Ortm(x,y,v1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
then Ortm(x,y,u2),Ortm(x,y,v2) // w,w1 by A1,A6,A9,Th6,ANALOAF:11;
hence thesis;
end;
hence thesis;
end;
theorem
Gen x,y implies for v,w,u1,v1,w1 holds not v,v1,w,u1 are_COrte_wrt x,y &
not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y
implies ex u2 st
(v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y) &
(u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y)
proof
assume
A1: Gen x,y;
let v,w,u1,v1,w1;
consider u such that
A2: v<>u and
A3: v,v1,v,u are_COrte_wrt x,y by A1,Th40;
assume that
A4: not v,v1,w,u1 are_COrte_wrt x,y and
A5: not v,v1,u1,w are_COrte_wrt x,y and
A6: u1,w1,u1,w are_COrte_wrt x,y;
A7: not Orte(x,y,v),Orte(x,y,v1) // w,u1 by A4;
A8: Orte(x,y,v),Orte(x,y,v1) // v,u by A3;
A9: Orte(x,y,u1),Orte(x,y,w1) // u1,w by A6;
A10: not Orte(x,y,v),Orte(x,y,v1) // u1,w by A5;
A11: v,u // Orte(x,y,v),Orte(x,y,v1) by A8,ANALOAF:12;
A12: u1,w // Orte(x,y,u1),Orte(x,y,w1) by A9,ANALOAF:12;
A13: u1<>w by A7,ANALOAF:9;
A14: not v,u // u1,w by A2,A10,A11,ANALOAF:11;
A15: not v,u // w,u1 by A2,A7,A11,ANALOAF:11;
Gen x,y implies ex u,v st for w ex a,b st a*u + b*v=w
proof
assume
A16: Gen x,y;
take x,y;
thus thesis by A16,ANALMETR:def 1;
end;
then consider u2 such that
A17: v,u // v,u2 or v,u // u2,v and
A18: u1,w // u1,u2 or u1,w // u2,u1 by A1,A14,A15,ANALOAF:21;
Orte(x,y,v),Orte(x,y,v1) // v,u2 or Orte(x,y,v),Orte(x,y,v1) // u2,v
by A2,A11,A17,ANALOAF:11;
then
A19: v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y;
Orte(x,y,u1),Orte(x,y,w1) // u1,u2 or Orte(x,y,u1),Orte(x,y,w1) // u2,u1
by A12,A13,A18,ANALOAF:11;
then u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y;
hence thesis by A19;
end;
theorem
Gen x,y implies ex u,v,w st (u,v,u,w are_COrte_wrt x,y &
for v1,w1 st v1,w1,u,v are_COrte_wrt x,y holds
(not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y
or v1=w1))
proof
assume
A1: Gen x,y;
Gen x,y implies ex u,v st u<>v
proof
assume
A2: Gen x,y;
take x,0.V;
thus thesis by A2,Lm4;
end;
then consider u,v such that
A3: u<>v by A1;
take u,v;
consider w such that
A4: w<>u and
A5: u,v,u,w are_COrte_wrt x,y by A1,Th40;
take w;
thus u,v,u,w are_COrte_wrt x,y by A5;
A6: Orte(x,y,u),Orte(x,y,v) // u,w by A5;
let v1,w1;
assume v1,w1,u,v are_COrte_wrt x,y;
then
A7: Orte(x,y,v1),Orte(x,y,w1) // u,v;
now
assume
A8: v1<>w1;
assume v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y;
then Orte(x,y,v1),Orte(x,y,w1) // u,w or
Orte(x,y,v1),Orte(x,y,w1) // w,u;
then u,v // u,w or u,v // w,u by A1,A7,A8,Th13,ANALOAF:11;
then Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u),Orte(x,y,w) or
Orte(x,y,u),Orte(x,y,v) // Orte(x,y,w),Orte(x,y,u) by A1,Th16;
then u,w // Orte(x,y,u),Orte(x,y,w) or u,w // Orte(x,y,w),Orte(x,y,u)
by A1,A3,A6,Th13,ANALOAF:11;
then consider a,b such that
A9: a*(w-u)=b*(Orte(x,y,w)-Orte(x,y,u)) and
A10: a<>0 or b<>0 by ANALMETR:14;
take a,b;
a*(w-u)=b*Orte(x,y,w-u) by A1,A9,Th11;
then
A11: a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=b*Orte(x,y,w-u) by A1,Lm5;
A12: now
assume
A13: a<>0;
A14: pr2(x,y,w-u)<>0
proof
assume
A15: not thesis;
then a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
(b*0)*x + (b*(-pr1(x,y,w-u)))*y by A11,Lm2;
then (a*pr1(x,y,w-u))*x + (a*pr2(x,y,w-u))*y=
(b*0)*x + (b*(-pr1(x,y,w-u)))*y by Lm2;
then a*pr1(x,y,w-u)=0 by A1,Lm3;
then pr1(x,y,w-u)=0 by A13,XCMPLX_1:6;
then w-u=0*x + 0*y by A1,A15,Lm5
.=0.V + 0*y by RLVECT_1:10
.=0.V + 0.V by RLVECT_1:10
.=0.V by RLVECT_1:4;
hence thesis by A4,RLVECT_1:21;
end;
(a"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
a"*(b*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y)) by A11,RLVECT_1:def 7;
then (a"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
(a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 7;
then 1*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
(a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A13,XCMPLX_0:def 7;
then pr1(x,y,w-u)*x + pr2(x,y,w-u)*y=
(a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 8;
then
A16: pr1(x,y,w-u)*x + pr2(x,y,w-u)*y=
(a"*b)*pr2(x,y,w-u)*x + (a"*b)*(-pr1(x,y,w-u))*y by Lm2;
then pr1(x,y,w-u)=(a"*b)*pr2(x,y,w-u) by A1,Lm3;
then
A17: pr2(x,y,w-u)=-((a"*b)*((a"*b)*pr2(x,y,w-u))) by A1,A16,Lm3;
-(pr2(x,y,w-u)"*pr2(x,y,w-u)) = (pr2(x,y,w-u)"*-pr2(x,y,w-u))
.= pr2(x,y,w-u)"*((a"*b)*((a"*b)*pr2(x,y,w-u))) by A17;
then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((a"*b)*(a"*b)) by A14,XCMPLX_0:def 7;
then -1=1*((a"*b)*(a"*b)) by A14,XCMPLX_0:def 7;
hence thesis by XREAL_1:63;
end;
now
assume
A18: b<>0;
A19: pr2(x,y,w-u)<>0
proof
assume
A20: not thesis;
then a*(pr1(x,y,w-u)*x + 0*y)=
(b*0)*x + (b*(-pr1(x,y,w-u)))*y by A11,Lm2;
then (a*pr1(x,y,w-u))*x + (a*0)*y=
(b*0)*x + (b*(-pr1(x,y,w-u)))*y by Lm2;
then b*(-pr1(x,y,w-u))=0 by A1,Lm3;
then -pr1(x,y,w-u)=0 by A18,XCMPLX_1:6;
then w-u=0*x + (-0)*y by A1,A20,Lm5
.=0.V + 0*y by RLVECT_1:10
.=0.V + 0.V by RLVECT_1:10
.=0.V by RLVECT_1:4;
hence thesis by A4,RLVECT_1:21;
end;
b"*(a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y))=
(b"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A11,RLVECT_1:def 7;
then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
(b"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 7;
then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
1*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A18,XCMPLX_0:def 7;
then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y by RLVECT_1:def 8;
then
A21: (b"*a)*pr1(x,y,w-u)*x + (b"*a)*pr2(x,y,w-u)*y=
pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y by Lm2;
then (b"*a)*pr2(x,y,w-u)=-pr1(x,y,w-u) by A1,Lm3;
then
A22: pr2(x,y,w-u)=(b"*a)*(-((b"*a)*pr2(x,y,w-u))) by A1,A21,Lm3;
-(pr2(x,y,w-u)"*pr2(x,y,w-u)) = (pr2(x,y,w-u)"*-pr2(x,y,w-u))
.= pr2(x,y,w-u)"*((b"*a)*((b"*a)*pr2(x,y,w-u))) by A22;
then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((b"*a)*(b"*a)) by A19,XCMPLX_0:def 7;
then -1=1*((b"*a)*(b"*a)) by A19,XCMPLX_0:def 7;
hence thesis by XREAL_1:63;
end;
hence thesis by A10,A12;
end;
hence thesis;
end;
theorem
Gen x,y implies for v,w,u1,v1,w1 holds not v,v1,w,u1 are_COrtm_wrt x,y &
not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y
implies ex u2 st
(v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y) &
(u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y)
proof
assume
A1: Gen x,y;
let v,w,u1,v1,w1;
consider u such that
A2: v<>u and
A3: v,v1,v,u are_COrtm_wrt x,y by A1,Th41;
assume that
A4: not v,v1,w,u1 are_COrtm_wrt x,y and
A5: not v,v1,u1,w are_COrtm_wrt x,y and
A6: u1,w1,u1,w are_COrtm_wrt x,y;
A7: not Ortm(x,y,v),Ortm(x,y,v1) // w,u1 by A4;
A8: Ortm(x,y,v),Ortm(x,y,v1) // v,u by A3;
A9: Ortm(x,y,u1),Ortm(x,y,w1) // u1,w by A6;
A10: not Ortm(x,y,v),Ortm(x,y,v1) // u1,w by A5;
A11: v,u // Ortm(x,y,v),Ortm(x,y,v1) by A8,ANALOAF:12;
A12: u1,w // Ortm(x,y,u1),Ortm(x,y,w1) by A9,ANALOAF:12;
A13: u1<>w by A7,ANALOAF:9;
A14: not v,u // u1,w by A2,A10,A11,ANALOAF:11;
A15: not v,u // w,u1 by A2,A7,A11,ANALOAF:11;
Gen x,y implies ex u,v st for w ex a,b st a*u + b*v=w
proof
assume
A16: Gen x,y;
take x,y;
thus thesis by A16,ANALMETR:def 1;
end;
then consider u2 such that
A17: v,u // v,u2 or v,u // u2,v and
A18: u1,w // u1,u2 or u1,w // u2,u1 by A1,A14,A15,ANALOAF:21;
Ortm(x,y,v),Ortm(x,y,v1) // v,u2 or Ortm(x,y,v),Ortm(x,y,v1) // u2,v
by A2,A11,A17,ANALOAF:11;
then
A19: v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y;
Ortm(x,y,u1),Ortm(x,y,w1) // u1,u2 or Ortm(x,y,u1),Ortm(x,y,w1) // u2,u1
by A12,A13,A18,ANALOAF:11;
then u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y;
hence thesis by A19;
end;
theorem
Gen x,y implies ex u,v,w st (u,v,u,w are_COrtm_wrt x,y &
for v1,w1 holds (v1,w1,u,v are_COrtm_wrt x,y implies
(not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y
or v1=w1)))
proof
assume
A1: Gen x,y;
take u=0*x+0*y,v=1*x+1*y,w=1*x+(-1)*y;
A2: pr1(x,y,u)=0 by A1,Lm6;
A3: pr2(x,y,u)=0 by A1,Lm6;
A4: pr1(x,y,v)=1 by A1,Lm6;
pr2(x,y,v)=1 by A1,Lm6;
then
A5: Ortm(x,y,u),Ortm(x,y,v) // u,w by A2,A3,A4,ANALOAF:8;
for v1,w1 holds (v1,w1,u,v are_COrtm_wrt x,y implies
(not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y
or v1=w1))
proof
let v1,w1;
assume v1,w1,u,v are_COrtm_wrt x,y;
then
A6: Ortm(x,y,v1),Ortm(x,y,w1) // u,v;
now
assume
A7: v1<>w1;
assume v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y;
then Ortm(x,y,v1),Ortm(x,y,w1) // u,w or
Ortm(x,y,v1),Ortm(x,y,w1) // w,u;
then u,v // u,w or u,v // w,u by A1,A6,A7,Th6,ANALOAF:11;
then consider a,b such that
A8: a*(v-u)=b*(w-u) and
A9: a<>0 or b<>0 by ANALMETR:14;
take a,b;
u=0.V+0*y by RLVECT_1:10
.=0.V+0.V by RLVECT_1:10
.=0.V by RLVECT_1:4;
then a*v=b*(w-0.V) by A8,RLVECT_1:13;
then
A10: a*v=b*w by RLVECT_1:13;
A11: now
assume
A12: a<>0;
a"*a*v=a"*(b*w) by A10,RLVECT_1:def 7;
then a"*a*v=a"*b*w by RLVECT_1:def 7;
then 1*v=a"*b*w by A12,XCMPLX_0:def 7;
then 1*v=a"*b*1*x+a"*b*(-1)*y by Lm2;
then
A13: 1*1*x+1*1*y=a"*b*1*x+a"*b*(-1)*y by Lm2;
then a*1=a*(a"*(b*1)) by A1,Lm3;
then
A14: a*1=a*a"*(b*1);
1=a"*b*(-1) by A1,A13,Lm3;
then 1=a"*a*(-1) by A12,A14,XCMPLX_0:def 7;
hence thesis by A12,XCMPLX_0:def 7;
end;
now
assume
A15: b<>0;
b"*a*v=b"*(b*w) by A10,RLVECT_1:def 7;
then b"*a*v=b"*b*w by RLVECT_1:def 7;
then b"*a*v=1*w by A15,XCMPLX_0:def 7;
then b"*a*1*x+b"*a*1*y=1*w by Lm2;
then
A16: b"*a*1*x+b"*a*1*y=1*1*x+1*(-1)*y by Lm2;
then b*1=b*(b"*(a*1)) by A1,Lm3;
then
A17: b*1=b*b"*(a*1);
-1=b"*a*1 by A1,A16,Lm3;
then -1=b"*b*1 by A15,A17,XCMPLX_0:def 7;
hence thesis by A15,XCMPLX_0:def 7;
end;
hence thesis by A9,A11;
end;
hence thesis;
end;
hence thesis by A5;
end;
reserve uu,vv for object;
definition
let V;
let x,y;
func CORTE(V,x,y) -> Relation of [:the carrier of V,the carrier of V:] means
:Def5:
[uu,vv] in it iff
ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
existence
proof
set VV = [:the carrier of V,the carrier of V :];
defpred P[object,object] means ex u1,u2,v1,v2 st $1=[u1,u2] &
$2=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
consider P being Relation of VV,VV such that
A1: for uu,vv being object holds
([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from RELSET_1:sch 1;
take P;
let uu,vv;
thus [uu,vv] in P implies ex u1,u2,v1,v2 st
uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y by A1;
assume
A2: ex
u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
then
A3: uu in VV by ZFMISC_1:def 2;
vv in VV by A2,ZFMISC_1:def 2;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let P,Q be Relation of [:the carrier of V,the carrier of V:] such that
A4: [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrte_wrt x,y and
A5: [uu,vv] in Q iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrte_wrt x,y;
for uu,vv being object holds [uu,vv] in P iff [uu,vv] in Q
proof
let uu,vv be object;
[uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrte_wrt x,y by A4;
hence thesis by A5;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let V;
let x,y;
func CORTM(V,x,y) -> Relation of [:the carrier of V,the carrier of V:] means
:Def6:
[uu,vv] in it iff
ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
existence
proof
set VV = [:the carrier of V,the carrier of V :];
defpred P[object,object] means ex u1,u2,v1,v2 st $1=[u1,u2] &
$2=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
consider P being Relation of VV,VV such that
A1: for uu,vv being object holds
([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from RELSET_1:sch 1;
take P;
let uu,vv;
thus [uu,vv] in P implies ex u1,u2,v1,v2 st
uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y by A1;
assume
A2: ex
u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
then
A3: uu in VV by ZFMISC_1:def 2;
vv in VV by A2,ZFMISC_1:def 2;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let P,Q be Relation of [:the carrier of V,the carrier of V:] such that
A4: [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrtm_wrt x,y and
A5: [uu,vv] in Q iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrtm_wrt x,y;
for uu,vv being object holds [uu,vv] in P iff [uu,vv] in Q
proof
let uu,vv be object;
[uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
u1,u2,v1,v2 are_COrtm_wrt x,y by A4;
hence thesis by A5;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let V;
let x,y;
func CESpace(V,x,y) -> strict OrtStr equals
OrtStr(# the carrier of V,CORTE(V,x,y) #);
correctness;
end;
registration
let V;
let x,y;
cluster CESpace(V,x,y) -> non empty;
coherence;
end;
definition
let V;
let x,y;
func CMSpace(V,x,y) -> strict OrtStr equals
OrtStr(# the carrier of V,CORTM(V,x,y) #);
correctness;
end;
registration
let V;
let x,y;
cluster CMSpace(V,x,y) -> non empty;
coherence;
end;
theorem
uu is Element of CESpace(V,x,y) iff uu is VECTOR of V;
theorem
uu is Element of CMSpace(V,x,y) iff uu is VECTOR of V;
reserve p,q,r,s for Element of CESpace(V,x,y);
theorem
u=p & v=q & u1=r & v1=s implies
(p,q _|_ r,s iff u,v,u1,v1 are_COrte_wrt x,y )
proof
assume that
A1: u=p and
A2: v=q and
A3: u1=r and
A4: v1=s;
A5: p,q _|_ r,s implies u,v,u1,v1 are_COrte_wrt x,y
proof
assume p,q _|_ r,s;
then [[p,q],[r,s]] in the orthogonality of CESpace(V,x,y)
by ANALMETR:def 5;
then consider u19,u29,v19,v29 being VECTOR of V such that
A6: [u,v]=[u19,u29] and
A7: [u1,v1]=[v19,v29] and
A8: u19,u29,v19,v29 are_COrte_wrt x,y by A1,A2,A3,A4,Def5;
A9: u=u19 by A6,XTUPLE_0:1;
A10: v=u29 by A6,XTUPLE_0:1;
u1=v19 by A7,XTUPLE_0:1;
hence thesis by A7,A8,A9,A10,XTUPLE_0:1;
end;
u,v,u1,v1 are_COrte_wrt x,y implies p,q _|_ r,s
proof
assume u,v,u1,v1 are_COrte_wrt x,y;
then [[u,v],[u1,v1]] in the orthogonality of
OrtStr(# the carrier of V,CORTE(V,x,y) #) by Def5;
hence thesis by A1,A2,A3,A4,ANALMETR:def 5;
end;
hence thesis by A5;
end;
reserve p,q,r,s for Element of CMSpace(V,x,y);
theorem
u=p & v=q & u1=r & v1=s implies
(p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
proof
assume that
A1: u=p and
A2: v=q and
A3: u1=r and
A4: v1=s;
A5: p,q _|_ r,s implies u,v,u1,v1 are_COrtm_wrt x,y
proof
assume p,q _|_ r,s;
then [[p,q],[r,s]] in the orthogonality of CMSpace(V,x,y)
by ANALMETR:def 5;
then consider u19,u29,v19,v29 being VECTOR of V such that
A6: [u,v]=[u19,u29] and
A7: [u1,v1]=[v19,v29] and
A8: u19,u29,v19,v29 are_COrtm_wrt x,y by A1,A2,A3,A4,Def6;
A9: u=u19 by A6,XTUPLE_0:1;
A10: v=u29 by A6,XTUPLE_0:1;
u1=v19 by A7,XTUPLE_0:1;
hence thesis by A7,A8,A9,A10,XTUPLE_0:1;
end;
u,v,u1,v1 are_COrtm_wrt x,y implies p,q _|_ r,s
proof
assume u,v,u1,v1 are_COrtm_wrt x,y;
then [[u,v],[u1,v1]] in the orthogonality of
OrtStr (# the carrier of V,CORTM(V,x,y) #) by Def6;
hence thesis by A1,A2,A3,A4,ANALMETR:def 5;
end;
hence thesis by A5;
end;