Copyright (c) 1991 Association of Mizar Users
environ
vocabulary RLVECT_1, ARYTM_1, ANALMETR, FUNCT_3, ANALOAF, SYMSP_1, RELAT_1,
ANALORT;
notation TARSKI, XBOOLE_0, ZFMISC_1, REAL_1, RELSET_1, RLVECT_1, STRUCT_0,
ANALOAF, ANALMETR, GEOMTRAP;
constructors REAL_1, ANALMETR, GEOMTRAP, TDGROUP, DOMAIN_1, XREAL_0, MEMBERED,
XBOOLE_0;
clusters TDGROUP, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0;
theorems GEOMTRAP, RELAT_1, REAL_1, RLVECT_1, ANALOAF, ANALMETR, ZFMISC_1,
XCMPLX_0, XCMPLX_1;
schemes RELSET_1;
begin
definition let V be Abelian (non empty LoopStr),
v,w be Element of V;
redefine func v + w;
commutativity by RLVECT_1:def 5;
end;
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 6
.= ((b1*x + c1*x) + b2*y) + c2*y by RLVECT_1:def 6
.= ((b1 + c1)*x + b2*y) + c2*y by RLVECT_1:def 9
.= (b1 + c1)*x + (b2*y + c2*y) by RLVECT_1:def 6
.= (b1 + c1)*x + (b2 + c2)*y by RLVECT_1:def 9;
thus v1 - v2 = (b1*x + b2*y)+(-(c1*x + c2*y)) by A1,A2,RLVECT_1:def 11
.= (b1*x + b2*y)+(-(c1*x) + -(c2*y)) by RLVECT_1:45
.= (b1*x + b2*y)+(c1*(-x) + -(c2*y)) by RLVECT_1:39
.= (b1*x + b2*y)+(c1*(-x) + c2*(-y)) by RLVECT_1:39
.= (b1*x + b2*y)+((-c1)*x + c2*(-y)) by RLVECT_1:38
.= (b1*x + b2*y)+((-c1)*x + (-c2)*y) by RLVECT_1:38
.= ((b1*x + b2*y) + (-c1)*x) + (-c2)*y by RLVECT_1:def 6
.= ((b1*x + (-c1)*x) + b2*y) + (-c2)*y by RLVECT_1:def 6
.= ((b1 + (-c1))*x + b2*y) + (-c2)*y by RLVECT_1:def 9
.= (b1 + (-c1))*x + (b2*y + (-c2)*y) by RLVECT_1:def 6
.= (b1 + (-c1))*x + (b2 + (-c2))*y by RLVECT_1:def 9
.= (b1 - c1)*x + (b2 + (-c2))*y by XCMPLX_0:def 8
.= (b1 - c1)*x + (b2 - c2)*y by XCMPLX_0:def 8; 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 9 .= (a*b1)*x + a*(b2*y) by RLVECT_1:def 9
.= (a*b1)*x + (a*b2)*y by RLVECT_1:def 9; 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;
0.V = (a1*x+a2*y)-(b1*x+b2*y) by A2,RLVECT_1:28
.= (a1-b1)*x+(a2-b2)*y by Lm1; then a1-b1=0 & a2-b2=0 by A1,ANALMETR:def 1;
then -b1 + a1 =0 & -b2 + a2 = 0 by XCMPLX_0:def 8;
then a1=-(-b1) & a2=-(-b2) by XCMPLX_0:def 6;
hence thesis; 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:23
.=0.V+0.V by RLVECT_1:23 .=0.V by RLVECT_1:10;
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:23
.=0.V+0.V by RLVECT_1:23 .=0.V by RLVECT_1:10;
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 ex b st u = (pr1(x,y,u))*x + b*y by GEOMTRAP:def 4;
hence thesis by A1,GEOMTRAP:def 5; end;
Lm6: (Gen x,y & u=k1*x+k2*y) implies k1=pr1(x,y,u) & k2=pr2(x,y,u)
proof assume A1: Gen x,y & u=k1*x+k2*y;
then u = pr1(x,y,u)*x + pr2(x,y,u)*y by Lm5; hence thesis by A1,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 & v = p1v*x + p2v*y by A1,Lm5;
then u + v = (p1u*x + p2u*y + p1v*x) + p2v*y by RLVECT_1:def 6
.= ((p1u*x + p1v*x) + p2u*y) + p2v*y by RLVECT_1:def 6
.= (p1u*x + p1v*x) + (p2u*y + p2v*y) by RLVECT_1:def 6
.= (p1u + p1v)*x + (p2u*y + p2v*y) by RLVECT_1:def 9
.= (p1u + p1v)*x + (p2u + p2v)*y by RLVECT_1:def 9;
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,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 pr1(x,y,a*u) = a*pr1(x,y,u) & pr2(x,y,a*u) = a*pr2(x,y,u) by A1,Lm6;
end;
definition let V,x,y;
let u;
func Ortm(x,y,u) -> VECTOR of V equals
:Def1: 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;
thus Ortm(x,y,u+v)=pr1(x,y,u+v)*x + (-pr2(x,y,u+v))*y by Def1
.= (pr1(x,y,u)+pr1(x,y,v))*x + (-pr2(x,y,u+v))*y by A1,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 9
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (pr2(x,y,u) + pr2(x,y,v))*(-y)
by RLVECT_1:38
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-((pr2(x,y,u) + pr2(x,y,v))*y))
by RLVECT_1:39
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y +pr2(x,y,v)*y))
by RLVECT_1:def 9
.=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y) + (-(pr2(x,y,v)*y)))
by RLVECT_1:45
.=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 + ((-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y)))
by RLVECT_1:def 6
.=pr1(x,y,u)*x + (-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
by RLVECT_1:def 6
.=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
by RLVECT_1:39
.=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
by RLVECT_1:39
.=pr1(x,y,u)*x + (-pr2(x,y,u))*y + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
by RLVECT_1:38
.=pr1(x,y,u)*x + (-pr2(x,y,u))*y + (pr1(x,y,v)*x + (-pr2(x,y,v))*y)
by RLVECT_1:38
.=pr1(x,y,u)*x + (-pr2(x,y,u))*y + Ortm(x,y,v) by Def1
.=Ortm(x,y,u) + Ortm(x,y,v) by Def1;
end;
theorem
Th2: Gen x,y implies Ortm(x,y,n*u)= n*Ortm(x,y,u)
proof
assume A1:Gen x,y;
thus Ortm(x,y,n*u)=pr1(x,y,n*u)*x + (-pr2(x,y,n*u))*y by Def1
.=n*pr1(x,y,u)*x + (-pr2(x,y,n*u))*y by A1,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:38
.=n*pr1(x,y,u)*x + (-(n*pr2(x,y,u)*y)) by RLVECT_1:39
.=n*pr1(x,y,u)*x + (-(n*(pr2(x,y,u)*y))) by RLVECT_1:def 9
.=n*pr1(x,y,u)*x + n*(-pr2(x,y,u)*y) by RLVECT_1:39
.=n*(pr1(x,y,u)*x) + n*(-pr2(x,y,u)*y) by RLVECT_1:def 9
.=n*((pr1(x,y,u)*x) + (-pr2(x,y,u)*y)) by RLVECT_1:def 9
.=n*((pr1(x,y,u)*x) + (pr2(x,y,u)*(-y))) by RLVECT_1:39
.=n*((pr1(x,y,u)*x) + ((-pr2(x,y,u))*y)) by RLVECT_1:38
.=n*Ortm(x,y,u) by Def1;
end;
theorem
Gen x,y implies Ortm(x,y,0.V) = 0.V
proof assume A1:Gen x,y; consider u;
thus Ortm(x,y,0.V) = Ortm(x,y,0*u) by RLVECT_1:23
.= 0*Ortm(x,y,u) by A1,Th2
.= 0.V by RLVECT_1:23;
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:45
.=pr1(x,y,u)*(-x) + (-(pr2(x,y,u)*y)) by RLVECT_1:39
.=(-pr1(x,y,u))*x + (-(pr2(x,y,u)*y)) by RLVECT_1:38
.=(-pr1(x,y,u))*x + pr2(x,y,u)*(-y) by RLVECT_1:39
.=(-pr1(x,y,u))*x + (-pr2(x,y,u))*y by RLVECT_1:38;
thus Ortm(x,y,-u)=pr1(x,y,-u)*x + (-pr2(x,y,-u))*y by Def1
.=(-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 A1,A2,Lm6
.=pr1(x,y,u)*(-x) + (-(-pr2(x,y,u)))*y by RLVECT_1:38
.=-(pr1(x,y,u)*x) + (-(-pr2(x,y,u)))*y by RLVECT_1:39
.=-(pr1(x,y,u)*x) + (-pr2(x,y,u))*(-y) by RLVECT_1:38
.=-(pr1(x,y,u)*x) + (-((-pr2(x,y,u))*y)) by RLVECT_1:39
.=-(pr1(x,y,u)*x + (-pr2(x,y,u))*y) by RLVECT_1:45
.=-Ortm(x,y,u) by Def1;
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;
thus Ortm(x,y,u-v)=Ortm(x,y,u+(-v)) by RLVECT_1:def 11
.=Ortm(x,y,u) + Ortm(x,y,(-v)) by A1,Th1
.=Ortm(x,y,u) + (-Ortm(x,y,v)) by A1,Th4
.=Ortm(x,y,u) - Ortm(x,y,v) by RLVECT_1:def 11;
end;
theorem
Th6: Gen x,y & Ortm(x,y,u)=Ortm(x,y,v) implies u=v
proof
assume A1:Gen x,y & Ortm(x,y,u)=Ortm(x,y,v);
then Ortm(x,y,u)=pr1(x,y,v)*x + (-pr2(x,y,v))*y by Def1;
then pr1(x,y,u)*x + (-pr2(x,y,u))*y - (pr1(x,y,v)*x + (-pr2(x,y,v))*y)
=pr1(x,y,v)*x + (-pr2(x,y,v))*y - (pr1(x,y,v)*x + (-pr2(x,y,v))*y) by Def1;
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:28;
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:41;
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:def 11;
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 6;
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 11;
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:42;
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:49;
then (pr1(x,y,u) - pr1(x,y,v))*x + ((-pr2(x,y,u)) - (-pr2(x,y,v)))*y
=0.V by RLVECT_1:49;
then pr1(x,y,u) - pr1(x,y,v)=0 & (-pr2(x,y,u)) - (-pr2(x,y,v))=0
by A1,ANALMETR:def 1;
then A2: pr1(x,y,u)=pr1(x,y,v) & -pr2(x,y,u)=-pr2(x,y,v) by XCMPLX_1:15;
hence u=pr1(x,y,v)*x + pr2(x,y,u)*y by A1,Lm5
.=pr1(x,y,v)*x + pr2(x,y,v)*y by A2,XCMPLX_1:134
.=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;
thus Ortm(x,y,Ortm(x,y,u))=Ortm(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y) by Def1
.=pr1(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y)*x
+(-pr2(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y))*y by Def1
.=pr1(x,y,u)*x+(-pr2(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y))*y by A1,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
:Def2: 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:45
.=pr1(x,y,v)*(-x) + (-(pr2(x,y,v)*y)) by RLVECT_1:39
.=(-pr1(x,y,v))*x + (-(pr2(x,y,v)*y)) by RLVECT_1:38
.=(-pr1(x,y,v))*x + pr2(x,y,v)*(-y) by RLVECT_1:39
.=(-pr1(x,y,v))*x + (-pr2(x,y,v))*y by RLVECT_1:38;
thus Orte(x,y,-v)=pr2(x,y,-v)*x + (-pr1(x,y,-v))*y by Def2
.=(-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 A1,A2,Lm6
.=pr2(x,y,v)*(-x) + (-(-pr1(x,y,v)))*y by RLVECT_1:38
.=-(pr2(x,y,v)*x) + (-(-pr1(x,y,v)))*y by RLVECT_1:39
.=-(pr2(x,y,v)*x) + (-pr1(x,y,v))*(-y) by RLVECT_1:38
.=-(pr2(x,y,v)*x) + (-((-pr1(x,y,v))*y)) by RLVECT_1:39
.=-(pr2(x,y,v)*x + (-pr1(x,y,v))*y) by RLVECT_1:45
.=-Orte(x,y,v) by Def2;
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;
thus Orte(x,y,u+v)=pr2(x,y,u+v)*x + (-pr1(x,y,u+v))*y by Def2
.=(pr2(x,y,u+v))*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y by A1,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 9
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (pr1(x,y,u)+pr1(x,y,v))*(-y)
by RLVECT_1:38
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-((pr1(x,y,u)+pr1(x,y,v))*y))
by RLVECT_1:39
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y +pr1(x,y,v)*y))
by RLVECT_1:def 9
.=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y) +(-(pr1(x,y,v)*y)))
by RLVECT_1:45
.=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 + (-(pr1(x,y,u)*y) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y))))
by RLVECT_1:def 6
.=pr2(x,y,u)*x + (-(pr1(x,y,u)*y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
by RLVECT_1:def 6
.=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
by RLVECT_1:39
.=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
by RLVECT_1:39
.=pr2(x,y,u)*x + ((-pr1(x,y,u))*y) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
by RLVECT_1:38
.=pr2(x,y,u)*x + (-pr1(x,y,u))*y + (pr2(x,y,v)*x +(-pr1(x,y,v))*y)
by RLVECT_1:38
.=pr2(x,y,u)*x + (-pr1(x,y,u))*y + Orte(x,y,v) by Def2
.=Orte(x,y,u) + Orte(x,y,v) by Def2;
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;
thus Orte(x,y,u-v)=Orte(x,y,u+(-v)) by RLVECT_1:def 11
.=Orte(x,y,u) + Orte(x,y,(-v)) by A1,Th10
.=Orte(x,y,u) + (-Orte(x,y,v)) by A1,Th9
.=Orte(x,y,u) - Orte(x,y,v) by RLVECT_1:def 11;
end;
theorem
Th12: Gen x,y implies Orte(x,y,n*u)=n*Orte(x,y,u)
proof
assume A1:Gen x,y;
thus Orte(x,y,n*u)=pr2(x,y,n*u)*x + (-pr1(x,y,n*u))*y by Def2
.=n*pr2(x,y,u)*x + (-pr1(x,y,n*u))*y by A1,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:38
.=n*pr2(x,y,u)*x + (-(n*pr1(x,y,u)*y)) by RLVECT_1:39
.=n*pr2(x,y,u)*x + (-(n*(pr1(x,y,u)*y))) by RLVECT_1:def 9
.=n*pr2(x,y,u)*x + n*(-(pr1(x,y,u)*y)) by RLVECT_1:39
.=n*(pr2(x,y,u)*x) + n*(-(pr1(x,y,u)*y)) by RLVECT_1:def 9
.=n*(pr2(x,y,u)*x + (-(pr1(x,y,u)*y))) by RLVECT_1:def 9
.=n*(pr2(x,y,u)*x + (pr1(x,y,u)*(-y))) by RLVECT_1:39
.=n*(pr2(x,y,u)*x + (-pr1(x,y,u))*y) by RLVECT_1:38
.=n*Orte(x,y,u) by Def2;
end;
theorem
Th13: Gen x,y & Orte(x,y,u)=Orte(x,y,v) implies u=v
proof
assume A1:Gen x,y & Orte(x,y,u)=Orte(x,y,v);
then Orte(x,y,u)=pr2(x,y,v)*x + (-pr1(x,y,v))*y by Def2;
then pr2(x,y,u)*x + (-pr1(x,y,u))*y - (pr2(x,y,v)*x + (-pr1(x,y,v))*y)
=pr2(x,y,v)*x + (-pr1(x,y,v))*y - (pr2(x,y,v)*x + (-pr1(x,y,v))*y) by Def2;
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:28;
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:41;
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:def 11;
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 6;
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 11;
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:42;
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:49;
then (pr2(x,y,u) - pr2(x,y,v))*x + ((-pr1(x,y,u)) - (-pr1(x,y,v)))*y
=0.V by RLVECT_1:49;
then pr2(x,y,u) - pr2(x,y,v)=0 & (-pr1(x,y,u)) - (-pr1(x,y,v))=0
by A1,ANALMETR:def 1;
then A2: pr2(x,y,u)=pr2(x,y,v) & -pr1(x,y,u)=-pr1(x,y,v) by XCMPLX_1:15;
thus u=pr1(x,y,u)*x + pr2(x,y,u)*y by A1,Lm5
.=pr1(x,y,v)*x + pr2(x,y,v)*y by A2,XCMPLX_1:134
.=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;
thus Orte(x,y,Orte(x,y,u))=Orte(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y) by Def2
.=(pr2(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y))*x+
(-pr1(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y))*y by Def2
.=(-pr1(x,y,u))*x+
(-pr1(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y))*y by A1,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:38
.=-(pr1(x,y,u)*x)+(-pr2(x,y,u))*y by RLVECT_1:39
.=-(pr1(x,y,u)*x)+pr2(x,y,u)*(-y) by RLVECT_1:38
.=-(pr1(x,y,u)*x)+(-(pr2(x,y,u)*y)) by RLVECT_1:39
.=-(pr1(x,y,u)*x+pr2(x,y,u)*y) by RLVECT_1:45
.=-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:30;
end;
definition let V; let x,y,u,v,u1,v1;
pred u,v,u1,v1 are_COrte_wrt x,y means
:Def3: Orte(x,y,u),Orte(x,y,v) // u1,v1;
pred u,v,u1,v1 are_COrtm_wrt x,y means
:Def4: 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 u<>v & u1<>v1;
then consider a,b such that A3: 0<a & 0<b and
A4:a*(v-u)=b*(v1-u1) by A2,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,A4,Th12
.= b*(Orte(x,y,v1-u1)) by A1,Th12
.=b*(Orte(x,y,v1)-Orte(x,y,u1)) by A1,Th11;
hence Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u1),Orte(x,y,v1)
by A3,ANALOAF:def 1;end;
hence thesis by ANALOAF:18;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 & 0<b and
A5: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,A5,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,ANALOAF:def 1;end;
hence thesis by ANALOAF:18;end;
hence thesis by ANALOAF:18;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 by Def3;
then v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:21;
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:21;
-u1-(-u)=-u1+(-(-u)) by RLVECT_1:def 11 .=u+(-u1) by RLVECT_1:30
.=u-u1 by RLVECT_1:def 11;
then A3:-u,-u1 // u1,u by ANALOAF:24;
A4:now assume -u<>-u1;
then Orte(x,y,v),Orte(x,y,v1) // u1,u by A2,A3,ANALOAF:20;
hence thesis by Def3;end;
now assume -u=-u1;
then u=-(-u1) by RLVECT_1:30 .= u1 by RLVECT_1:30;
then Orte(x,y,v),Orte(x,y,v1) // u1,u by ANALOAF:18;
hence thesis by Def3;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 by Def4;
then v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
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 by Def4;end;
theorem
Th20: u,u,v,w are_COrte_wrt x,y
proof
Orte(x,y,u),Orte(x,y,u) // v,w by ANALOAF:18;
hence u,u,v,w are_COrte_wrt x,y by Def3;
end;
theorem
u,u,v,w are_COrtm_wrt x,y
proof
Ortm(x,y,u),Ortm(x,y,u) // v,w by ANALOAF:18;
hence u,u,v,w are_COrtm_wrt x,y by Def4;
end;
theorem
u,v,w,w are_COrte_wrt x,y
proof
Orte(x,y,u),Orte(x,y,v) // w,w by ANALOAF:18;
hence u,v,w,w are_COrte_wrt x,y by Def3;
end;
theorem
u,v,w,w are_COrtm_wrt x,y
proof
Ortm(x,y,u),Ortm(x,y,v) // w,w by ANALOAF:18;
hence u,v,w,w are_COrtm_wrt x,y by Def4;
end;
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 by Def2;
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
.= pr1(x,y,v-u)*pr2(x,y,v-u) + (-pr1(x,y,v-u)*pr2(x,y,v-u)) by XCMPLX_1:175
.= 0 by XCMPLX_0:def 6;
then v-u,w are_Ort_wrt x,y by A1,GEOMTRAP:34;
hence thesis by ANALMETR:def 3;
end;
theorem
u,v,Orte(x,y,u),Orte(x,y,v) are_COrte_wrt x,y
proof
Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u),Orte(x,y,v) by ANALOAF:17;
hence u,v,Orte(x,y,u),Orte(x,y,v) are_COrte_wrt x,y by Def3;
end;
theorem
u,v,Ortm(x,y,u),Ortm(x,y,v) are_COrtm_wrt x,y
proof
Ortm(x,y,u),Ortm(x,y,v) // Ortm(x,y,u),Ortm(x,y,v) by ANALOAF:17;
hence u,v,Ortm(x,y,u),Ortm(x,y,v) are_COrtm_wrt x,y by Def4;
end;
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;
(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
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 A5: u=v & u1=v1;
take u2=0.V,v2=x;
Orte(x,y,u2),Orte(x,y,v2) // u,v & Orte(x,y,u2),Orte(x,y,v2) // u1,v1
by A5,ANALOAF:18;
then A6:u2,v2,u1,v1 are_COrte_wrt x,y & u2,v2,u,v are_COrte_wrt x,y
by Def3; u2<>v2 by A1,Lm4;
hence thesis by A6; end;
A7:now assume A8: u<>v;
consider u2 such that A9: Orte(x,y,u2)=u by A1,Th15;
consider v2 such that A10: Orte(x,y,v2)=v by A1,Th15;
Orte(x,y,u2),Orte(x,y,v2) // u,v by A9,A10,ANALOAF:17;
then A11:u2,v2,u,v are_COrte_wrt x,y by Def3;
u2,v2,u1,v1 are_COrte_wrt x,y by A3,A9,A10,Def3;
hence thesis by A8,A9,A10,A11; end;
now assume A12: u1<>v1;
consider u2 such that A13: Orte(x,y,u2)=u1 by A1,Th15;
consider v2 such that A14: Orte(x,y,v2)=v1 by A1,Th15;
Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A13,A14,ANALOAF:17;
then A15:u2,v2,u1,v1 are_COrte_wrt x,y by Def3;
Orte(x,y,u2),Orte(x,y,v2) // u,v by A3,A13,A14,ANALOAF:21;
then u2,v2,u,v are_COrte_wrt x,y by Def3;
hence thesis by A12,A13,A14,A15; end;
hence thesis by A4,A7; 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
proof
given u2,v2 such that A16:u2<>v2 & u2,v2,u,v are_COrte_wrt x,y &
u2,v2,u1,v1 are_COrte_wrt x,y;
A17: Orte(x,y,u2) <> Orte(x,y,v2) by A1,A16,Th13;
Orte(x,y,u2),Orte(x,y,v2) // u,v &
Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A16,Def3;
hence thesis by A17,ANALOAF:20; end;
hence thesis by A2; end;
hence thesis; 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;
(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
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 A5: u=v & u1=v1;
take u2=0.V,v2=x;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v & Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1
by A5,ANALOAF:18;
then A6:u2,v2,u1,v1 are_COrtm_wrt x,y & u2,v2,u,v are_COrtm_wrt x,y
by Def4; u2<>v2 by A1,Lm4;
hence thesis by A6; end;
A7:now assume A8: u<>v;
consider u2 such that A9: Ortm(x,y,u2)=u by A1,Th8;
consider v2 such that A10: Ortm(x,y,v2)=v by A1,Th8;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A9,A10,ANALOAF:17;
then A11:u2,v2,u,v are_COrtm_wrt x,y by Def4;
u2,v2,u1,v1 are_COrtm_wrt x,y by A3,A9,A10,Def4;
hence thesis by A8,A9,A10,A11; end;
now assume A12: u1<>v1;
consider u2 such that A13: Ortm(x,y,u2)=u1 by A1,Th8;
consider v2 such that A14: Ortm(x,y,v2)=v1 by A1,Th8;
Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A13,A14,ANALOAF:17;
then A15:u2,v2,u1,v1 are_COrtm_wrt x,y by Def4;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A3,A13,A14,ANALOAF:21;
then u2,v2,u,v are_COrtm_wrt x,y by Def4;
hence thesis by A12,A13,A14,A15; end;
hence thesis by A4,A7; 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
proof
given u2,v2 such that A16:u2<>v2 & u2,v2,u,v are_COrtm_wrt x,y &
u2,v2,u1,v1 are_COrtm_wrt x,y;
A17: Ortm(x,y,u2) <> Ortm(x,y,v2) by A1,A16,Th6;
Ortm(x,y,u2),Ortm(x,y,v2) // u,v &
Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A16,Def4;
hence thesis by A17,ANALOAF:20; end;
hence thesis by A2; end;
hence thesis; 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:28;
then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:9;
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:35;
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:13;
then u2,v2 // u1,v1 or u2,v2 // v1,u1 by ANALMETR:18;
hence u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y by Def3;
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 by Def3; then consider a,b such that
A7: a*(v2-u2)=b*(v1-u1) and A8: a<>0 or b<>0 by ANALMETR:18;
A9: now assume A10: b=0;
then 0.V = a*(v2-u2) by A7,RLVECT_1:23; then v2-u2=0.V
by A8,A10,RLVECT_1:24; then v2=u2 by RLVECT_1:35; then u=v by A1,Th13;
then v-u=0.V by RLVECT_1:28;
then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:9;
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 9;
then ((b")*a)*(v2-u2)=((b")*b)*(v1-u1) by RLVECT_1:def 9;
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 9;
then v-u,v1-u1 are_Ort_wrt x,y by A5,ANALMETR:11;
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 A2:u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y;
assume A3: u<>v & u1<>v1;
A4: Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // v1,u1
by A2,Def3;
Orte(x,y,u) <> Orte(x,y,v) by A1,A3,Th13;
then u1,v1 // v1,u1 by A4,ANALOAF:20;
hence contradiction by A3,ANALOAF:19;
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 A2:u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y;
assume A3: u<>v & u1<>v1;
A4: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // v1,u1
by A2,Def4;
Ortm(x,y,u) <> Ortm(x,y,v) by A1,A3,Th6;
then u1,v1 // v1,u1 by A4,ANALOAF:20;
hence contradiction by A3,ANALOAF:19;
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 A1:Gen x,y &
u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y;
then A2:Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // u1,w
by Def3;
now assume A3:u<>v;
now assume A4: u1<>v1 & u1<>w;
Orte(x,y,u) <> Orte(x,y,v) by A1,A3,Th13;
then A5: u1,v1 // u1,w by A2,ANALOAF:20;
A6: now assume A7: u1,v1 // v1,w;
u1,v1 // Orte(x,y,u),Orte(x,y,v) by A2,ANALOAF:21;
then Orte(x,y,u),Orte(x,y,v) // v1,w by A4,A7,ANALOAF:20;
hence thesis by Def3; end;
now assume A8: u1,w // w,v1;
u1,w // Orte(x,y,u),Orte(x,y,v) by A2,ANALOAF:21;
then Orte(x,y,u),Orte(x,y,v) // w,v1 by A4,A8,ANALOAF:20;
hence thesis by Def3; end;
hence thesis by A5,A6,ANALOAF:23; end;
hence thesis by A1; 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 A1:Gen x,y &
u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y;
then A2:Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // u1,w
by Def4;
A3:now assume A4:u<>v & u1<>v1;
then Ortm(x,y,u) <> Ortm(x,y,v) by A1,Th6;
then u1,v1 // u1,w by A2,ANALOAF:20;
then A5:u1,v1 // v1,w or u1,w // w,v1 by ANALOAF:23;
now assume A6:u1<>w;
u1,v1 // Ortm(x,y,u),Ortm(x,y,v) & u1,w // Ortm(x,y,u),Ortm(x,y,v)
by A2,ANALOAF:21;
then Ortm(x,y,u),Ortm(x,y,v) // v1,w or
Ortm(x,y,u),Ortm(x,y,v) // w,v1 by A4,A5,A6,ANALOAF:20;
hence thesis by Def4;end;
hence thesis by A1;end;
now assume u=v; then Ortm(x,y,u),Ortm(x,y,v) // v1,w or
Ortm(x,y,u),Ortm(x,y,v) // w,v1 by ANALOAF:18;
hence thesis by Def4;end;
hence thesis by A1,A3;end;
theorem
u,v,u1,v1 are_COrte_wrt x,y implies v,u,v1,u1 are_COrte_wrt x,y
proof
assume u,v,u1,v1 are_COrte_wrt x,y;
then Orte(x,y,u),Orte(x,y,v) // u1,v1 by Def3;
then Orte(x,y,v),Orte(x,y,u) // v1,u1 by ANALOAF:21;
hence thesis by Def3;
end;
theorem
u,v,u1,v1 are_COrtm_wrt x,y implies v,u,v1,u1 are_COrtm_wrt x,y
proof
assume u,v,u1,v1 are_COrtm_wrt x,y;
then Ortm(x,y,u),Ortm(x,y,v) // u1,v1 by Def4;
then Ortm(x,y,v),Ortm(x,y,u) // v1,u1 by ANALOAF:21;
hence thesis by Def4;
end;
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 A2:u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y;
then A3:Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // v1,w
by Def3;
then A4:u1,v1 // Orte(x,y,u),Orte(x,y,v) by ANALOAF:21;
A5:now assume u<>v;
then Orte(x,y,u) <> Orte(x,y,v) by A1,Th13;
then u1,v1 // v1,w by A3,ANALOAF:20;
then A6:u1,v1 // u1,w by ANALOAF:22;
now assume u1<>v1;
then Orte(x,y,u),Orte(x,y,v) // u1,w by A4,A6,ANALOAF:20;
hence thesis by Def3;end;
hence thesis by A2;
end;
now assume u=v;
then Orte(x,y,u),Orte(x,y,v) // u1,w by ANALOAF:18;
hence thesis by Def3;
end;
hence thesis by A5;
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 A2:u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y;
then A3:Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // v1,w
by Def4;
then A4:u1,v1 // Ortm(x,y,u),Ortm(x,y,v) by ANALOAF:21;
A5:now assume u<>v;
then Ortm(x,y,u) <> Ortm(x,y,v) by A1,Th6;
then u1,v1 // v1,w by A3,ANALOAF:20;
then A6: u1,v1 // u1,w by ANALOAF:22;
now assume u1<>v1;
then Ortm(x,y,u),Ortm(x,y,v) // u1,w by A4,A6,ANALOAF:20;
hence thesis by Def4; end;
hence thesis by A2;
end;
now assume u=v;
then Ortm(x,y,u),Ortm(x,y,v) // u1,w by ANALOAF:18;
hence thesis by Def4;
end;
hence thesis by A5;
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:18;
then A4:w,u1,u,v are_COrte_wrt x,y by Def3;
now assume w=u1; then x=0.V by RLVECT_1:22;
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:25;
then w,u1 // u2,v2 by ANALOAF:21;
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,Def3;
now assume w=u1; then w=
w+(v2-u2) by RLVECT_1:42; then v2-u2=0.V by RLVECT_1:22;
hence contradiction by A5,A6,A7,RLVECT_1:35; 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:18;
then A4:w,u1,u,v are_COrtm_wrt x,y by Def4;
now assume w=u1; then x=0.V by RLVECT_1:22;
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:25;
then w,u1 // u2,v2 by ANALOAF:21;
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,Def4;
now assume w=u1; then w=
w+(v2-u2) by RLVECT_1:42; then v2-u2=0.V by RLVECT_1:22;
hence contradiction by A5,A6,A7,RLVECT_1:35; 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:18;
then A4:u,v,w,u1 are_COrte_wrt x,y by Def3;
now assume w=u1; then x=0.V by RLVECT_1:22;
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:25;
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:21;
then Orte(x,y,u1),Orte(x,y,w) // u,v by ANALOAF:21;
then u1,w,u,v are_COrte_wrt x,y by Def3;
then A8:u,v,w,u1 are_COrte_wrt x,y by A1,Th18;
now assume w=u1; then w=
w+(u2-v2) by RLVECT_1:42; then u2-v2=0.V by RLVECT_1:22;
hence contradiction by A5,A6,A7,RLVECT_1:35; end;
hence thesis by A8;
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:18;
then w,u1,u,v are_COrtm_wrt x,y by Def4;
then A4:u,v,w,u1 are_COrtm_wrt x,y by A1,Th19;
w<>u1 proof
assume w=u1; then x=0.V by RLVECT_1:22;
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:25;
then w,u1 // u2,v2 by ANALOAF:21;
then Ortm(x,y,w),Ortm(x,y,u1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
then w,u1,u,v are_COrtm_wrt x,y by A6,A7,Def4;
then A8:u,v,w,u1 are_COrtm_wrt x,y by A1,Th19; w<>u1
proof
assume w=u1; then w= w+(v2-u2) by RLVECT_1:42; then v2-u2=0.V by RLVECT_1:22;
hence contradiction by A5,A6,A7,RLVECT_1:35; end;
hence thesis by A8;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 A2: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;
then Orte(x,y,u),Orte(x,y,u1) // v,v1 by Def3;
then A3:v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:21;
Orte(x,y,w),Orte(x,y,w1) // v,v1 by A2,Def3;
then A4:v,v1 // Orte(x,y,w),Orte(x,y,w1) by ANALOAF:21;
A5:Orte(x,y,w),Orte(x,y,w1) // u2,v2 by A2,Def3;
now assume A6:w<>w1 & v<>v1;
then A7:Orte(x,y,w) <> Orte(x,y,w1) by A1,Th13;
Orte(x,y,w),Orte(x,y,w1) // Orte(x,y,u),Orte(x,y,u1)
by A3,A4,A6,ANALOAF:20;
then Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A5,A7,ANALOAF:20;
hence u,u1,u2,v2 are_COrte_wrt x,y by Def3;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 A2: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;
then Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
then A3:v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
Ortm(x,y,w),Ortm(x,y,w1) // v,v1 by A2,Def4;
then A4:v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:21;
A5:Ortm(x,y,w),Ortm(x,y,w1) // u2,v2 by A2,Def4;
now assume A6:w<>w1 & v<>v1;
then A7:Ortm(x,y,w) <> Ortm(x,y,w1) by A1,Th6;
Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
by A3,A4,A6,ANALOAF:20;
then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A5,A7,ANALOAF:20;
hence u,u1,u2,v2 are_COrtm_wrt x,y by Def4;end;
hence thesis;end;
canceled 2;
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 A2: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;
then v,v1,u1,u are_COrte_wrt x,y by A1,Th18;
then A3:Orte(x,y,v),Orte(x,y,v1) // u1,u by Def3;
Orte(x,y,v),Orte(x,y,v1) // w,w1 by A2,Def3;
then A4:w,w1 // Orte(x,y,v),Orte(x,y,v1) by ANALOAF:21;
Orte(x,y,u2),Orte(x,y,v2) // w,w1 by A2,Def3;
then A5:w,w1 // Orte(x,y,u2),Orte(x,y,v2) by ANALOAF:21;
now assume A6:w<>w1 & v<>v1;
then A7:Orte(x,y,v),Orte(x,y,v1) // Orte(x,y,u2),Orte(x,y,v2)
by A4,A5,ANALOAF:20;
Orte(x,y,v) <> Orte(x,y,v1) by A1,A6,Th13;
then Orte(x,y,u2),Orte(x,y,v2) // u1,u by A3,A7,ANALOAF:20;
then Orte(x,y,v2),Orte(x,y,u2) // u,u1 by ANALOAF:21;
then v2,u2,u,u1 are_COrte_wrt x,y by Def3;
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 A2: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;
then Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
then A3:v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
w,w1,v,v1 are_COrtm_wrt x,y by A1,A2,Th19;
then Ortm(x,y,w),Ortm(x,y,w1) // v,v1 by Def4;
then A4:v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:21;
w,w1,u2,v2 are_COrtm_wrt x,y by A1,A2,Th19;
then A5:Ortm(x,y,w),Ortm(x,y,w1) // u2,v2 by Def4;
now assume A6:w<>w1 & v<>v1;
then A7:Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
by A3,A4,ANALOAF:20;
Ortm(x,y,w) <> Ortm(x,y,w1) by A1,A6,Th6;
then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A5,A7,ANALOAF:20;
hence thesis by Def4;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 A2: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;
then A3: Orte(x,y,u),Orte(x,y,u1) // v,v1 by Def3;
A4: Orte(x,y,v),Orte(x,y,v1) // w,w1 by A2,Def3;
A5:Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A2,Def3;
now assume u<>u1 & v<>v1;
then A6: Orte(x,y,u)<>Orte(x,y,u1) & Orte(x,y,v)<>Orte(x,y,v1) by A1,Th13;
then v,v1 // u2,v2 by A3,A5,ANALOAF:20;
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 A4,A6,ANALOAF:20;
hence thesis by Def3;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 A2: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;
then A3: Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
A4: Ortm(x,y,v),Ortm(x,y,v1) // w,w1 by A2,Def4;
A5:Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A2,Def4;
now assume u<>u1 & v<>v1;
then A6: Ortm(x,y,u)<>Ortm(x,y,u1) & Ortm(x,y,v)<>Ortm(x,y,v1) by A1,Th6;
then v,v1 // u2,v2 by A3,A5,ANALOAF:20;
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 A4,A6,ANALOAF:20;
hence thesis by Def4;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 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;
then A4:not Orte(x,y,v),Orte(x,y,v1) // w,u1 &
Orte(x,y,v),Orte(x,y,v1) // v,u &
Orte(x,y,u1),Orte(x,y,w1) // u1,w &
not Orte(x,y,v),Orte(x,y,v1) // u1,w by A3,Def3;
then A5: v,u // Orte(x,y,v),Orte(x,y,v1) &
u1,w // Orte(x,y,u1),Orte(x,y,w1) by ANALOAF:21;
A6: u1<>w by A4,ANALOAF:18;
A7: not (v,u // u1,w or v,u // w,u1) by A2,A4,A5,ANALOAF:20;
Gen x,y implies (ex u,v st (for w ex a,b st a*u + b*v=w))
proof assume A8:Gen x,y;take x,y;thus thesis by A8,ANALMETR:def 1;end;
then consider u2 such that A9: v,u // v,u2 or v,u // u2,v and
A10: u1,w // u1,u2 or u1,w // u2,u1 by A1,A7,ANALOAF:31;
Orte(x,y,v),Orte(x,y,v1) // v,u2 or Orte(x,y,v),Orte(x,y,v1) // u2,v
by A2,A5,A9,ANALOAF:20;
then A11: v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y
by Def3;
Orte(x,y,u1),Orte(x,y,w1) // u1,u2 or Orte(x,y,u1),Orte(x,y,w1) // u2,u1
by A5,A6,A10,ANALOAF:20;
then u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y
by Def3;
hence thesis by A11; 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 & u,v,u,w are_COrte_wrt x,y by A1,Th40;take w;
A5:Orte(x,y,u) <> Orte(x,y,v) by A1,A3,Th13;
thus u,v,u,w are_COrte_wrt x,y by A4;
A6:Orte(x,y,u),Orte(x,y,v) // u,w by A4,Def3;
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 by Def3;
now assume v1<>w1; then A8:Orte(x,y,v1)<>Orte(x,y,w1) by A1,Th13;
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 by Def3;
then u,v // u,w or u,v // w,u by A7,A8,ANALOAF:20;
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 A5,A6,ANALOAF:20;
then consider a,b such that A9:a*(w-u)=b*(Orte(x,y,w)-Orte(x,y,u)) &
(a<>0 or b<>0) by ANALMETR:18;take a,b;
a*(w-u)=b*Orte(x,y,w-u) & (a<>0 or b<>0) by A1,A9,Th11;
then a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=b*Orte(x,y,w-u)
& (a<>0 or b<>0) by A1,Lm5;
then A10:a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
b*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y)
& (a<>0 or b<>0) by Def2;
A11:now assume A12:a<>0;
A13:pr2(x,y,w-u)<>0
proof assume A14: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 A10,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 A12,XCMPLX_1:6;
then w-u=0*x + 0*y by A1,A14,Lm5
.=0.V + 0*y by RLVECT_1:23 .=0.V + 0.V by RLVECT_1:23
.=0.V by RLVECT_1:10;
hence thesis by A4,RLVECT_1:35;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 A10,RLVECT_1:def 9;
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 9;
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 A12,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 9;
then 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) &
pr2(x,y,w-u)=(a"*b)*(-pr1(x,y,w-u)) by A1,Lm3;
then pr2(x,y,w-u)=-((a"*b)*((a"*b)*pr2(x,y,w-u))) by XCMPLX_1:175;
then pr2(x,y,w-u)"*(-pr2(x,y,w-u))=
pr2(x,y,w-u)"*((a"*b)*((a"*b)*pr2(x,y,w-u)));
then -(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 XCMPLX_1:175;
then -1=pr2(x,y,w-u)"*((a"*b)*((a"*b)*pr2(x,y,w-u))) by A13,XCMPLX_0:def
7
;
then -1=pr2(x,y,w-u)"*(pr2(x,y,w-u)*((a"*b)*(a"*b))) by XCMPLX_1:4;
then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((a"*b)*(a"*b)) by XCMPLX_1:4;
then -1=1*((a"*b)*(a"*b)) by A13,XCMPLX_0:def 7;
hence thesis by REAL_1:93;end;
now assume A15:b<>0;
A16:pr2(x,y,w-u)<>0
proof assume A17:not thesis;
then a*(pr1(x,y,w-u)*x + 0*y)=
(b*0)*x + (b*(-pr1(x,y,w-u)))*y by A10,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 A15,XCMPLX_1:6;
then w-u=0*x + 0*y by A1,A17,Lm5,REAL_1:26
.=0.V + 0*y by RLVECT_1:23 .=0.V + 0.V by RLVECT_1:23
.=0.V by RLVECT_1:10;
hence thesis by A4,RLVECT_1:35;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 A10,RLVECT_1:def 9;
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 9;
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 A15,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 9;
then (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)*pr1(x,y,w-u)=pr2(x,y,w-u) &
(b"*a)*pr2(x,y,w-u)=-pr1(x,y,w-u) by A1,Lm3;
then pr2(x,y,w-u)=(b"*a)*(-((b"*a)*pr2(x,y,w-u)));
then pr2(x,y,w-u)=-((b"*a)*((b"*a)*pr2(x,y,w-u))) by XCMPLX_1:175;
then pr2(x,y,w-u)"*(-pr2(x,y,w-u))=
pr2(x,y,w-u)"*((b"*a)*((b"*a)*pr2(x,y,w-u)));
then -(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 XCMPLX_1:175;
then -1=pr2(x,y,w-u)"*((b"*a)*((b"*a)*pr2(x,y,w-u))) by A16,XCMPLX_0:def
7
;
then -1=pr2(x,y,w-u)"*(pr2(x,y,w-u)*((b"*a)*(b"*a))) by XCMPLX_1:4;
then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((b"*a)*(b"*a)) by XCMPLX_1:4;
then -1=1*((b"*a)*(b"*a)) by A16,XCMPLX_0:def 7;
hence thesis by REAL_1:93;end;
hence thesis by A9,A11;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 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;
then A4:not Ortm(x,y,v),Ortm(x,y,v1) // w,u1 &
Ortm(x,y,v),Ortm(x,y,v1) // v,u &
Ortm(x,y,u1),Ortm(x,y,w1) // u1,w &
not Ortm(x,y,v),Ortm(x,y,v1) // u1,w by A3,Def4;
then A5: v,u // Ortm(x,y,v),Ortm(x,y,v1) &
u1,w // Ortm(x,y,u1),Ortm(x,y,w1) by ANALOAF:21;
A6: u1<>w by A4,ANALOAF:18;
A7: not (v,u // u1,w or v,u // w,u1) by A2,A4,A5,ANALOAF:20;
Gen x,y implies (ex u,v st (for w ex a,b st a*u + b*v=w))
proof assume A8:Gen x,y;take x,y;thus thesis by A8,ANALMETR:def 1;end;
then consider u2 such that A9: v,u // v,u2 or v,u // u2,v and
A10: u1,w // u1,u2 or u1,w // u2,u1 by A1,A7,ANALOAF:31;
Ortm(x,y,v),Ortm(x,y,v1) // v,u2 or Ortm(x,y,v),Ortm(x,y,v1) // u2,v
by A2,A5,A9,ANALOAF:20;
then A11: v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y
by Def4;
Ortm(x,y,u1),Ortm(x,y,w1) // u1,u2 or Ortm(x,y,u1),Ortm(x,y,w1) // u2,u1
by A5,A6,A10,ANALOAF:20;
then u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y
by Def4;
hence thesis by A11; 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 & pr2(x,y,u)=0 & pr1(x,y,v)=1 & pr2(x,y,v)=1 by A1,Lm6;
then A3:Ortm(x,y,u)=0*x+0*y by Def1,REAL_1:26;
Ortm(x,y,v)=1*x+(-1)*y by A2,Def1;
then A4: Ortm(x,y,u),Ortm(x,y,v) // u,w by A3,ANALOAF:17;
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 A5:Ortm(x,y,v1),Ortm(x,y,w1) // u,v by Def4;
now assume v1<>w1; then A6:Ortm(x,y,v1)<>Ortm(x,y,w1) by A1,Th6;
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 by Def4;
then u,v // u,w or u,v // w,u by A5,A6,ANALOAF:20;
then consider a,b such that A7:a*(v-u)=b*(w-u) &
(a<>0 or b<>0) by ANALMETR:18;take a,b;
u=0.V+0*y by RLVECT_1:23 .=0.V+0.V by RLVECT_1:23 .=0.V by RLVECT_1:10;
then a*v=b*(w-0.V) & (a<>0 or b<>0) by A7,RLVECT_1:26;
then A8:a*v=b*w & (a<>0 or b<>0) by RLVECT_1:26;
A9:now assume A10:a<>0;
a"*a*v=a"*(b*w) by A8,RLVECT_1:def 9;
then a"*a*v=a"*b*w by RLVECT_1:def 9;
then 1*v=a"*b*w by A10,XCMPLX_0:def 7;
then 1*v=a"*b*1*x+a"*b*(-1)*y by Lm2;
then 1*1*x+1*1*y=a"*b*1*x+a"*b*(-1)*y by Lm2;
then a*1=a*(a"*(b*1)) & 1=a"*b*(-1) by A1,Lm3;
then a*1=a*a"*(b*1) & 1=a"*b*(-1) by XCMPLX_1:4;
then 1=a"*a*(-1) by A10,XCMPLX_0:def 7; then 1=1*(-1) by A10,XCMPLX_0:def 7;
hence thesis;end;
now assume A11:b<>0;
b"*a*v=b"*(b*w) by A8,RLVECT_1:def 9;
then b"*a*v=b"*b*w by RLVECT_1:def 9;
then b"*a*v=1*w by A11,XCMPLX_0:def 7;
then b"*a*1*x+b"*a*1*y=1*w by Lm2;
then b"*a*1*x+b"*a*1*y=1*1*x+1*(-1)*y by Lm2;
then b*1=b*(b"*(a*1)) & -1=b"*a*1 by A1,Lm3;
then b*1=b*b"*(a*1) & -1=b"*a*1 by XCMPLX_1:4;
then -1=b"*b*1 by A11,XCMPLX_0:def 7;
hence thesis by A11,XCMPLX_0:def 7;end;
hence thesis by A7,A9;end;hence thesis;end;
hence thesis by A4,Def4;end;
reserve uu,vv for set;
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[set,set] 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 holds
([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from Rel_On_Set_Ex;
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 uu in VV & vv in VV by ZFMISC_1:def 2;
hence [uu,vv] in P by A1,A2;
end;
uniqueness
proof let P,Q be Relation of [:the carrier of V,the carrier of V:]
such that
A3:[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
A4:[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 holds [uu,vv] in P iff [uu,vv] in Q
proof let uu,vv;
[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 A3;
hence thesis by A4;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[set,set] 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 holds
([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from Rel_On_Set_Ex;
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 uu in VV & vv in VV by ZFMISC_1:def 2;
hence [uu,vv] in P by A1,A2;
end;
uniqueness
proof let P,Q be Relation of [:the carrier of V,the carrier of V:]
such that
A3:[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
A4:[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 holds [uu,vv] in P iff [uu,vv] in Q
proof let uu,vv;
[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 A3;
hence thesis by A4;end;
hence thesis by RELAT_1:def 2;end;
end;
definition let V;let x,y;
func CESpace(V,x,y) -> strict AffinStruct equals
:Def7: AffinStruct (# the carrier of V,CORTE(V,x,y) #);
correctness;
end;
definition let V;let x,y;
cluster CESpace(V,x,y) -> non empty;
coherence
proof
CESpace(V,x,y) = AffinStruct (# the carrier of V,CORTE(V,x,y) #) by Def7;
hence the carrier of CESpace(V,x,y) is non empty;
end;
end;
definition let V;let x,y;
func CMSpace(V,x,y) -> strict AffinStruct equals
:Def8: AffinStruct (# the carrier of V,CORTM(V,x,y) #);
correctness;
end;
definition let V;let x,y;
cluster CMSpace(V,x,y) -> non empty;
coherence
proof
CMSpace(V,x,y) = AffinStruct (# the carrier of V,CORTM(V,x,y) #) by Def8;
hence the carrier of CMSpace(V,x,y) is non empty;
end;
end;
theorem
uu is Element of CESpace(V,x,y) iff uu is VECTOR of V
proof
A1:uu is Element of CESpace(V,x,y) implies uu is VECTOR of V
proof
assume uu is Element of CESpace(V,x,y);
then uu is Element of
AffinStruct (# the carrier of V,CORTE(V,x,y) #) by Def7;
hence uu is VECTOR of V;end;
uu is VECTOR of V implies uu is Element of CESpace(V,x,y)
proof
assume uu is VECTOR of V;
then uu is Element of
AffinStruct (# the carrier of V,CORTE(V,x,y) #);
hence thesis by Def7;end;
hence thesis by A1;end;
theorem
uu is Element of CMSpace(V,x,y) iff uu is VECTOR of V
proof
A1:uu is Element of CMSpace(V,x,y) implies uu is VECTOR of V
proof
assume uu is Element of CMSpace(V,x,y);
then uu is Element of
AffinStruct (# the carrier of V,CORTM(V,x,y) #) by Def8;
hence uu is VECTOR of V;end;
uu is VECTOR of V implies uu is Element of CMSpace(V,x,y)
proof
assume uu is VECTOR of V;
then uu is Element of
AffinStruct (# the carrier of V,CORTM(V,x,y) #);
hence thesis by Def8;end;
hence thesis by A1;end;
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 A1: u=p & v=q & u1=r & v1=s;
A2: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 CONGR of CESpace(V,x,y) by ANALOAF:def 2;
then [[u,v],[u1,v1]] in the CONGR of
AffinStruct (# the carrier of V,CORTE(V,x,y) #) by A1,Def7;
then consider
u1',u2',v1',v2' being VECTOR of V such that
A3: [u,v]=[u1',u2'] & [u1,v1]=[v1',v2'] and
A4: u1',u2',v1',v2' are_COrte_wrt x,y by Def5;
u=u1' & v=u2' & u1=v1' & v1=v2' by A3,ZFMISC_1:33;
hence thesis by A4;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 CONGR of
AffinStruct (# the carrier of V,CORTE(V,x,y) #) by Def5;
then [[p,q],[r,s]] in the CONGR of CESpace(V,x,y) by A1,Def7;
hence thesis by ANALOAF:def 2;end;
hence thesis by A2;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 A1: u=p & v=q & u1=r & v1=s;
A2: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 CONGR of CMSpace(V,x,y) by ANALOAF:def 2;
then [[u,v],[u1,v1]] in the CONGR of
AffinStruct (# the carrier of V,CORTM(V,x,y) #) by A1,Def8;
then consider
u1',u2',v1',v2' being VECTOR of V such that
A3: [u,v]=[u1',u2'] & [u1,v1]=[v1',v2'] and
A4: u1',u2',v1',v2' are_COrtm_wrt x,y by Def6;
u=u1' & v=u2' & u1=v1' & v1=v2' by A3,ZFMISC_1:33;
hence thesis by A4;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 CONGR of
AffinStruct (# the carrier of V,CORTM(V,x,y) #) by Def6;
then [[p,q],[r,s]] in the CONGR of CMSpace(V,x,y) by A1,Def8;
hence thesis by ANALOAF:def 2;end;
hence thesis by A2;end;