:: A Construction of Analytical Ordered Trapezium Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received October 29, 1990
:: Copyright (c) 1990-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, REAL_1, PARSP_1, ANALOAF, ANALMETR, RELAT_1,
ARYTM_3, SUPINF_2, CARD_1, SUBSET_1, STRUCT_0, DIRAF, ARYTM_1, PBOOLE,
SYMSP_1, MCART_1, ZFMISC_1, BINOP_1, FUNCT_1, MIDSP_1, XBOOLE_0,
GEOMTRAP;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, STRUCT_0, DIRAF, RELSET_1, RLVECT_1,
MIDSP_1, AFF_1, ANALOAF, BINOP_1, ANALMETR;
constructors BINOP_1, DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, MIDSP_1, AFF_1,
ANALMETR;
registrations SUBSET_1, RELSET_1, MEMBERED, STRUCT_0, ANALOAF, DIRAF,
ANALMETR, XREAL_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0;
equalities RLVECT_1;
theorems RLVECT_1, RELAT_1, DIRAF, ANALOAF, ANALMETR, AFF_1, RLSUB_2,
XCMPLX_0, XCMPLX_1, XREAL_1, XTUPLE_0;
schemes RELSET_1, BINOP_1, BINOP_2;
begin
reserve V for RealLinearSpace;
reserve u,u1,u2,v,v1,v2,w,w1,y for VECTOR of V;
reserve a,a1,a2,b,b1,b2,c1,c2 for Real;
reserve x,z for set;
definition
let V;
let u,v,u1,v1;
pred u,v '||' u1,v1 means
u,v // u1,v1 or u,v // v1,u1;
end;
theorem Th1:
Gen w,y implies OASpace(V) is OAffinSpace
proof
assume Gen w,y;
then for a1,a2 st a1*w + a2*y = 0.V holds a1=0 & a2=0 by ANALMETR:def 1;
hence thesis by ANALOAF:26;
end;
theorem Th2:
for p,q,p1,q1 being Element of OASpace(V) st p=u & q=v & p1=u1 &
q1=v1 holds (p,q // p1,q1 iff u,v // u1,v1)
proof
A1: OASpace(V) = AffinStruct (#the carrier of V, DirPar(V)#) by ANALOAF:def 4;
let p,q,p1,q1 be Element of OASpace(V) such that
A2: p=u & q=v & p1=u1 & q1=v1;
A3: now
assume u,v // u1,v1;
then [[p,q],[p1,q1]] in the CONGR of OASpace(V) by A2,A1,ANALOAF:22;
hence p,q // p1,q1 by ANALOAF:def 2;
end;
now
assume p,q // p1,q1;
then [[u,v],[u1,v1]] in DirPar(V) by A2,A1,ANALOAF:def 2;
hence u,v // u1,v1 by ANALOAF:22;
end;
hence thesis by A3;
end;
theorem Th3:
Gen w,y implies for p,q,p1,q1 being Element of (the carrier of
Lambda(OASpace(V))) st p=u & q=v & p1=u1 & q1=v1 holds (p,q // p1,q1 iff u,v
'||' u1,v1)
proof
assume Gen w,y;
then reconsider S = OASpace(V) as OAffinSpace by Th1;
let p,q,p1,q1 be Element of (the carrier of Lambda(OASpace(V))) such that
A1: p=u & q=v & p1=u1 & q1=v1;
Lambda(OASpace(V)) = AffinStruct (# the carrier of OASpace(V), lambda(
the CONGR of OASpace(V)) #) by DIRAF:def 2;
then reconsider p9=p,q9=q,p19=p1,q19=q1 as Element of S;
A2: now
assume u,v '||' u1,v1;
then u,v // u1,v1 or u,v // v1,u1;
then p9,q9 // p19,q19 or p9,q9 // q19,p19 by A1,Th2;
then p9,q9 '||' p19, q19 by DIRAF:def 4;
hence p,q // p1,q1 by DIRAF:38;
end;
now
assume p,q // p1,q1;
then p9,q9 '||' p19,q19 by DIRAF:38;
then p9,q9 // p19,q19 or p9,q9 // q19,p19 by DIRAF:def 4;
then u,v // u1,v1 or u,v // v1,u1 by A1,Th2;
hence u,v '||' u1,v1;
end;
hence thesis by A2;
end;
theorem Th4:
for p,q,p1,q1 being Element of (the carrier of AMSpace(V,w,y)) st
p=u & q=v & p1=u1 & q1=v1 holds (p,q // p1,q1 iff u,v '||' u1,v1)
proof
let p,q,p1,q1 be Element of (the carrier of AMSpace(V,w,y)) such that
A1: p=u & q=v & p1=u1 & q1=v1;
A2: now
assume p,q // p1,q1;
then ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by A1,ANALMETR:22;
then u,v // u1,v1 or u,v // v1,u1 by ANALMETR:14;
hence u,v '||' u1,v1;
end;
now
assume u,v '||' u1,v1;
then u,v // u1,v1 or u,v // v1,u1;
then ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by ANALMETR:14;
hence p,q // p1,q1 by A1,ANALMETR:22;
end;
hence thesis by A2;
end;
definition
let V;
let u,v;
func u#v -> VECTOR of V means
:Def2:
it+it = u+v;
existence
proof
set y = u+v;
set w = (2")*y;
2" + 2" = 1;
then w+w = 1*y by RLVECT_1:def 6
.= y by RLVECT_1:def 8;
hence thesis;
end;
uniqueness
proof
let w,w1;
assume w+w = u+v & w1+w1 = u+v;
then 0.V = (w+w)-(w1+w1) by RLVECT_1:15
.= w+(w-(w1+w1)) by RLVECT_1:def 3
.= w+((w-w1)-w1) by RLVECT_1:27
.= (w+(w-w1))-w1 by RLVECT_1:def 3
.= (w-w1)+(w-w1) by RLVECT_1:def 3;
then w-w1 = 0.V by RLVECT_1:20;
hence thesis by RLVECT_1:21;
end;
commutativity;
idempotence;
end;
theorem Th5:
ex y st u#y=w
proof
take y = (-u)+(w+w);
u+y = (u+(-u))+(w+w) by RLVECT_1:def 3
.= 0.V+(w+w) by RLVECT_1:5
.= w+w by RLVECT_1:4;
hence thesis by Def2;
end;
theorem Th6:
(u#u1)#(v#v1)=(u#v)#(u1#v1)
proof
set p=u#u1, q=v#v1, r=u#v, s=u1#v1;
set x=p#q,y=r#s;
A1: now
let w;
w=1*w by RLVECT_1:def 8;
then (w+w)+(w+w) = (1+1)*w + ((1*w)+(1*w)) by RLVECT_1:def 6
.= (1+1)*w + (1+1)*w by RLVECT_1:def 6
.= ((1+1)+(1+1))*w by RLVECT_1:def 6;
hence (w+w)+(w+w) = 4*w;
end;
(x+x)+(x+x) = (x+x)+(p+q) by Def2
.= (p+q)+(p+q) by Def2
.= p+(q+(p+q)) by RLVECT_1:def 3
.= p+(p+(q+q)) by RLVECT_1:def 3
.= (p+p)+(q+q) by RLVECT_1:def 3
.= (p+p)+(v+v1) by Def2
.= (u+u1)+(v+v1) by Def2
.= u+(u1+(v+v1)) by RLVECT_1:def 3
.= u+(v+(v1+u1)) by RLVECT_1:def 3
.= (u+v)+(v1+u1) by RLVECT_1:def 3
.= (u+v)+(s+s) by Def2
.= (r+r)+(s+s) by Def2
.= r+(r+(s+s)) by RLVECT_1:def 3
.= r+(s+(s+r)) by RLVECT_1:def 3
.= (r+s)+(s+r) by RLVECT_1:def 3
.= (y+y)+(r+s) by Def2
.= (y+y)+(y+y) by Def2;
then 4*x = (y+y)+(y+y) by A1
.= 4*y by A1;
hence thesis by RLVECT_1:36;
end;
theorem Th7:
u#y=u#w implies y=w
proof
assume
A1: u#y=u#w;
set p=u#y;
u+y = p+p by Def2
.= u+w by A1,Def2;
hence thesis by RLVECT_1:8;
end;
theorem Th8:
u,v // y#u,y#v
proof
set p=y#u,r=y#v;
A1: y+u = p+p & y+v = r+r by Def2;
2*(r-p) = (1+1)*r - (1+1)*p by RLVECT_1:34
.= (1*r+1*r)-(1+1)*p by RLVECT_1:def 6
.= (1*r+1*r)-(1*p+1*p) by RLVECT_1:def 6
.= (r+1*r)-(1*p+1*p) by RLVECT_1:def 8
.= (r+r)-(1*p+1*p) by RLVECT_1:def 8
.= (r+r)-(p+1*p) by RLVECT_1:def 8
.= (y+v)-(y+u) by A1,RLVECT_1:def 8
.= v+(y-(y+u)) by RLVECT_1:def 3
.= v+((y-y)-u) by RLVECT_1:27
.= v+(0.V-u) by RLVECT_1:15
.= v-u by RLVECT_1:14
.= 1*(v-u) by RLVECT_1:def 8;
hence thesis by ANALOAF:def 1;
end;
theorem
u,v '||' w#u,w#v
by Th8;
theorem Th10:
2*(u#v-u) = v-u & 2*(v-u#v) = v-u
proof
set p=u#v;
A1: 2-1 =1;
A2: 2*(v-p) = 2*v-(1+1)*p by RLVECT_1:34
.= 2*v-(1*p+1*p) by RLVECT_1:def 6
.= 2*v - (1*p+p) by RLVECT_1:def 8
.= 2*v - (p+p) by RLVECT_1:def 8
.= 2*v - (u+v) by Def2
.= (2*v-v)-u by RLVECT_1:27
.= (2*v-1*v)-u by RLVECT_1:def 8
.= 1*v - u by A1,RLVECT_1:35
.= v-u by RLVECT_1:def 8;
A3: 1-2 = -1;
2*(p-u) = (1+1)*p - 2*u by RLVECT_1:34
.= (1*p+1*p) - 2*u by RLVECT_1:def 6
.= (p+1*p) - 2*u by RLVECT_1:def 8
.= (p+p) - 2*u by RLVECT_1:def 8
.= (u+v) - 2*u by Def2
.=v+(u-2*u) by RLVECT_1:def 3
.= v+(1*u-2*u) by RLVECT_1:def 8
.= v+(-1)*u by A3,RLVECT_1:35
.= v-u by RLVECT_1:16;
hence thesis by A2;
end;
theorem Th11:
u,u#v // u#v,v
proof
set p = u#v;
2*(p-u) = v-u by Th10
.= 2*(v-p) by Th10;
hence thesis by ANALOAF:def 1;
end;
theorem Th12:
u,v // u,u#v & u,v // u#v,v
proof
set p = u#v;
1*(v-u) = v-u by RLVECT_1:def 8
.= 2*(p-u) by Th10;
hence u,v // u,u#v by ANALOAF:def 1;
1*(v-u) = v-u by RLVECT_1:def 8
.= 2*(v-p) by Th10;
hence thesis by ANALOAF:def 1;
end;
Lm1: u,y // y,v implies v,y // y,u & u,y // u,v & y,v // u,v
proof
assume
A1: u,y // y,v;
then y,u // v,y by ANALOAF:12;
hence
A2: v,y // y,u by ANALOAF:12;
thus u,y // u,v by A1,ANALOAF:13;
v,y // v,u by A2,ANALOAF:13;
hence thesis by ANALOAF:12;
end;
theorem Th13:
u,y // y,v implies u#y,y // y,y#v
proof
set p=u#y, q=y#v;
u,p // p,y by Th11;
then p,y // u,y by Lm1;
then
A1: u,y // p,y by ANALOAF:12;
y,q // q,v by Th11;
then y,q // y,v by Lm1;
then
A2: y,v // y,q by ANALOAF:12;
assume
A3: u,y // y,v;
now
assume that
A4: u<>y and
A5: y<>v;
y,v // p,y by A3,A1,A4,ANALOAF:11;
hence thesis by A2,A5,ANALOAF:11;
end;
hence thesis by ANALOAF:9;
end;
theorem Th14:
u,v // u1,v1 implies u,v // (u#u1),(v#v1)
proof
assume
A1: u,v // u1,v1;
per cases;
suppose
u=v or u1 = v1;
hence thesis by Th8,ANALOAF:9;
end;
suppose
A2: u<>v & u1<>v1;
set p=u#u1,q=v#v1;
consider a,b such that
A3: 0<a & 0<b and
A4: a*(v-u) = b*(v1-u1) by A1,A2,ANALOAF:def 1;
A5: 0<a+b & 0<b*2 by A3,XREAL_1:34,129;
(b*2)*(q-p) = b*(2*(q-p)) by RLVECT_1:def 7
.= b*((1+1)*q - 2*p) by RLVECT_1:34
.= b*((1*q+1*q) - 2*p) by RLVECT_1:def 6
.= b*((q+1*q) - 2*p) by RLVECT_1:def 8
.= b*((q+q) - 2*p) by RLVECT_1:def 8
.= b*((v+v1) - 2*p) by Def2
.= b*(v+(v1 - (1+1)*p)) by RLVECT_1:def 3
.= b*(v+(v1 - (1*p+1*p))) by RLVECT_1:def 6
.= b*(v+(v1 - (p+1*p))) by RLVECT_1:def 8
.= b*(v+(v1 - (p+p))) by RLVECT_1:def 8
.= b*(v+(v1 - (u+u1))) by Def2
.= b*(v+((v1 - u1)-u)) by RLVECT_1:27
.= b*((v+(v1 - u1))-u) by RLVECT_1:def 3
.= b*((v1 - u1)+(v-u)) by RLVECT_1:def 3
.= a*(v - u)+b*(v-u) by A4,RLVECT_1:def 5
.= (a+b)*(v-u) by RLVECT_1:def 6;
hence thesis by A5,ANALOAF:def 1;
end;
end;
Lm2: u,v // u1,v1 implies u,v '||' (u#v1),(v#u1)
proof
assume
A1: u,v // u1,v1;
per cases;
suppose
u=v;
then u,v // (u#v1),(v#u1) by ANALOAF:9;
hence thesis;
end;
suppose
u1=v1;
then u,v // (u#v1),(v#u1) by Th8;
hence thesis;
end;
suppose
u<>v & u1<>v1;
then consider a,b such that
0<a and
A2: 0<b and
A3: a*(v-u) = b*(v1-u1) by A1,ANALOAF:def 1;
A4: b*(u1-v1) = b*(-(v1-u1)) by RLVECT_1:33
.= -(a*(v-u)) by A3,RLVECT_1:25
.= a*(-(v-u)) by RLVECT_1:25
.= (-a)*(v-u) by RLVECT_1:24;
set p=u#v1,q=v#u1, A=b*2,D=b-a;
A5: A<>0 by A2;
A*(q-p) = b*(2*(q-p)) by RLVECT_1:def 7
.= b*((1+1)*q - 2*p) by RLVECT_1:34
.= b*((1*q+1*q) - 2*p) by RLVECT_1:def 6
.= b*((q+1*q) - 2*p) by RLVECT_1:def 8
.= b*((q+q) - 2*p) by RLVECT_1:def 8
.= b*((v+u1) - 2*p) by Def2
.= b*(v+(u1 - (1+1)*p)) by RLVECT_1:def 3
.= b*(v+(u1 - (1*p+1*p))) by RLVECT_1:def 6
.= b*(v+(u1 - (p+1*p))) by RLVECT_1:def 8
.= b*(v+(u1 - (p+p))) by RLVECT_1:def 8
.= b*(v+(u1 - (u+v1))) by Def2
.= b*(v+((u1 - v1)-u)) by RLVECT_1:27
.= b*((v+(u1 - v1))-u) by RLVECT_1:def 3
.= b*((u1 - v1)+(v-u)) by RLVECT_1:def 3
.= (-a)*(v-u)+b*(v-u) by A4,RLVECT_1:def 5
.= (b+(-a))*(v-u) by RLVECT_1:def 6
.= D*(v-u);
then u,v // p,q or u,v // q,p by A5,ANALMETR:14;
hence thesis;
end;
end;
Lm3: u1#u2 = v1#v2 implies v1-u1 = -(v2-u2)
proof
set p=u1#u2;
A1: p+p = u1+u2 by Def2;
assume u1#u2=v1#v2;
then
A2: p+p = v1+v2 by Def2;
(v1-u1)+v2 = (v2+v1)-u1 by RLVECT_1:def 3
.= u2 by A1,A2,RLSUB_2:61;
then (v1-u1)+(v2-u2) = u2-u2 by RLVECT_1:def 3
.= 0.V by RLVECT_1:15;
hence thesis by RLVECT_1:6;
end;
Lm4: u,v,u1,v1 are_Ort_wrt w,y implies u,v,v1,u1 are_Ort_wrt w,y
proof
assume u,v,u1,v1 are_Ort_wrt w,y;
then v-u,v1-u1 are_Ort_wrt w,y by ANALMETR:def 3;
then
A1: v-u,(-1)*(v1-u1) are_Ort_wrt w,y by ANALMETR:7;
(-1)*(v1-u1) = -(v1-u1) by RLVECT_1:16
.= u1-v1 by RLVECT_1:33;
hence thesis by A1,ANALMETR:def 3;
end;
Lm5: u,v,u1,v1 are_Ort_wrt w,y implies u1,v1,u,v are_Ort_wrt w,y
proof
assume u,v,u1,v1 are_Ort_wrt w,y;
then v-u,v1-u1 are_Ort_wrt w,y by ANALMETR:def 3;
then v1-u1,v-u are_Ort_wrt w,y by ANALMETR:4;
hence thesis by ANALMETR:def 3;
end;
Lm6: Gen w,y implies u,v,u1,u1 are_Ort_wrt w,y
proof
A1: u1-u1 = 0.V by RLVECT_1:15;
assume Gen w,y;
then v-u,u1-u1 are_Ort_wrt w,y by A1,ANALMETR:5;
hence thesis by ANALMETR:def 3;
end;
Lm7: Gen w,y & u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y implies u
,v,v1,v2 are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y;
v-u,v1-w1 are_Ort_wrt w,y & v-u,v2-w1 are_Ort_wrt w,y by A2,ANALMETR:def 3;
then
A3: v-u,(v2-w1)-(v1-w1) are_Ort_wrt w,y by A1,ANALMETR:10;
(v2-w1)-(v1-w1) = v2-(w1+(v1-w1)) by RLVECT_1:27
.= v2-(v1-(w1-w1)) by RLVECT_1:29
.= v2-(v1-0.V) by RLVECT_1:15
.= v2-v1 by RLVECT_1:13;
hence thesis by A3,ANALMETR:def 3;
end;
Lm8: Gen w,y & u,v,u,v are_Ort_wrt w,y implies u=v
proof
assume that
A1: Gen w,y and
A2: u,v,u,v are_Ort_wrt w,y;
v-u,v-u are_Ort_wrt w,y by A2,ANALMETR:def 3;
then v-u = 0.V by A1,ANALMETR:11;
hence thesis by RLVECT_1:21;
end;
Lm9: Gen w,y implies u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y
proof
A1: u1-u1 = 0.V by RLVECT_1:15;
assume Gen w,y;
then v-u,u1-u1 are_Ort_wrt w,y by A1,ANALMETR:5;
hence u,v,u1,u1 are_Ort_wrt w,y by ANALMETR:def 3;
hence thesis by Lm5;
end;
Lm10: Gen w,y & (u1,v1 '||' u,v or u,v '||' u1,v1) & (u2,v2,u,v are_Ort_wrt w,
y or u,v,u2,v2 are_Ort_wrt w,y) & u<>v implies u1,v1,u2,v2 are_Ort_wrt w,y & u2
,v2,u1,v1 are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u1,v1 '||' u,v or u,v '||' u1,v1 and
A3: u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y and
A4: u<>v;
reconsider p9=u,q9=v,p19=u1,q19=v1,p29=u2,q29=v2 as Element of the carrier
of AMSpace(V,w,y) by ANALMETR:19;
reconsider S=AMSpace(V,w,y) as OrtAfSp by A1,ANALMETR:33;
reconsider p=p9,q=q9,p1=p19,q1=q19,p2=p29,q2=q29 as Element of S;
A5: p2,q2 _|_ p,q or p,q _|_ p2,q2 by A3,ANALMETR:21;
p1,q1 // p,q or p,q // p1,q1 by A2,Th4;
then p1,q1 _|_ p2,q2 & p2,q2 _|_ p1,q1 by A4,A5,ANALMETR:62;
hence thesis by ANALMETR:21;
end;
definition
let V;
let w,y,u,u1,v,v1;
pred u,u1,v,v1 are_DTr_wrt w,y means
u,u1 // v,v1 & u,u1,u#u1,v#v1
are_Ort_wrt w,y & v,v1,u#u1,v#v1 are_Ort_wrt w,y;
end;
theorem
Gen w,y implies u,u,v,v are_DTr_wrt w,y
by Lm5,Lm6,ANALOAF:9;
theorem
Gen w,y implies u,v,u,v are_DTr_wrt w,y
by Lm6,ANALOAF:8;
theorem Th17:
u,v,v,u are_DTr_wrt w,y implies u=v by ANALOAF:10;
theorem Th18:
Gen w,y & v1,u,u,v2 are_DTr_wrt w,y implies v1=u & u=v2
proof
assume that
A1: Gen w,y and
A2: v1,u,u,v2 are_DTr_wrt w,y;
set a=v1#u, b=u#v2;
A3: v1,u,a,b are_Ort_wrt w,y by A2;
A4: u,v2,a,b are_Ort_wrt w,y by A2;
A5: v1,u // u,v2 by A2;
per cases;
suppose
v1 = v2;
hence thesis by A2,Th17;
end;
suppose
v1<>v2;
then
A6: a<>b by Th7;
u,v2 // u,b by Th12;
then
A7: u,v2 '||' u,b;
A8: a,u // u,b by A5,Th13;
then u,b // a,b by Lm1;
then
A9: u,b '||' a,b;
A10: u=v2
proof
assume
A11: u<>v2;
A12: u<>b
proof
assume u=b;
then u#v2=u#u;
hence contradiction by A11,Th7;
end;
u,b,a,b are_Ort_wrt w,y by A1,A4,A7,A11,Lm10;
then u,b,u,b are_Ort_wrt w, y by A1,A6,A9,Lm10;
hence contradiction by A1,A12,Lm8;
end;
v1,u // a,u by Th12;
then
A13: v1,u '||' a,u;
a,u // a,b by A8,Lm1;
then
A14: a,u '||' a,b;
v1=u
proof
assume
A15: v1<>u;
A16: u<>a
proof
assume u=a;
then v1#u=u#u;
hence contradiction by A15,Th7;
end;
a,u,a,b are_Ort_wrt w,y by A1,A3,A13,A15,Lm10;
then a,u,a,u are_Ort_wrt w, y by A1,A6,A14,Lm10;
hence contradiction by A1,A16,Lm8;
end;
hence thesis by A10;
end;
end;
theorem Th19:
Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y
& u<>v implies u1,v1,u2,v2 are_DTr_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y and
A3: u,v,u2,v2 are_DTr_wrt w,y and
A4: u<>v;
set a=u1#v1, b=u2#v2;
u,v,u#v,u1#v1 are_Ort_wrt w,y & u,v,u#v,u2#v2 are_Ort_wrt w,y by A2,A3;
then
A5: u,v,a,b are_Ort_wrt w,y by A1,Lm7;
A6: u,v // u2,v2 by A3;
then u,v '||' u2,v2;
then
A7: u2,v2,a,b are_Ort_wrt w,y by A1,A4,A5,Lm10;
A8: u,v // u1,v1 by A2;
then u,v '||' u1,v1;
then
A9: u1,v1,a,b are_Ort_wrt w,y by A1,A4,A5,Lm10;
u1,v1 // u2,v2 by A4,A8,A6,ANALOAF:11;
hence thesis by A9,A7;
end;
theorem Th20:
Gen w,y implies ex t being VECTOR of V st (u,v,u1,t are_DTr_wrt
w,y or u,v,t,u1 are_DTr_wrt w,y)
proof
assume
A1: Gen w,y;
set a=u#v;
per cases;
suppose
A2: u=v;
A3: u1,u1,u#u,u1#u1 are_Ort_wrt w,y by A1,Lm5,Lm6;
u,u // u1,u1 & u,u,u#u,u1#u1 are_Ort_wrt w,y by A1,Lm5,Lm6,ANALOAF:9;
then u,u,u1,u1 are_DTr_wrt w,y by A3;
hence thesis by A2;
end;
suppose
A4: u<>v;
a<>u
proof
assume a=u;
then u#u = u#v;
hence contradiction by A4,Th7;
end;
then u-a<>0.V by RLVECT_1:21;
then consider r being Real such that
A5: (u1-a)-r*(u-a),u-a are_Ort_wrt w,y by A1,ANALMETR:13;
set b = u1-r*(u-a);
set t = 2*b-u1;
u1+t = (1+1)*b by RLSUB_2:61
.= 1*b+1*b by RLVECT_1:def 6
.= b+1*b by RLVECT_1:def 8
.= b+b by RLVECT_1:def 8;
then
A6: u1#t = b by Def2;
u1-b = (u1-u1)+r*(u-a) by RLVECT_1:29
.= 0.V + r*(u-a) by RLVECT_1:15
.= r*(u-a) by RLVECT_1:4;
then
A7: u1-t = 2*(r*(u-a)) by A6,Th10
.= (2*r)*(u-a) by RLVECT_1:def 7;
A8: u1-(a+r*(u-a)) = (u1-r*(u-a))-a by RLVECT_1:27;
then b-a,u-a are_Ort_wrt w,y by A5,RLVECT_1:27;
then b-a,u1-t are_Ort_wrt w,y by A7,ANALMETR:7;
then
A9: a,b,t,u1 are_Ort_wrt w,y by ANALMETR:def 3;
then
A10: t,u1,u#v,t#u1 are_Ort_wrt w,y by A6,Lm5;
A11: u-v = 2*(u-u#v) by Th10;
then u1-t = r*(u-v) by A7,RLVECT_1:def 7;
then r*(u-v) = 1*(u1-t) by RLVECT_1:def 8;
then v,u // t,u1 or v,u // u1,t by ANALMETR:14;
then
A12: u,v // u1,t or u,v // t,u1 by ANALOAF:12;
a,b,u1,t are_Ort_wrt w,y by A9,Lm4;
then
A13: u1,t,u#v,u1#t are_Ort_wrt w,y by A6,Lm5;
b-a = (u1-a)-r*(u-a) by A8,RLVECT_1:27;
then b-a,u-v are_Ort_wrt w,y by A5,A11,ANALMETR:7;
then a,b,v,u are_Ort_wrt w,y by ANALMETR:def 3;
then a,b,u,v are_Ort_wrt w,y by Lm4;
then u,v,u#v,u1#t are_Ort_wrt w,y by A6,Lm5;
then u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y by A13,A10,A12;
hence thesis;
end;
end;
theorem Th21:
u,v,u1,v1 are_DTr_wrt w,y implies u1,v1,u,v are_DTr_wrt w,y
by ANALOAF:12,Lm4;
theorem Th22:
u,v,u1,v1 are_DTr_wrt w,y implies v,u,v1,u1 are_DTr_wrt w,y
proof
assume
A1: u,v,u1,v1 are_DTr_wrt w,y;
then u,v // u1,v1;
then
A2: v,u // v1,u1 by ANALOAF:12;
A3: now
let u,u9,v,v9 be VECTOR of V;
assume u,u9,v,v9 are_Ort_wrt w,y;
then v,v9,u,u9 are_Ort_wrt w,y by Lm5;
then v,v9,u9,u are_Ort_wrt w,y by Lm4;
hence u9,u,v,v9 are_Ort_wrt w,y by Lm5;
end;
u1,v1,u#v,u1#v1 are_Ort_wrt w,y by A1;
then
A4: v1,u1,v#u,v1#u1 are_Ort_wrt w,y by A3;
u,v,u#v,u1#v1 are_Ort_wrt w,y by A1;
then v,u,v#u,v1#u1 are_Ort_wrt w,y by A3;
hence thesis by A2,A4;
end;
Lm11: Gen w,y & u<>v & u,v '||' u,u1 & u,v '||' u,v1 & u,v '||' u,u2 & u,v
'||' u,v2 implies u1,v1 '||' u2,v2
proof
assume that
A1: Gen w,y and
A2: u<>v and
A3: u,v '||' u,u1 and
A4: u,v '||' u,v1 and
A5: u,v '||' u,u2 and
A6: u,v '||' u,v2;
reconsider p9=u,q9=v,p19=u1,q19=v1,p29=u2,q29=v2 as Element of Lambda(
OASpace(V)) by ANALMETR:16;
reconsider S9 = OASpace(V) as OAffinSpace by A1,Th1;
reconsider S = Lambda(S9) as AffinSpace by DIRAF:41;
reconsider p=p9,q=q9,p1=p19,q1=q19,p2=p29,q2=q29 as Element of the carrier
of S;
p,q // p,p1 by A1,A3,Th3;
then
A7: LIN p,q,p1 by AFF_1:def 1;
p,q // p,q1 by A1,A4,Th3;
then
A8: LIN p,q,q1 by AFF_1:def 1;
p,q // p, q2 by A1,A6,Th3;
then LIN p,q,q2 by AFF_1:def 1;
then
A9: LIN p1,q1,q2 by A2,A7,A8,AFF_1:8;
p,q // p,p2 by A1,A5,Th3;
then LIN p,q,p2 by AFF_1:def 1;
then LIN p1,q1,p2 by A2,A7,A8,AFF_1:8;
then p1,q1 // p2,q2 by A9,AFF_1:10;
hence thesis by A1,Th3;
end;
theorem Th23:
Gen w,y & v,u1,v,u2 are_DTr_wrt w,y implies u1=u2
proof
assume that
A1: Gen w,y and
A2: v,u1,v,u2 are_DTr_wrt w,y;
A3: v,u1,v#u1,v#u2 are_Ort_wrt w,y by A2;
A4: v,u2,v#u1,v#u2 are_Ort_wrt w,y by A2;
v,u1 // v,u1 by ANALOAF:8;
then
A5: v,u1 '||' v,u1;
set b=v#u1, c = v#u2;
A6: v,u1 // v,b by Th12;
then
A7: v,u1 '||' v,b;
A8: v,u1 // v,u2 by A2;
v,u2 // v,b
proof
per cases;
suppose
v=b;
hence thesis by ANALOAF:9;
end;
suppose
v<>b;
then v<>u1;
hence thesis by A8,A6,ANALOAF:11;
end;
end;
then
A9: v,u2 '||' v,b;
v,u2 // v,v by ANALOAF:9;
then
A10: v,u2 '||' v,v;
A11: v,u2 // v,c by Th12;
then
A12: v,u2 '||' v,c;
A13: v,u2 // v,u1 by A8,ANALOAF:12;
v,u1 // v,c
proof
per cases;
suppose
v=c;
hence thesis by ANALOAF:9;
end;
suppose
v<>c;
then v<>u2;
hence thesis by A13,A11,ANALOAF:11;
end;
end;
then
A14: v,u1 '||' v,c;
v,u2 // v,u2 by ANALOAF:8;
then
A15: v,u2 '||' v,u2;
v,u1 // v,v by ANALOAF:9;
then
A16: v,u1 '||' v,v;
assume
A17: u1<>u2;
per cases by A17;
suppose
A18: v<>u1;
then v,u1 '||' b,c by A1,A7,A5,A16,A14,Lm11;
then b,c,b,c are_Ort_wrt w,y by A1,A3,A18,Lm10;
hence thesis by A1,A17,Lm8,Th7;
end;
suppose
A19: v<>u2;
then v,u2 '||' b,c by A1,A12,A15,A10,A9,Lm11;
then b,c,b,c are_Ort_wrt w,y by A1,A4,A19,Lm10;
hence thesis by A1,A17,Lm8,Th7;
end;
end;
theorem Th24:
Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y
implies (u=v or v1=v2)
proof
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y;
assume u<>v;
then u1,v1,u1,v2 are_DTr_wrt w,y by A1,A2,Th19;
hence thesis by A1,Th23;
end;
theorem Th25:
Gen w,y & u<>u1 & u,u1,v,v1 are_DTr_wrt w,y & (u,u1,v,v2
are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y) implies v1=v2
proof
assume that
A1: Gen w,y and
A2: u<>u1 & u,u1,v,v1 are_DTr_wrt w,y and
A3: u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y;
now
assume u,u1,v2,v are_DTr_wrt w,y;
then
A4: v2,v,v,v1 are_DTr_wrt w,y by A1,A2,Th19;
then v=v2 by A1,Th18;
hence thesis by A1,A4,Th18;
end;
hence thesis by A1,A2,A3,Th24;
end;
theorem Th26:
Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies u,v,(u#u1),(v#v1) are_DTr_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y;
set p=u#u1,q=v#v1,r=u#v,s=u1#v1;
A3: u=v & u1=v1 implies p,q,r,(p#q) are_Ort_wrt w,y by A1,Lm9;
p#q = r#s by Th6;
then r,s // r,p#q by Th12;
then
A4: r,s '||' r,p#q;
u,v,r,s are_Ort_wrt w,y & u1,v1,r,s are_Ort_wrt w,y by A2;
then
A5: r<>s implies u1,v1,r,(p#q) are_Ort_wrt w,y & u,v,r,(p#q) are_Ort_wrt w,
y by A1,A4,Lm10;
A6: now
assume r=s;
then r=r#s .= p#q by Th6;
hence u1,v1,r,(p#q) are_Ort_wrt w,y & u,v,r,(p#q) are_Ort_wrt w,y by A1,Lm9
;
end;
A7: u,v // u1,v1 by A2;
then u1,v1 // u,v by ANALOAF:12;
then u1,v1 // (u1#u),(v1#v) by Th14;
then u1,v1 '||' p,q;
then
A8: u=v & u1<>v1 implies p,q,r,(p#q) are_Ort_wrt w,y by A1,A6,A5,Lm10;
A9: u,v // (u#u1),(v#v1) by A7,Th14;
then u,v '||' p,q;
then u<>v implies p,q,r,(p#q) are_Ort_wrt w,y by A1,A6,A5,Lm10;
hence thesis by A9,A6,A5,A8,A3;
end;
theorem Th27:
Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies (u,v,(u#v1),(v#u1)
are_DTr_wrt w,y or u,v,(v#u1),(u#v1) are_DTr_wrt w,y)
proof
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y;
set p=u#v1,q=v#u1,r=u#v,s=u1#v1;
A3: u,v,r,s are_Ort_wrt w,y by A2;
A4: p#q = r#s by Th6;
then r,s // r,p#q by Th12;
then
A5: r,s '||' r,p#q;
u,v // u1,v1 by A2;
then
A6: u,v '||' p,q by Lm2;
then
A7: u,v // p,q or u,v // q,p;
per cases;
suppose
u=v;
hence thesis by A1,A2,Th26;
end;
suppose that
A8: u<>v;
per cases;
suppose
A9: r=s;
then
A10: q,p,r,(q#p) are_Ort_wrt w,y by A1,A4,Lm9;
u,v,r,(p#q) are_Ort_wrt w,y & p,q,r,(p#q) are_Ort_wrt w,y by A1,A4,A9,Lm9
;
hence thesis by A7,A10;
end;
suppose
r<>s;
then
A11: u,v,r,(p#q) are_Ort_wrt w,y by A1,A3,A5,Lm10;
then r,(p#q),p,q are_Ort_wrt w,y by A1,A6,A8,Lm10;
then r,(p#q),q,p are_Ort_wrt w,y by Lm4;
then
A12: q,p,r,(q#p) are_Ort_wrt w,y by Lm5;
p,q,r,(p#q) are_Ort_wrt w,y by A1,A6,A8,A11,Lm10;
hence thesis by A7,A11,A12;
end;
end;
end;
theorem Th28:
for u,u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of V holds ( u=u1#t1
& u=u2#t2 & u=v1#w1 & u=v2#w2 & u1,u2,v1,v2 are_DTr_wrt w,y implies t1,t2,w1,w2
are_DTr_wrt w,y)
proof
let u,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V;
assume that
A1: u=u1#t1 & u=u2#t2 and
A2: u=v1#w1 & u=v2#w2 and
A3: u1,u2,v1,v2 are_DTr_wrt w,y;
A4: u1,u2 // v1,v2 by A3;
set p=u1#u2,q=v1#v2,r=t1#t2,s=w1#w2;
A5: q#s = u#u by A2,Th6
.=u;
p#r = u#u by A1,Th6
.=u;
then
A6: s-r = -(q-p) by A5,Lm3
.= (-1)*(q-p) by RLVECT_1:16;
A7: u2-u1 = -(t2-t1) & v2-v1 = -(w2-w1) by A1,A2,Lm3;
A8: t1,t2 // w1,w2
proof
per cases;
suppose
u1=u2;
then t1=t2 by A1,Th7;
hence thesis by ANALOAF:9;
end;
suppose
v1=v2;
then w1=w2 by A2,Th7;
hence thesis by ANALOAF:9;
end;
suppose
u1<>u2 & v1<>v2;
then consider a,b such that
A9: 0<a & 0<b and
A10: a*(u2-u1)=b*(v2-v1) by A4,ANALOAF:def 1;
a*(t2-t1) = a*(-(-(t2-t1))) by RLVECT_1:17
.= -(b*(-(w2-w1))) by A7,A10,RLVECT_1:25
.= b*(-(-(w2-w1))) by RLVECT_1:25
.= b*(w2-w1) by RLVECT_1:17;
hence thesis by A9,ANALOAF:def 1;
end;
end;
w2-w1 = -(v2-v1) by A2,Lm3;
then
A11: w2-w1 = (-1)*(v2-v1) by RLVECT_1:16;
v1,v2,p,q are_Ort_wrt w,y by A3;
then v2-v1,q-p are_Ort_wrt w,y by ANALMETR:def 3;
then w2-w1,s-r are_Ort_wrt w,y by A6,A11,ANALMETR:6;
then
A12: w1,w2,r,s are_Ort_wrt w,y by ANALMETR:def 3;
t2-t1 = -(u2-u1) by A1,Lm3;
then
A13: t2-t1 = (-1)*(u2-u1) by RLVECT_1:16;
u1,u2,p,q are_Ort_wrt w,y by A3;
then u2-u1,q-p are_Ort_wrt w,y by ANALMETR:def 3;
then t2-t1,s-r are_Ort_wrt w,y by A6,A13,ANALMETR:6;
then t1,t2,r,s are_Ort_wrt w,y by ANALMETR:def 3;
hence thesis by A8,A12;
end;
Lm12: v1 = b1*w + b2*y & v2 = c1*w + c2*y implies v1 + v2 = (b1 + c1)*w + (b2
+ c2)*y & v1 - v2 = (b1 - c1)*w + (b2 - c2)*y
proof
assume
A1: v1 = b1*w + b2*y & v2 = c1*w + c2*y;
hence v1 + v2 = ((b1*w + b2*y) + c1*w) + c2*y by RLVECT_1:def 3
.= ((b1*w + c1*w) + b2*y) + c2*y by RLVECT_1:def 3
.= ((b1 + c1)*w + b2*y) + c2*y by RLVECT_1:def 6
.= (b1 + c1)*w + (b2*y + c2*y) by RLVECT_1:def 3
.= (b1 + c1)*w + (b2 + c2)*y by RLVECT_1:def 6;
thus v1 - v2 = (b1*w + b2*y)+(-(c1*w) + -(c2*y)) by A1,RLVECT_1:31
.= (b1*w + b2*y)+(c1*(-w) + -(c2*y)) by RLVECT_1:25
.= (b1*w + b2*y)+(c1*(-w) + c2*(-y)) by RLVECT_1:25
.= (b1*w + b2*y)+((-c1)*w + c2*(-y)) by RLVECT_1:24
.= (b1*w + b2*y)+((-c1)*w + (-c2)*y) by RLVECT_1:24
.= ((b1*w + b2*y) + (-c1)*w) + (-c2)*y by RLVECT_1:def 3
.= ((b1*w + (-c1)*w) + b2*y) + (-c2)*y by RLVECT_1:def 3
.= ((b1 + (-c1))*w + b2*y) + (-c2)*y by RLVECT_1:def 6
.= (b1 + (-c1))*w + (b2*y + (-c2)*y) by RLVECT_1:def 3
.= (b1 - c1)*w + (b2 + (-c2))*y by RLVECT_1:def 6
.= (b1 - c1)*w + (b2 - c2)*y;
end;
Lm13: v = b1*w + b2*y implies a*v = (a*b1)*w + (a*b2)*y
proof
assume v= b1*w + b2*y;
hence a*v = a*(b1*w) + a*(b2*y) by RLVECT_1:def 5
.= (a*b1)*w + a*(b2*y) by RLVECT_1:def 7
.= (a*b1)*w + (a*b2)*y by RLVECT_1:def 7;
end;
Lm14: Gen w,y & a1*w + a2*y = b1*w + b2*y implies a1=b1 & a2=b2
proof
assume that
A1: Gen w,y and
A2: a1*w+a2*y=b1*w+b2*y;
0.V = (a1*w+a2*y)-(b1*w+b2*y) by A2,RLVECT_1:15
.= (a1-b1)*w+(a2-b2)*y by Lm12;
then -b1 + a1 =0 & -b2 + a2 = 0 by A1,ANALMETR:def 1;
hence thesis;
end;
definition
let V,w,y,u such that
A1: Gen w,y;
func pr1(w,y,u) -> Real means
:Def4:
ex b st u=it*w+b*y;
existence
by A1,ANALMETR:def 1;
uniqueness by A1,Lm14;
end;
definition
let V,w,y,u such that
A1: Gen w,y;
func pr2(w,y,u) -> Real means
:Def5:
ex a st u=a*w+it*y;
existence
proof
consider a,b such that
A2: u = a*w+b*y by A1,ANALMETR:def 1;
take b;
thus thesis by A2;
end;
uniqueness by A1,Lm14;
end;
Lm15: Gen w,y implies u = pr1(w,y,u)*w + pr2(w,y,u)*y
proof
assume
A1: Gen w,y;
then consider b such that
A2: u = (pr1(w,y,u))*w + b*y by Def4;
thus thesis by A1,Def5,A2;
end;
Lm16: Gen w,y & u=a*w+b*y implies a=pr1(w,y,u) & b=pr2(w,y,u)
proof
assume that
A1: Gen w,y and
A2: u=a*w+b*y;
u = pr1(w,y,u)*w + pr2(w,y,u)*y by A1,Lm15;
hence thesis by A1,A2,Lm14;
end;
Lm17: Gen w,y implies pr1(w,y,u+v) = pr1(w,y,u)+pr1(w,y,v) & pr2(w,y,u+v) =
pr2(w,y,u)+pr2(w,y,v) & pr1(w,y,u-v) = pr1(w,y,u)-pr1(w,y,v) & pr2(w,y,u-v) =
pr2(w,y,u)-pr2(w,y,v) & pr1(w,y,a*u) = a*pr1(w,y,u) & pr2(w,y,a*u) = a*pr2(w,y,
u)
proof
set p1u = pr1(w,y,u), p2u = pr2(w,y,u), p1v = pr1(w,y,v), p2v = pr2(w,y,v);
assume
A1: Gen w,y;
then
A2: u = p1u*w + p2u*y by Lm15;
A3: v = p1v*w + p2v*y by A1,Lm15;
then u + v = (p1u*w + p2u*y + p1v*w) + p2v*y by A2,RLVECT_1:def 3
.= ((p1u*w + p1v*w) + p2u*y) + p2v*y by RLVECT_1:def 3
.= (p1u*w + p1v*w) + (p2u*y + p2v*y) by RLVECT_1:def 3
.= (p1u + p1v)*w + (p2u*y + p2v*y) by RLVECT_1:def 6
.= (p1u + p1v)*w + (p2u + p2v)*y by RLVECT_1:def 6;
hence pr1(w,y,u+v) = p1u + p1v & pr2(w,y,u+v) = p2u + p2v by A1,Lm16;
u - v = (p1u - p1v)*w + (p2u - p2v)*y by A2,A3,Lm12;
hence pr1(w,y,u-v) = p1u - p1v & pr2(w,y,u-v) = p2u - p2v by A1,Lm16;
a*u = (a*p1u)*w + (a*p2u)*y by A2,Lm13;
hence thesis by A1,Lm16;
end;
Lm18: Gen w,y implies 2*pr1(w,y,u#v) = pr1(w,y,u)+pr1(w,y,v) & 2*pr2(w,y,u#v)
= pr2(w,y,u)+pr2(w,y,v)
proof
assume
A1: Gen w,y;
set p=u#v;
2*(u#v) = (1+1)*p .= 1*p + 1*p by RLVECT_1:def 6
.= p + 1*p by RLVECT_1:def 8
.= p+p by RLVECT_1:def 8
.= u+v by Def2;
then 2*pr1(w,y,u#v) = pr1(w,y,u+v) & 2*pr2(w,y,u#v) = pr2(w,y,u+v) by A1,Lm17
;
hence thesis by A1,Lm17;
end;
Lm19: -u + -v = -(u+v)
proof
(u+v)+(-u + -v) = ((u+v)+ -u) + -v by RLVECT_1:def 3
.= (v+(u+ -u)) + -v by RLVECT_1:def 3
.= (v+0.V) + -v by RLVECT_1:5
.= v + -v by RLVECT_1:4
.= 0.V by RLVECT_1:5;
hence thesis by RLVECT_1:def 10;
end;
Lm20: (u2 + a2*v) - (u1 + a1*v) = (u2-u1) + (a2-a1)*v
proof
thus (u2+a2*v) - (u1+a1*v) = ((u2+a2*v) -u1)-a1*v by RLVECT_1:27
.= (a2*v+(u2 -u1))-a1*v by RLVECT_1:def 3
.= (u2-u1)+(a2*v-a1*v) by RLVECT_1:def 3
.= (u2 - u1)+(a2-a1)*v by RLVECT_1:35;
end;
definition
let V,w,y,u,v;
func PProJ(w,y,u,v) -> Real equals
pr1(w,y,u)*pr1(w,y,v) + pr2(w,y,u)*pr2(w,y,v);
correctness;
end;
theorem
for u,v holds PProJ(w,y,u,v) = PProJ(w,y,v,u);
theorem Th30:
Gen w,y implies for u,v,v1 holds PProJ(w,y,u,v+v1)=PProJ(w,y,u,v
)+PProJ(w,y,u,v1) & PProJ(w,y,u,v-v1)=PProJ(w,y,u,v)-PProJ(w,y,u,v1) & PProJ(w,
y,v-v1,u)=PProJ(w,y,v,u)-PProJ(w,y,v1,u) & PProJ(w,y,v+v1,u)=PProJ(w,y,v,u)+
PProJ(w,y,v1,u)
proof
assume
A1: Gen w,y;
let u,v,v1 be VECTOR of V;
A2: now
let u,v,v1 be VECTOR of V;
A3: PProJ(w,y,u,v-v1) = pr1(w,y,u)*(pr1(w,y,v)-pr1(w,y,v1))+pr2(w,y,u)*pr2
(w,y,v-v1) by A1,Lm17
.= pr1(w,y,u)*(pr1(w,y,v)-pr1(w,y,v1))+pr2(w,y,u)*(pr2(w,y,v)-pr2(w,y,
v1)) by A1,Lm17
.= PProJ(w,y,u,v)-PProJ(w,y,u,v1);
PProJ(w,y,u,v+v1) = pr1(w,y,u)*(pr1(w,y,v)+pr1(w,y,v1))+pr2(w,y,u)*pr2
(w,y,v+v1) by A1,Lm17
.= pr1(w,y,u)*(pr1(w,y,v)+pr1(w,y,v1))+pr2(w,y,u)*(pr2(w,y,v)+pr2(w,y,
v1)) by A1,Lm17
.= PProJ(w,y,u,v)+PProJ(w,y,u,v1);
hence
PProJ(w,y,u,v+v1)=PProJ(w,y,u,v)+PProJ(w,y,u,v1) & PProJ(w,y,u,v-v1)=
PProJ(w,y,u,v)-PProJ(w,y,u,v1) by A3;
end;
hence PProJ(w,y,u,v+v1) = PProJ(w,y,u,v)+PProJ(w,y,u,v1) & PProJ(w,y,u,v-v1)
= PProJ(w,y,u,v)-PProJ(w,y,u,v1);
thus PProJ(w,y,v-v1,u) = PProJ(w,y,u,v-v1)
.= PProJ(w,y,u,v)-PProJ (w,y,u,v1) by A2
.= PProJ(w,y,v,u)-PProJ (w,y,v1,u);
thus PProJ(w,y,v+v1,u)= PProJ(w,y,u,v+v1)
.= PProJ(w,y,u,v)+PProJ (w,y,u,v1) by A2
.= PProJ(w,y,v,u)+PProJ (w,y,v1,u);
end;
theorem Th31:
Gen w,y implies for u,v being VECTOR of V, a being Real holds
PProJ(w,y,a*u,v)=a*PProJ(w,y,u,v) & PProJ(w,y,u,a*v)=a*PProJ(w,y,u,v) & PProJ(w
,y,a*u,v)=PProJ(w,y,u,v)*a & PProJ(w,y,u,a*v)=PProJ(w,y,u,v)*a
proof
assume
A1: Gen w,y;
A2: now
let u,v be VECTOR of V,a be Real;
PProJ(w,y,a*u,v) = (a*pr1(w,y,u))*pr1(w,y,v)+pr2(w,y,a*u)*pr2(w,y,v)
by A1,Lm17
.= (a*pr1(w,y,u))*pr1(w,y,v)+(a*pr2(w,y,u))*pr2(w,y,v) by A1,Lm17
.= a*PProJ(w,y,u,v);
hence PProJ(w,y,a*u,v) = a*PProJ(w,y,u,v);
end;
let u,v be VECTOR of V,a be Real;
thus PProJ(w,y,a*u,v) = a*PProJ(w,y,u,v) by A2;
thus PProJ(w,y,u,a*v) = PProJ(w,y,a*v,u) .= a*PProJ(w,y,v,u) by A2
.= a*PProJ(w,y,u,v);
thus PProJ(w,y,a*u,v) = PProJ(w,y,u,v)*a by A2;
thus PProJ(w,y,u,a*v) = PProJ(w,y,a*v,u) .= a*PProJ(w,y,v,u) by A2
.= PProJ(w,y,u,v)*a;
end;
theorem Th32:
Gen w,y implies for u,v being VECTOR of V holds (u,v are_Ort_wrt
w,y iff PProJ(w,y,u,v)=0)
proof
assume
A1: Gen w,y;
let u,v be VECTOR of V;
set a1=pr1(w,y,u),a2=pr2(w,y,u),b1=pr1(w,y,v),b2=pr2(w,y,v);
u = a1*w+a2*y & v = b1*w+b2*y by A1,Lm15;
hence thesis by A1,ANALMETR:1,def 2;
end;
theorem Th33:
Gen w,y implies for u,v,u1,v1 being VECTOR of V holds (u,v,u1,v1
are_Ort_wrt w,y iff PProJ (w,y,v-u,v1-u1)=0)
proof
assume
A1: Gen w,y;
let u,v,u1,v1 be VECTOR of V;
u,v,u1,v1 are_Ort_wrt w,y iff v-u,v1-u1 are_Ort_wrt w,y by ANALMETR:def 3;
hence thesis by A1,Th32;
end;
theorem Th34:
Gen w,y implies for u,v,v1 being VECTOR of V holds 2*PProJ(w,y,u
,v#v1) = PProJ(w,y,u,v)+PProJ(w,y,u,v1)
proof
assume
A1: Gen w,y;
let u,v,v1 be VECTOR of V;
set a1=pr1(w,y,u),a2=pr2(w,y,u),b1=pr1(w,y,v),b2=pr2(w,y,v), c1=pr1(w,y,v1),
c2=pr2(w,y,v1);
thus 2*PProJ(w,y,u,v#v1) = a1*(2*pr1(w,y,v#v1))+ 2*(a2*pr2(w,y,v#v1))
.= a1*(b1+c1)+ a2*(2*pr2(w,y,v#v1)) by A1,Lm18
.= a1*(b1+c1)+ a2*(b2+c2) by A1,Lm18
.= PProJ(w,y,u,v)+PProJ(w,y,u,v1);
end;
theorem Th35:
Gen w,y implies for u,v being VECTOR of V st u<>v holds PProJ(w,
y,u-v,u-v) <> 0
proof
assume
A1: Gen w,y;
let u,v be VECTOR of V;
assume
A2: u<>v;
assume PProJ(w,y,u-v,u-v) = 0;
then u-v,u-v are_Ort_wrt w,y by A1,Th32;
then u-v = 0.V by A1,ANALMETR:11;
hence contradiction by A2,RLVECT_1:21;
end;
theorem Th36:
Gen w,y implies for p,q,u,v,v9 being VECTOR of V,
A being Real
st p,q,u,v are_DTr_wrt w,y & p<>q & A = (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u
))*(PProJ(w,y,p-q,p-q))" & v9=u+A*(p-q) holds v=v9
proof
assume
A1: Gen w,y;
let p,q,u,v,v9 be VECTOR of V,A be Real;
assume that
A2: p,q,u,v are_DTr_wrt w,y and
A3: p<>q and
A4: A = (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))" and
A5: v9=u+A*(p-q);
A6: PProJ(w,y,p-q,p-q) <> 0 by A1,A3,Th35;
A7: PProJ(w,y,p-q,A*(p-q)) = ((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(
PProJ(w,y,p-q,p-q))")*PProJ (w,y,p-q,p-q) by A1,A4,Th31
.= (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*((PProJ(w,y,p-q,p-q))"*PProJ
(w,y,p-q,p-q))
.= (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*1 by A6,XCMPLX_0:def 7
.= PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u);
set s=p#q;
set X=PProJ(w,y,p-q,(v9#u)-s);
2*X = 2*(PProJ(w,y,p-q,v9#u)-PProJ(w,y,p-q,p#q)) by A1,Th30
.= 2*PProJ(w,y,p-q,v9#u)-2*PProJ(w,y,p-q,p#q)
.= (PProJ(w,y,p-q,v9)+PProJ(w,y,p-q,u))-2*PProJ(w,y,p-q,p#q) by A1,Th34
.= (PProJ(w,y,p-q,v9)+PProJ(w,y,p-q,u))-(PProJ(w,y,p-q,p)+PProJ (w,y,p-q
,q)) by A1,Th34
.= (PProJ(w,y,p-q,u+A*(p-q)) + PProJ(w,y,p-q,u)) - PProJ (w,y,p-q,p+q)
by A1,A5,Th30
.= ((PProJ(w,y,p-q,u) + PProJ(w,y,p-q,A*(p-q))) + PProJ(w,y,p-q,u)) -
PProJ(w,y,p-q,p+q) by A1,Th30;
then q,p,p#q,v9#u are_Ort_wrt w,y by A1,A7,Th33;
then s,v9#u,q,p are_Ort_wrt w,y by Lm5;
then
A8: s,v9#u,p,q are_Ort_wrt w,y by Lm4;
set Y = PProJ(w,y,v9-u,(v9#u)-s);
A9: v9-u = A*(p-q) by A5,RLSUB_2:61;
1*(v9-u) = (u+A*(p-q))-u by A5,RLVECT_1:def 8
.= A*(p-q) by RLSUB_2:61;
then q,p // u,v9 or q,p // v9,u by ANALMETR:14;
then
A10: p,q // u,v9 or p,q // v9,u by ANALOAF:12;
A11: PProJ(w,y,A*(p-q),A*(p-q)) = A*PProJ(w,y,p-q,A*(p-q)) by A1,Th31
.= A*(((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))")*
PProJ(w,y,p-q,p-q)) by A1,A4,Th31
.= A*((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*((PProJ(w,y,p-q,p-q))"*
PProJ(w,y,p-q,p-q)))
.= A*((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*1) by A6,XCMPLX_0:def 7
.= A*(PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u));
2*Y = 2*(PProJ(w,y,v9-u,v9#u)-PProJ(w,y,v9-u,p#q)) by A1,Th30
.= 2*PProJ(w,y,v9-u,v9#u)-2*PProJ(w,y,v9-u,p#q)
.= (PProJ(w,y,v9-u,v9)+PProJ(w,y,v9-u,u))-2*PProJ(w,y,v9-u,p#q) by A1,Th34
.= (PProJ(w,y,v9-u,v9)+PProJ(w,y,v9-u,u))-(PProJ(w,y,v9-u,p)+PProJ (w,y,
v9-u,q)) by A1,Th34
.= (PProJ(w,y,v9-u,u+A*(p-q)) + PProJ(w,y,v9-u,u)) - PProJ (w,y,v9-u,p+q
) by A1,A5,Th30
.= ((PProJ(w,y,v9-u,u) + PProJ(w,y,v9-u,A*(p-q))) + PProJ(w,y,v9-u,u)) -
PProJ (w,y,v9-u,p+q) by A1,Th30;
then
A12: 2*Y = ((PProJ(w,y,A*(p-q),u) + (A*PProJ(w,y,p-q,p+q) - A*(2*PProJ(w,y,p
-q,u)))) + PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A9,A11
.= ((PProJ(w,y,A*(p-q),u) + (PProJ(w,y,A*(p-q),p+q) - 2*(A*PProJ(w,y,p-q
,u)))) + PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A1,Th31
.= ((PProJ(w,y,A*(p-q),u) + (PProJ(w,y,A*(p-q),p+q) - 2*PProJ (w,y,A*(p-
q),u))) + PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A1,Th31
.= 0;
then u,v9,s,v9#u are_Ort_wrt w,y by A1,Th33;
then s,v9#u,u,v9 are_Ort_wrt w,y by Lm5;
then s,v9#u,v9,u are_Ort_wrt w,y by Lm4;
then p,q,s,u#v9 are_Ort_wrt w,y & u,v9,s,u#v9 are_Ort_wrt w,y & p,q,s,v9#u
are_Ort_wrt w,y & v9,u,s,v9#u are_Ort_wrt w,y by A1,A8,A12,Lm5,Th33;
then p,q,u,v9 are_DTr_wrt w,y or p,q,v9,u are_DTr_wrt w,y by A10;
hence thesis by A1,A2,A3,Th25;
end;
Lm21: Gen w,y implies for u,u9,u1,u2,t1,t2 being VECTOR of V,
A1,A2 being Real
st A1 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u1))*((PProJ (w,y,u-u9,u-u9))"
) & A2 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u2))*((PProJ (w,y,u-u9,u-u9))
") & t1 = u1+A1*(u-u9) & t2 = u2+A2*(u-u9) holds t2-t1 = (u2 - u1)+(A2-A1)*(u-
u9) & A2-A1 = ((-2)*PProJ(w,y,u-u9,u2-u1))*((PProJ(w,y,u-u9,u-u9))")
proof
assume
A1: Gen w,y;
let u,u9,u1,u2,t1,t2 be VECTOR of V, A1,A2 be Real such that
A2: A1 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u1))*((PProJ (w,y,u-u9
,u-u9)) ") & A2 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u2))*((PProJ (w,y,u-
u9,u- u9)) ") & t1 = u1+A1*(u-u9) & t2 = u2+A2*(u-u9);
thus t2-t1 = (u2 - u1)+(A2-A1)*(u-u9) & A2-A1 = ((-2)*PProJ(w,y,u-u9,u2-u1))
*((PProJ(w,y,u-u9,u-u9))")
proof
set uu = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u2)) - (PProJ(w,y,u-u9,u
+u9) - 2*PProJ(w,y,u-u9,u1));
A3: 2*u1 - 2*u2 = -(2*u2 - 2*u1) by RLVECT_1:33
.= -(2*(u2 - u1)) by RLVECT_1:34
.= 2*(-(u2 - u1)) by RLVECT_1:25
.= (-2)*(u2 - u1) by RLVECT_1:24;
uu = (PProJ(w,y,u-u9,u+u9) - PProJ(w,y,u-u9,2*u2)) - (PProJ(w,y,u-u9,u
+u9) - 2*PProJ(w,y,u-u9,u1)) by A1,Th31
.= (PProJ(w,y,u-u9,u+u9) - PProJ(w,y,u-u9,2*u2)) - (PProJ(w,y,u-u9,u+
u9) - PProJ(w,y,u-u9,2*u1)) by A1,Th31
.= PProJ(w,y,u-u9,2*u1) - PProJ(w,y,u-u9,2*u2)
.= PProJ(w,y,u-u9,2*u1 - 2*u2) by A1,Th30;
then uu = (-2)*PProJ(w,y,u-u9,u2-u1) by A1,A3,Th31;
hence thesis by A2,Lm20,XCMPLX_1:40;
end;
end;
theorem Th37:
Gen w,y implies for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of
V st u<>u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,
w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 holds t1,t2 //
w1,w2
proof
assume
A1: Gen w,y;
let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that
A2: u<>u9 and
A3: u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y and
A4: u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y and
A5: u1,u2 // v1,v2;
set A1 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u1))*(PProJ(w,y,u-u9,u-u9)
)", A2 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u2))*(PProJ(w,y,u-u9,u-u9))",
A3 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,v1))*(PProJ(w,y,u-u9,u-u9))", A4
= (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,v2))*(PProJ(w,y,u-u9,u-u9))";
A6: (u1+A1*(u-u9))=t1 & (u2+A2*(u-u9))=t2 by A1,A2,A3,Th36;
A7: (v1+A3*(u-u9))=w1 & (v2+A4*(u-u9))=w2 by A1,A2,A4,Th36;
A8: t1=u1+A1*(u-u9) & t2=u2+A2*(u-u9) by A1,A2,A3,Th36;
per cases;
suppose
u1=u2;
then t1=t2 by A1,A2,A3,Th24;
hence thesis by ANALOAF:def 1;
end;
suppose
v1=v2;
then w1=w2 by A1,A2,A4,Th24;
hence thesis by ANALOAF:def 1;
end;
suppose that
A9: u1<>u2 & v1<>v2;
set cc = (PProJ(w,y,u-u9,u-u9))";
set vv = ((-2)*PProJ(w,y,u-u9,v2-v1));
set uu = ((-2)*PProJ(w,y,u-u9,u2-u1));
A10: w2-w1 = (v2 - v1)+(A4-A3)*(u-u9) by A1,A7,Lm21;
consider a,b such that
A11: a*(u2-u1) = b*(v2-v1) and
A12: 0<a & 0<b by A5,A9,ANALOAF:7;
A13: a*uu = (-2)*(a*PProJ(w,y,u-u9,u2-u1))
.= (-2)*PProJ(w,y,u-u9,b*(v2-v1)) by A1,A11,Th31
.= (-2)*(b*PProJ(w,y,u-u9,v2-v1)) by A1,Th31
.=b*vv;
A14: a*(A2-A1) = a*(uu*cc) by A1,A8,Lm21
.= (b*vv)*cc by A13,XCMPLX_1:4
.= b*(vv*cc)
.= b*(A4-A3) by A1,A7,Lm21;
t2-t1 = (u2 - u1)+(A2-A1)*(u-u9) by A1,A6,Lm21;
then a*(t2-t1) = a*(u2 - u1) + a*((A2-A1)*(u-u9)) by RLVECT_1:def 5
.= b*(v2-v1) + (b*(A4-A3))*(u-u9) by A11,A14,RLVECT_1:def 7
.= b*(v2 - v1) + b*((A4-A3)*(u-u9)) by RLVECT_1:def 7
.= b*(w2-w1) by A10,RLVECT_1:def 5;
hence thesis by A12,ANALOAF:def 1;
end;
end;
theorem
Gen w,y implies for u,u9,u1,u2,v1,t1,t2,w1 being VECTOR of V st u<>u9
& u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1
are_DTr_wrt w,y & v1=u1#u2 holds w1 = t1#t2
proof
assume
A1: Gen w,y;
let u,u9,u1,u2,v1,t1,t2,w1 be VECTOR of V such that
A2: u<>u9 and
A3: u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y and
A4: u,u9,v1,w1 are_DTr_wrt w,y and
A5: v1=u1#u2;
set G = PProJ(w,y,u-u9,u+u9), H = PProJ(w,y,u-u9,u1), W = PProJ(w,y,u-u9,u2)
, I = PProJ(w,y,u-u9,v1), N = PProJ(w,y,u-u9,u-u9);
set A1 = (G - 2*H)*N", A2 = (G - 2*W)*N", A3 = (G - 2*I)*N";
A6: H+W = PProJ(w,y,u-u9,u1+u2) by A1,Th30
.= PProJ(w,y,u-u9,v1+v1) by A5,Def2
.= I+I by A1,Th30;
v1+A3*(u-u9) =w1 by A1,A2,A4,Th36;
then
A7: w1+w1 = A3*(u-u9)+(v1 + (v1+A3*(u-u9))) by RLVECT_1:def 3
.= A3*(u-u9)+((v1 + v1)+A3*(u-u9)) by RLVECT_1:def 3
.= (v1 + v1)+(A3*(u-u9)+A3*(u-u9)) by RLVECT_1:def 3
.= (v1 + v1)+(A3+A3)*(u-u9) by RLVECT_1:def 6;
u1+A1*(u-u9)=t1 & u2+A2*(u-u9)=t2 by A1,A2,A3,Th36;
then
A8: t1+t2 = A1*(u-u9)+(u1 + (u2+A2*(u-u9))) by RLVECT_1:def 3
.= A1*(u-u9)+((u1 + u2)+A2*(u-u9)) by RLVECT_1:def 3
.= (u1 + u2)+(A1*(u-u9)+A2*(u-u9)) by RLVECT_1:def 3
.= (u1 + u2)+(A1+A2)*(u-u9) by RLVECT_1:def 6
.= (v1 + v1)+(A1+A2)*(u-u9) by A5,Def2;
set vv = (G - 2*I) + (G - 2*I);
A1+A2 = ((G - 2*H) + (G - 2*W))*N" .= vv*N" by A6
.=A3+A3;
hence thesis by A8,A7,Def2;
end;
theorem Th39:
Gen w,y implies for u,u9,u1,u2,t1,t2 being VECTOR of V st u<>u9
& u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y holds u,u9,u1#u2,t1#
t2 are_DTr_wrt w,y
proof
assume
A1: Gen w,y;
let u,u9,u1,u2,t1,t2 be VECTOR of V such that
A2: u<>u9 and
A3: u,u9,u1,t1 are_DTr_wrt w,y and
A4: u,u9,u2,t2 are_DTr_wrt w,y;
u1,t1,u2,t2 are_DTr_wrt w,y by A1,A2,A3,A4,Th19;
then
A5: u1,t1,u1#u2,t1#t2 are_DTr_wrt w,y by A1,Th26;
u2,t2,u1,t1 are_DTr_wrt w,y by A1,A2,A3,A4,Th19;
then
A6: u2,t2,u2#u1,t2#t1 are_DTr_wrt w,y by A1,Th26;
per cases;
suppose
A7: u1<>t1;
u1,t1,u,u9 are_DTr_wrt w,y by A3,Th21;
hence thesis by A1,A5,A7,Th19;
end;
suppose
A8: u2<>t2;
u2,t2,u,u9 are_DTr_wrt w,y by A4,Th21;
hence thesis by A1,A6,A8,Th19;
end;
suppose that
A9: u1=t1 and
A10: u2=t2;
u#u9,(u1#u2)#(t1#t2),u1#u2,t1#t2 are_Ort_wrt w,y by A1,A9,A10,Lm6;
then
A11: u1#u2,t1#t2,u#u9,(u1#u2)#(t1#t2) are_Ort_wrt w,y by Lm5;
A12: u,u9,u#u9,u1#u2 are_Ort_wrt w,y
proof
set uu9=u#u9;
A13: 2*(u1#u2) = (1+1)*(u1#u2) .= 1*(u1#u2)+1*(u1#u2) by RLVECT_1:def 6
.= (u1#u2)+1*(u1#u2) by RLVECT_1:def 8
.= (u1#u2)+(u1#u2) by RLVECT_1:def 8
.=u1+u2 by Def2;
A14: -(2*uu9) = -((1+1)*uu9) .= -(1*uu9+1*uu9) by RLVECT_1:def 6
.= -(uu9 + 1*uu9) by RLVECT_1:def 8
.= -(uu9+uu9) by RLVECT_1:def 8
.= -uu9 + -uu9 by Lm19;
u,u9,uu9,u2#t2 are_Ort_wrt w,y by A4;
then u9-u,u2-uu9 are_Ort_wrt w,y by A10,ANALMETR:def 3;
then
A15: u9-u,(2")*(u2-uu9) are_Ort_wrt w,y by ANALMETR:7;
u,u9,uu9,u1#t1 are_Ort_wrt w,y by A3;
then u9-u,u1-uu9 are_Ort_wrt w,y by A9,ANALMETR:def 3;
then
A16: u9-u,(2")*(u1-uu9) are_Ort_wrt w,y by ANALMETR:7;
u1#u2-uu9 = (2"*2)*(u1#u2-uu9) by RLVECT_1:def 8
.= 2"*(2*(u1#u2-uu9)) by RLVECT_1:def 7
.= 2"*((u1+u2)-(2*uu9)) by A13,RLVECT_1:34
.= 2"*(((u1+u2)+ -uu9) + -uu9) by A14,RLVECT_1:def 3
.= 2"*(((u1-uu9)+u2) + -uu9) by RLVECT_1:def 3
.= 2"*((u1-uu9)+(u2-uu9)) by RLVECT_1:def 3
.= 2"*(u1-uu9)+2"*(u2-uu9) by RLVECT_1:def 5;
then u9-u,u1#u2-uu9 are_Ort_wrt w,y by A1,A16,A15,ANALMETR:10;
hence thesis by ANALMETR:def 3;
end;
u,u9 // u1#u2,t1#t2 by A9,A10,ANALOAF:9;
hence thesis by A9,A10,A11,A12;
end;
end;
theorem Th40:
Gen w,y implies for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of
V st u<>u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,
w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y
holds t1,t2,w1,w2 are_Ort_wrt w,y
proof
assume
A1: Gen w,y;
let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that
A2: u<>u9 and
A3: u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y and
A4: u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y and
A5: u1,u2,v1,v2 are_Ort_wrt w,y;
set A1 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u1))*(PProJ(w,y,u-u9,u-u9)
)", A2 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,u2))*(PProJ(w,y,u-u9,u-u9))",
A3 = (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,v1))*(PProJ(w,y,u-u9,u-u9))", A4
= (PProJ(w,y,u-u9,u+u9) - 2*PProJ(w,y,u-u9,v2))*(PProJ(w,y,u-u9,u-u9))";
(u1+A1*(u-u9))=t1 & (u2+A2*(u-u9))=t2 by A1,A2,A3,Th36;
then
A6: t2-t1 = (u2 - u1)+(A2-A1)*(u-u9) by A1,Lm21;
A7: t1=u1+A1*(u-u9) & t2=u2+A2*(u-u9) by A1,A2,A3,Th36;
A8: (v1+A3*(u-u9))=w1 & (v2+A4*(u-u9))=w2 by A1,A2,A4,Th36;
then w2-w1 = (v2 - v1)+(A4-A3)*(u-u9) by A1,Lm21;
then
A9: PProJ(w,y,t2-t1,w2-w1) =PProJ(w,y,u2-u1,(v2 - v1)+(A4-A3)*(u-u9)) +
PProJ(w,y,(A2-A1)*(u-u9),(v2 - v1)+(A4-A3)*(u-u9)) by A1,A6,Th30
.= (PProJ(w,y,u2-u1,v2-v1) + PProJ(w,y,u2-u1,(A4-A3)*(u-u9))) + PProJ(w,
y,(A2-A1)*(u-u9),(v2 - v1)+(A4-A3)*(u-u9)) by A1,Th30
.= (0 + PProJ(w,y,u2-u1,(A4-A3)*(u-u9))) + PProJ(w,y,(A2-A1)*(u-u9),(v2
- v1)+(A4-A3)*(u-u9)) by A1,A5,Th33
.= PProJ(w,y,u2-u1,(A4-A3)*(u-u9)) + (PProJ(w,y,(A2-A1)*(u-u9),(v2 - v1)
) + PProJ (w,y,(A2-A1)*(u-u9),(A4-A3)*(u-u9))) by A1,Th30;
set aa = (PProJ(w,y,u-u9,u-u9))"*((PProJ(w,y,u-u9,u2-u1)*PProJ (w,y,u-u9,v2-
v1)));
A10: PProJ(w,y,(A2-A1)*(u-u9),(v2 - v1)) = PProJ(w,y,v2-v1,(A2-A1)*(u-u9))
.= PProJ(w,y,v2-v1,u-u9)*(A2-A1) by A1,Th31
.= PProJ(w,y,v2-v1,u-u9)*( ((-2)*PProJ(w,y,u-u9,u2-u1))* ((PProJ(w,y,u-
u9,u-u9))") ) by A1,A7,Lm21
.=(-2)*aa;
A11: PProJ(w,y,u-u9,u-u9) <> 0 by A1,A2,Th35;
A12: PProJ(w,y,u2-u1,(A4-A3)*(u-u9)) = PProJ (w,y,u2-u1,u-u9)*(A4-A3) by A1
,Th31
.= PProJ(w,y,u2-u1,u-u9)*( ((-2)*PProJ(w,y,u-u9,v2-v1))* ((PProJ(w,y,u-
u9,u-u9))") ) by A1,A8,Lm21
.=(-2)*aa;
PProJ(w,y,(A2-A1)*(u-u9),(A4-A3)*(u-u9)) = (A2-A1)*PProJ(w,y,u-u9,(A4-
A3)*(u-u9)) by A1,Th31
.= (A2-A1)*((A4-A3)*PProJ(w,y,u-u9,u-u9)) by A1,Th31
.= (A2-A1)*( (((-2)*PProJ(w,y,u-u9,v2-v1)) * ((PProJ(w,y,u-u9,u-u9))") )
* PProJ(w,y,u-u9,u-u9) ) by A1,A8,Lm21
.= (A2-A1)*( ((-2)*PProJ(w,y,u-u9,v2-v1))*(((PProJ(w,y,u-u9,u-u9))" )*
PProJ(w,y,u-u9,u-u9)) )
.= (A2-A1)*( ((-2)*PProJ(w,y,u-u9,v2-v1))*1 ) by A11,XCMPLX_0:def 7
.= ((-2)*(A2-A1))*PProJ(w,y,u-u9,v2-v1)
.= ((-2)*( ((-2)*PProJ(w,y,u-u9,u2-u1))*((PProJ(w,y,u-u9,u-u9))")) )*
PProJ(w,y,u-u9,v2-v1) by A1,A7,Lm21
.=4*aa;
hence thesis by A1,A9,A12,A10,Th33;
end;
theorem Th41:
for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of V holds (Gen w,
y & u<>u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,
w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_DTr_wrt w,y
implies t1,t2,w1,w2 are_DTr_wrt w,y)
proof
let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V;
assume that
A1: Gen w,y & u<>u9 and
A2: u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y and
A3: u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y and
A4: u1,u2,v1,v2 are_DTr_wrt w,y;
set uu=u1#u2,vv=v1#v2;
A5: u,u9,uu,(t1#t2) are_DTr_wrt w,y & u,u9,vv,(w1#w2) are_DTr_wrt w,y by A1,A2
,A3,Th39;
v1,v2,uu,vv are_Ort_wrt w,y by A4;
then
A6: w1,w2,t1#t2,w1#w2 are_Ort_wrt w,y by A1,A3,A5,Th40;
u1,u2,uu,vv are_Ort_wrt w,y by A4;
then
A7: t1,t2,t1#t2,w1#w2 are_Ort_wrt w,y by A1,A2,A5,Th40;
u1,u2 // v1,v2 by A4;
then t1,t2 // w1,w2 by A1,A2,A3,Th37;
hence thesis by A7,A6;
end;
definition
let V;
let w,y;
func DTrapezium(V,w,y) -> Relation of [:the carrier of V,the carrier of V:]
means
:Def7:
for x,z being object holds
[x,z] in it iff ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y;
existence
proof
defpred P[object,object] means
ex u,u1,v,v1 st $1=[u,u1] & $2=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y;
set VV = [:the carrier of V,the carrier of V:];
consider P being Relation of VV,VV such that
A1: for x,z being object holds [x,z] in P iff x in VV & z in VV & P[x,z]
from RELSET_1:sch 1;
take P;
let x,z be object;
thus [x,z] in P implies ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y by A1;
assume ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y;
hence thesis by A1;
end;
uniqueness
proof
let P,Q be Relation of [:the carrier of V,the carrier of V:] such that
A2: for x,z being object holds
[x,z] in P iff ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y and
A3: for x,z being object holds
[x,z] in Q iff ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y;
for x,z being object holds [x,z] in P iff [x,z] in Q
proof
let x,z be object;
[x,z] in P iff ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1
are_DTr_wrt w,y by A2;
hence thesis by A3;
end;
hence thesis by RELAT_1:def 2;
end;
end;
theorem Th42:
[[u,v],[u1,v1]] in DTrapezium(V,w,y) iff u,v,u1,v1 are_DTr_wrt w ,y
proof
now
assume [[u,v],[u1,v1]] in DTrapezium(V,w,y);
then consider u9,v9,u19,v19 being VECTOR of V such that
A1: [u,v]=[u9,v9] and
A2: [u1,v1]=[u19,v19] and
A3: u9,v9,u19,v19 are_DTr_wrt w,y by Def7;
A4: u1=u19 by A2,XTUPLE_0:1;
u=u9 & v=v9 by A1,XTUPLE_0:1;
hence u,v,u1,v1 are_DTr_wrt w,y by A2,A3,A4,XTUPLE_0:1;
end;
hence thesis by Def7;
end;
definition
let V;
func MidPoint(V) -> BinOp of the carrier of V means
:Def8:
for u,v holds it. (u,v) = u#v;
existence
proof
deffunc F(VECTOR of V,VECTOR of V) = $1#$2;
ex B being BinOp of the carrier of V st for u,v holds B.(u,v) = F(u,v)
from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
deffunc F(VECTOR of V,VECTOR of V) = $1#$2;
for o1,o2 being BinOp of the carrier of V st (for a,b being Element of
V holds o1.(a,b) = F(a,b)) & (for a,b being Element of V holds o2.(a,b) = F(a,b
)) holds o1 = o2 from BINOP_2:sch 2;
hence thesis;
end;
end;
definition
struct(AffinStruct,MidStr) AfMidStruct (# carrier -> set, MIDPOINT -> BinOp
of the carrier, CONGR -> Relation of [:the carrier,the carrier:] #);
end;
registration
cluster non empty strict for AfMidStruct;
existence
proof
set D = the non empty set,m = the BinOp of D,c = the Relation of [: D,D:];
take AfMidStruct (#D,m,c #);
thus the carrier of AfMidStruct (#D,m,c #) is non empty;
thus thesis;
end;
end;
definition
let V,w,y;
func DTrSpace(V,w,y) -> strict AfMidStruct equals
AfMidStruct(#the carrier
of V, MidPoint(V),DTrapezium(V,w,y)#);
correctness;
end;
registration
let V,w,y;
cluster DTrSpace(V,w,y) -> non empty;
coherence;
end;
definition
::$CD
end;
registration
let AMS be non empty AfMidStruct;
cluster the AffinStruct of AMS -> non empty;
coherence;
end;
definition
let AMS be non empty AfMidStruct, a,b be Element of AMS;
func a#b -> Element of AMS equals
(the MIDPOINT of AMS).(a,b);
correctness;
end;
reserve a,b,c,d,a1,a2,b1,c1,d1,d2,p,q for Element of DTrSpace(V,w,y);
theorem
for x being set holds x is Element of the carrier of DTrSpace(V,w,y)
iff x is VECTOR of V;
theorem Th44:
u=a & v=b & u1=a1 & v1=b1 implies (a,b // a1,b1 iff u,v,u1,v1
are_DTr_wrt w,y)
proof
assume
A1: u=a & v=b & u1=a1 & v1=b1;
hereby
assume a,b // a1,b1;
then [[a,b],[a1,b1]] in DTrapezium(V,w,y) by ANALOAF:def 2;
hence u,v,u1,v1 are_DTr_wrt w,y by A1,Th42;
end;
assume u,v,u1,v1 are_DTr_wrt w,y;
then [[a,b],[a1,b1]] in DTrapezium(V,w,y) by A1,Th42;
hence a,b // a1,b1 by ANALOAF:def 2;
end;
theorem
Gen w,y & u=a & v=b implies u#v = a#b by Def8;
Lm22: Gen w,y & a,b // b,c implies a=b & b=c
proof
assume that
A1: Gen w,y and
A2: a,b // b,c;
reconsider u=a,v=b,u1=c as VECTOR of V;
u,v,v,u1 are_DTr_wrt w,y by A2,Th44;
hence thesis by A1,Th18;
end;
Lm23: Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1
proof
assume that
A1: Gen w,y and
A2: a,b // a1,b1 & a,b // c1,d1 and
A3: a<>b;
reconsider u=a,v=b,u1=a1,v1=b1,u2=c1,v2=d1 as VECTOR of V;
u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y by A2,Th44;
then u1,v1,u2,v2 are_DTr_wrt w,y by A1,A3,Th19;
hence thesis by Th44;
end;
Lm24: a,b // c,d implies c,d // a,b & b,a // d,c
proof
reconsider u=a,v=b,u1=c,v1=d as VECTOR of V;
assume a,b // c,d;
then u,v,u1,v1 are_DTr_wrt w,y by Th44;
then v,u,v1,u1 are_DTr_wrt w,y & u1,v1,u,v are_DTr_wrt w,y by Th21,Th22;
hence thesis by Th44;
end;
Lm25: Gen w,y implies ex d st a,b // c,d or a,b // d,c
proof
reconsider u=a,v=b,u1=c as VECTOR of V;
assume Gen w,y;
then consider t being VECTOR of V such that
A1: u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y by Th20;
reconsider d=t as Element of DTrSpace(V,w,y);
a,b // c,d or a,b // d,c by A1,Th44;
hence thesis;
end;
Lm26: Gen w,y & a,b // c,d1 & a,b // c,d2 implies a=b or d1=d2
proof
assume that
A1: Gen w,y and
A2: a,b // c,d1 & a,b // c,d2;
reconsider u=a,v=b,u1=c,v1=d1,v2=d2 as VECTOR of V;
u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y by A2,Th44;
hence thesis by A1,Th24;
end;
Lm27: a#b = b#a
proof
reconsider u=a,v=b as VECTOR of V;
thus a#b = u#v by Def8
.= b#a by Def8;
end;
Lm28: a#a = a
proof
reconsider u=a as VECTOR of V;
u#u = u;
hence thesis by Def8;
end;
Lm29: (a#b)#(c#d) = (a#c)#(b#d)
proof
reconsider u=a,u1=b,v=c,v1=d as VECTOR of V;
set ab= a#b,cd=c#d,ac=a#c,bd=b#d,uu1=u#u1,vv1=v#v1,uv=u#v,u1v1=u1#v1;
A1: ac = uv & bd=u1v1 by Def8;
ab=uu1 & cd=vv1 by Def8;
hence (ab)#(cd) = (uu1)#(vv1) by Def8
.= (uv)#(u1v1) by Th6
.= (ac)#(bd) by A1,Def8;
end;
Lm30: ex p st p#a=b
proof
reconsider u=a,v=b as VECTOR of V;
consider u1 such that
A1: u#u1=v by Th5;
reconsider p=u1 as Element of DTrSpace(V,w,y);
p#a= u # u1 by Def8;
hence thesis by A1;
end;
Lm31: a#a1=a#a2 implies a1=a2
proof
assume
A1: a#a1=a#a2;
reconsider u=a,u1=a1,u2=a2 as VECTOR of V;
u#u1=a#a1 & u#u2=a#a2 by Def8;
hence thesis by A1,Th7;
end;
Lm32: Gen w,y & a,b // c,d implies a,b // (a#c),(b#d)
proof
assume that
A1: Gen w,y and
A2: a,b // c,d;
reconsider u=a,v=b,u1=c,v1=d as VECTOR of V;
u,v,u1,v1 are_DTr_wrt w,y by A2,Th44;
then
A3: u,v,(u#u1),(v#v1) are_DTr_wrt w,y by A1,Th26;
a#c = u#u1 & b#d = v#v1 by Def8;
hence thesis by A3,Th44;
end;
Lm33: Gen w,y & a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d))
proof
assume that
A1: Gen w,y and
A2: a,b // c,d;
reconsider u=a,v=b,u1=c,v1=d as VECTOR of V;
u,v,u1,v1 are_DTr_wrt w,y by A2,Th44;
then
A3: u,v,(u#v1),(v#u1) are_DTr_wrt w,y or u,v,(v#u1),(u#v1) are_DTr_wrt w,y
by A1,Th27;
a#d = u#v1 & b#c = v#u1 by Def8;
hence thesis by A3,Th44;
end;
Lm34: a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies a1,b1 // c1,d1
proof
assume that
A1: a,b // c,d & a#a1=p and
A2: b#b1=p & c#c1=p and
A3: d#d1=p;
reconsider u1=a,u2=b,v1=c,v2=d,u=p,t1=a1,t2=b1,w1=c1,w2=d1 as VECTOR of V;
A4: u=u2#t2 & u=v1#w1 by A2,Def8;
A5: u=v2#w2 by A3,Def8;
u1,u2,v1,v2 are_DTr_wrt w,y & u=u1#t1 by A1,Def8,Th44;
then t1,t2,w1,w2 are_DTr_wrt w,y by A4,A5,Th28;
hence thesis by Th44;
end;
Lm35: Gen w,y & p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
a,b // c,d implies a1,b1 // c1,d1
proof
assume that
A1: Gen w,y & p<>q and
A2: p,q // a,a1 & p,q // b,b1 and
A3: p,q // c,c1 & p,q // d,d1 and
A4: a,b // c,d;
reconsider u=p,u9=q,u1=a,u2=b,v1=c,v2=d,t1=a1,t2=b1,w1=c1,w2=d1 as VECTOR of
V;
A5: u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y by A3,Th44;
A6: u1,u2,v1,v2 are_DTr_wrt w,y by A4,Th44;
u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y by A2,Th44;
then t1,t2,w1,w2 are_DTr_wrt w,y by A1,A5,A6,Th41;
hence thesis by Th44;
end;
definition
let IT be non empty AfMidStruct;
attr IT is MidOrdTrapSpace-like means
:Def11:
for a,b,c,d,a1,b1,c1,d1,p,q
being Element of IT holds a#b=b#a & a#a=a & (a#b)#(c#d)=(a#c)#(b#d) & (ex p
being Element of IT st p#a=b) & (a#b=a#c implies b=c) & (a,b // c,d implies a,b
// (a#c),(b#d)) & (a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d)
)) & (a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies a1,b1 // c1,d1) &
(p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d
implies a1,b1 // c1,d1) & (a,b // b,c implies a=b & b=c) & (a,b // a1,b1 & a,b
// c1,d1 & a<>b implies a1,b1 // c1,d1) & (a,b // c,d implies c,d // a,b & b,a
// d,c) & (ex d being Element of IT st a,b // c,d or a,b // d,c) & (a,b // c,p
& a,b // c,q implies a=b or p=q);
end;
registration
cluster strict MidOrdTrapSpace-like for non empty AfMidStruct;
existence
proof
consider V such that
A1: ex w,y st Gen w,y by ANALMETR:3;
consider w,y being VECTOR of V such that
A2: Gen w,y by A1;
set X = DTrSpace(V,w,y);
X is MidOrdTrapSpace-like
by Lm27,Lm28,Lm29,Lm30,Lm31,A2,Lm32,Lm33,Lm34,Lm35,Lm22,Lm23,Lm24,Lm25,Lm26
;
hence thesis;
end;
end;
definition
mode MidOrdTrapSpace is MidOrdTrapSpace-like non empty AfMidStruct;
end;
theorem
Gen w,y implies DTrSpace(V,w,y) is MidOrdTrapSpace
proof
set X = DTrSpace(V,w,y);
assume
A1: Gen w,y;
X is MidOrdTrapSpace-like
by Lm27,Lm28,Lm29,Lm30,Lm31,A1,Lm32,Lm33,Lm34,Lm35,Lm22,Lm23,Lm24,Lm25,Lm26;
hence thesis;
end;
set MOS = the MidOrdTrapSpace;
set X = the AffinStruct of MOS;
Lm36: now
let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;
reconsider a9=a,b9=b,c9=c,d9=d,a19=a1,b19=b1,c19=c1,d19=d1,p9=p,q9=q as
Element of MOS;
A1: now
let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of MOS
such that
A2: a=a9 & b=b9 & c =c9 & d=d9;
A3: now
assume a9,b9 // c9,d9;
then [[a,b],[c,d]] in the CONGR of MOS by A2,ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2;
end;
now
assume a,b // c,d;
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A2,ANALOAF:def 2;
end;
hence a,b // c,d iff a9,b9 // c9,d9 by A3;
end;
hereby
assume a,b // b,c;
then a9,b9 // b9,c9 by A1;
hence a=b & b=c by Def11;
end;
hereby
assume that
A4: a,b // a1,b1 & a,b // c1,d1 and
A5: a<>b;
a9,b9 // a19,b19 & a9,b9 // c19,d19 by A1,A4;
then a19,b19 // c19,d19 by A5,Def11;
hence a1,b1 // c1,d1 by A1;
end;
hereby
assume a,b // c,d;
then a9,b9 // c9,d9 by A1;
then c9,d9 // a9,b9 & b9,a9 // d9,c9 by Def11;
hence c,d // a,b & b,a // d,c by A1;
end;
thus ex d being Element of X st a,b // c,d or a,b // d,c
proof
consider x9 being Element of MOS such that
A6: a9,b9 // c9,x9 or a9,b9 // x9,c9 by Def11;
reconsider x=x9 as Element of X;
take x;
thus thesis by A1,A6;
end;
assume a,b // c,p & a,b // c,q;
then a9,b9 // c9,p9 & a9,b9 // c9, q9 by A1;
hence a=b or p=q by Def11;
end;
definition
let IT be non empty AffinStruct;
attr IT is OrdTrapSpace-like means
:Def12:
for a,b,c,d,a1,b1,c1,d1,p,q being
Element of IT holds (a,b // b,c implies a=b & b=c) & (a,b // a1,b1 & a,b // c1,
d1 & a<>b implies a1,b1 // c1,d1) & (a,b // c,d implies c,d // a,b & b,a // d,c
) & (ex d being Element of IT st a,b // c,d or a,b // d,c) & (a,b // c,p & a,b
// c,q implies a=b or p=q);
end;
registration
cluster strict OrdTrapSpace-like for non empty AffinStruct;
existence by Def12,Lm36;
end;
definition
mode OrdTrapSpace is OrdTrapSpace-like non empty AffinStruct;
end;
registration
let MOS be MidOrdTrapSpace;
cluster the AffinStruct of MOS -> OrdTrapSpace-like;
coherence
proof
set X = the AffinStruct of MOS;
the AffinStruct of MOS is OrdTrapSpace-like
proof
let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;
reconsider a9=a,b9=b,c9=c,d9=d,a19=a1,b19=b1,c19=c1,d19=d1,p9=p,q9=q as
Element of MOS;
A1: now
let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of
MOS such that
A2: a=a9 & b=b9 & c =c9 & d=d9;
hereby
assume a,b // c,d;
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A2,ANALOAF:def 2;
end;
assume a9,b9 // c9,d9;
then [[a,b],[c,d]] in the CONGR of MOS by A2,ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2;
end;
hereby
assume a,b // b,c;
then a9,b9 // b9,c9 by A1;
hence a=b & b=c by Def11;
end;
hereby
assume that
A3: a,b // a1,b1 & a,b // c1,d1 and
A4: a<>b;
a9,b9 // a19,b19 & a9,b9 // c19,d19 by A1,A3;
then a19,b19 // c19,d19 by A4,Def11;
hence a1,b1 // c1,d1 by A1;
end;
hereby
assume a,b // c,d;
then a9,b9 // c9,d9 by A1;
then c9,d9 // a9,b9 & b9,a9 // d9,c9 by Def11;
hence c,d // a,b & b,a // d,c by A1;
end;
thus ex d being Element of X st a,b // c,d or a,b // d,c
proof
consider x9 being Element of MOS such that
A5: a9,b9 // c9,x9 or a9,b9 // x9,c9 by Def11;
reconsider x=x9 as Element of X;
take x;
thus thesis by A1,A5;
end;
assume a,b // c,p & a,b // c,q;
then a9,b9 // c9,p9 & a9,b9 // c9, q9 by A1;
hence a=b or p=q by Def11;
end;
hence thesis;
end;
end;
reserve OTS for OrdTrapSpace;
reserve a,b,c,d for Element of OTS;
reserve a9,b9,c9,d9,a19,b19,d19 for Element of Lambda(OTS);
theorem Th47:
for x being set holds (x is Element of OTS iff x is Element of Lambda(OTS))
proof
let x be set;
Lambda(OTS) = AffinStruct (# the carrier of OTS, lambda(the CONGR of OTS
) #) by DIRAF:def 2;
hence thesis;
end;
theorem Th48:
a=a9 & b=b9 & c =c9 & d=d9 implies (a9,b9 // c9,d9 iff a,b // c,
d or a,b // d,c)
proof
A1: Lambda(OTS) = AffinStruct(#the carrier of OTS,lambda(the CONGR of OTS)#)
by DIRAF:def 2;
assume
A2: a=a9 & b=b9 & c =c9 & d=d9;
hereby
assume a9,b9 // c9,d9;
then [[a9,b9],[c9,d9]] in lambda(the CONGR of OTS) by A1,ANALOAF:def 2;
then
[[a,b],[c,d]] in the CONGR of OTS or [[a,b],[d,c]] in the CONGR of OTS
by A2,DIRAF:def 1;
hence a,b // c,d or a,b // d,c by ANALOAF:def 2;
end;
assume a,b // c,d or a,b // d,c;
then [[a,b],[c,d]] in the CONGR of OTS or [[a,b],[d,c]] in the CONGR of OTS
by ANALOAF:def 2;
then [[a,b],[c,d]] in the CONGR of Lambda(OTS) by A1,DIRAF:def 1;
hence thesis by A2,ANALOAF:def 2;
end;
Lm37: for a9,b9,c9 ex d9 st a9,b9 // c9,d9
proof
let a9,b9,c9;
reconsider a=a9,b=b9,c =c9 as Element of OTS by Th47;
consider d such that
A1: a,b // c,d or a,b // d,c by Def12;
reconsider d9=d as Element of Lambda(OTS) by Th47;
take d9;
thus thesis by A1,Th48;
end;
Lm38: a9,b9 // c9,d9 implies c9,d9 // a9,b9
proof
reconsider a=a9,b=b9,c =c9,d=d9 as Element of the carrier of OTS by Th47;
assume
A1: a9,b9 // c9,d9;
per cases by A1,Th48;
suppose
a,b // c,d;
then c,d // a,b by Def12;
hence thesis by Th48;
end;
suppose
a,b // d,c;
then b,a // c,d by Def12;
then c,d // b,a by Def12;
hence thesis by Th48;
end;
end;
Lm39: a19<>b19 & a19,b19 // a9,b9 & a19,b19 // c9,d9 implies a9,b9 // c9,d9
proof
reconsider a1=a19,b1=b19,a=a9,b=b9,c =c9,d=d9 as Element of OTS by Th47;
assume that
A1: a19<>b19 and
A2: a19,b19 // a9,b9 and
A3: a19,b19 // c9,d9;
A4: a1,b1 // c,d or a1,b1 // d,c by A3,Th48;
a1,b1 // a,b or a1,b1 // b,a by A2,Th48;
then a,b // c,d or a,b // d,c or b,a // c,d or b,a // d,c by A1,A4,Def12;
then a,b // c,d or a,b // d,c by Def12;
hence thesis by Th48;
end;
Lm40: a9,b9 // c9,d9 & a9,b9 // c9,d19 implies a9=b9 or d9=d19
proof
reconsider a=a9,b=b9,c =c9,d=d9,d1=d19 as Element of OTS by Th47;
assume a9,b9 // c9,d9 & a9,b9 // c9,d19;
then
A1: a,b // c,d & a,b // c,d1 or a,b // c,d & a,b // d1,c or a,b // d,c & a,b
// c,d1 or a,b // d,c & a,b // d1,c by Th48;
assume
A2: a9<>b9;
then d=d1 or d1,c // c,d or d,c // c,d1 or b,a // c,d & b,a // c,d1 by A1
,Def12;
then d=d1 or c =d & c =d1 by A2,Def12;
hence thesis;
end;
Lm41: a,b // a,b
proof
consider c such that
A1: a,b // a,c or a,b // c,a by Def12;
per cases by A1;
suppose
a,b // c,a;
then
A2: c,a // a,b by Def12;
then c =a by Def12;
hence thesis by A2,Def12;
end;
suppose
A3: a,b // a,c;
per cases;
suppose
A4: a<>c;
a,c // a,b by A3,Def12;
hence thesis by A4,Def12;
end;
suppose
a=c;
then a,a // a,b by A3,Def12;
hence thesis by Def12;
end;
end;
end;
Lm42: a9,b9 // b9,a9
proof
reconsider a=a9,b=b9 as Element of OTS by Th47;
a,b // a,b by Lm41;
hence thesis by Th48;
end;
definition
let IT be non empty AffinStruct;
attr IT is TrapSpace-like means
for a9,b9,c9,d9,p9,q9 being Element of IT
holds a9,b9 // b9,a9 & (a9,b9 // c9,d9 & a9,b9 // c9,q9 implies a9=b9 or d9=q9)
& (p9<>q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9) & (a9,b9 //
c9,d9 implies c9,d9 // a9,b9) & ex x9 being Element of IT st a9,b9 // c9,x9;
end;
Lm43: for OTS be OrdTrapSpace holds Lambda(OTS) is TrapSpace-like
by Lm42,Lm40,Lm39,Lm38,Lm37;
registration
cluster strict TrapSpace-like for non empty AffinStruct;
existence
proof
set TS =Lambda(the OrdTrapSpace);
TS is TrapSpace-like by Lm43;
hence thesis;
end;
end;
definition
mode TrapSpace is TrapSpace-like non empty AffinStruct;
end;
registration
let OTS be OrdTrapSpace;
cluster Lambda(OTS) -> TrapSpace-like;
correctness by Lm43;
end;
definition
let IT be non empty AffinStruct;
attr IT is Regular means
for p,q,a,a1,b,b1,c,c1,d,d1 being Element
of IT st p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b //
c,d holds a1,b1 // c1,d1;
end;
registration
cluster strict Regular for non empty OrdTrapSpace;
existence
proof
set MOTS = the MidOrdTrapSpace;
set X = the AffinStruct of MOTS;
A1: now
let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of
MOTS such that
A2: a=a9 & b=b9 & c =c9 & d=d9;
hereby
assume a,b // c,d;
then [[a,b],[c,d]] in the CONGR of MOTS by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A2,ANALOAF:def 2;
end;
assume a9,b9 // c9,d9;
then [[a,b],[c,d]] in the CONGR of MOTS by A2,ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2;
end;
X is Regular
proof
let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X such that
A3: p<>q and
A4: p,q // a,a1 & p,q // b,b1 and
A5: p,q // c,c1 & p,q // d,d1 and
A6: a,b // c,d;
reconsider a9=a,b9=b,c9=c,d9=d,a19=a1,b19=b1,c19=c1,d19=d1,p9=p,q9=q as
Element of MOTS;
A7: p9,q9 // c9,c19 & p9,q9 // d9,d19 by A1,A5;
A8: a9,b9 // c9,d9 by A1,A6;
p9,q9 // a9,a19 & p9,q9 // b9,b19 by A1,A4;
then a19,b19 // c19,d19 by A3,A7,A8,Def11;
hence a1,b1 // c1,d1 by A1;
end;
hence thesis;
end;
end;
registration
let MOS be MidOrdTrapSpace;
cluster the AffinStruct of MOS -> Regular;
correctness
proof
set X=the AffinStruct of MOS;
now
let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X;
assume that
A1: p<>q and
A2: p,q // a,a1 & p,q // b,b1 and
A3: p,q // c,c1 & p,q // d,d1 and
A4: a,b // c,d;
reconsider a9=a,b9=b,c9=c,d9=d,a19=a1,b19=b1,c19=c1,d19=d1,p9=p,q9=q as
Element of MOS;
A5: now
let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of
MOS such that
A6: a=a9 & b=b9 & c =c9 & d=d9;
hereby
assume a,b // c,d;
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A6,ANALOAF:def 2;
end;
assume a9,b9 // c9,d9;
then [[a,b],[c,d]] in the CONGR of MOS by A6,ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2;
end;
then
A7: p9,q9 // c9,c19 & p9,q9 // d9,d19 by A3;
A8: a9,b9 // c9,d9 by A4,A5;
p9,q9 // a9,a19 & p9,q9 // b9,b19 by A2,A5;
then a19,b19 // c19,d19 by A1,A7,A8,Def11;
hence a1,b1 // c1,d1 by A5;
end;
hence thesis;
end;
end;