:: Analytical Metric Affine Spaces and Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received August 10, 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, RELAT_1, ARYTM_3, ARYTM_1, CARD_1,
SUPINF_2, ANALOAF, DIRAF, ZFMISC_1, STRUCT_0, SUBSET_1, XBOOLE_0,
SYMSP_1, INCSP_1, AFF_1, ANALMETR;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, ORDINAL1, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, NUMBERS, STRUCT_0, DIRAF, RELSET_1, RLVECT_1,
AFF_1, ANALOAF;
constructors DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, AFF_1;
registrations SUBSET_1, RELSET_1, XXREAL_0, STRUCT_0, ANALOAF, DIRAF, XREAL_0,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0;
equalities RLVECT_1;
theorems RLVECT_1, RELAT_1, AFF_1, FUNCSDOM, DIRAF, ANALOAF, TARSKI, XCMPLX_0,
XCMPLX_1, XREAL_1, XTUPLE_0;
schemes RELSET_1, SUBSET_1;
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;
Lm1: 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;
Lm2: for w,y holds 0*w + 0*y = 0.V
proof
let w,y;
thus 0*w + 0*y = 0.V + 0*y by RLVECT_1:10
.=0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
end;
Lm3: 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;
definition
let V;
let w,y;
pred Gen w,y means
:Def1:
(for u ex a1,a2 st u = a1*w + a2*y) &
for a1,a2 st a1*w + a2*y = 0.V holds a1=0 & a2=0;
end;
definition
let V;
let u,v,w,y;
pred u,v are_Ort_wrt w,y means
:Def2:
ex a1,a2,b1,b2 st u = a1*w + a2*y & v = b1*w + b2*y & a1*b1 + a2*b2 = 0;
end;
Lm4: 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 Lm1;
then -b1 + a1 =0 & -b2 + a2 = 0 by A1;
hence thesis;
end;
theorem Th1:
for w,y st Gen w,y holds (u,v are_Ort_wrt w,y iff for a1,a2,b1,b2
st u = a1*w + a2*y & v = b1*w + b2*y holds a1*b1 + a2*b2 = 0 )
proof
let w,y such that
A1: Gen w,y;
hereby
assume u,v are_Ort_wrt w,y;
then consider a1,a2,b1,b2 such that
A2: u = a1*w + a2*y and
A3: v = b1*w + b2*y and
A4: a1*b1 + a2*b2 = 0;
let a19,a29,b19,b29 be Real;
assume that
A5: u = a19*w + a29*y and
A6: v = b19*w + b29*y;
A7: b1=b19 by A1,A3,A6,Lm4;
a1=a19 & a2=a29 by A1,A2,A5,Lm4;
hence 0 = a19*b19 + a29*b29 by A1,A3,A4,A6,A7,Lm4;
end;
consider a1,a2 such that
A8: u = a1*w + a2*y by A1;
consider b1,b2 such that
A9: v = b1*w + b2*y by A1;
assume
for a1,a2,b1,b2 st u = a1*w + a2*y & v = b1*w + b2*y holds a1*b1 + a2*b2 = 0;
then a1*b1 + a2*b2 = 0 by A8,A9;
hence thesis by A8,A9;
end;
Lm5: Gen w,y implies w<>0.V & y<>0.V
proof
assume
A1: Gen w,y;
thus w<>0.V
proof
assume w=0.V;
then 0.V = 1*w by RLVECT_1:def 8
.= 1*w + 0.V by RLVECT_1:4
.= 1*w + 0*y by RLVECT_1:10;
hence contradiction by A1;
end;
thus y<>0.V
proof
assume y=0.V;
then 0.V = 1*y by RLVECT_1:def 8
.= 0.V + 1*y by RLVECT_1:4
.= 0*w + 1*y by RLVECT_1:10;
hence contradiction by A1;
end;
end;
theorem
w,y are_Ort_wrt w,y
proof
A1: y = 0.V + y by RLVECT_1:4
.= 0.V + 1*y by RLVECT_1:def 8
.= 0*w + 1*y by RLVECT_1:10;
A2: 1*0 + 0*1 = 0;
w = w + 0.V by RLVECT_1:4
.= 1*w + 0.V by RLVECT_1:def 8
.= 1*w + 0*y by RLVECT_1:10;
hence thesis by A1,A2;
end;
theorem Th3:
ex V st ex w,y st Gen w,y by Def1,FUNCSDOM:23;
theorem
u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y;
theorem Th5:
Gen w,y implies for u,v holds u,0.V are_Ort_wrt w,y & 0.V,v are_Ort_wrt w,y
proof
assume
A1: Gen w,y;
let u,v;
consider a1,a2 such that
A2: u = a1*w + a2*y by A1;
consider b1,b2 such that
A3: v = b1*w + b2*y by A1;
A4: 0.V = 0.V + 0.V by RLVECT_1:4
.= 0*w + 0.V by RLVECT_1:10
.= 0*w + 0*y by RLVECT_1:10;
a1*0 + a2*0 = 0;
hence u,0.V are_Ort_wrt w,y by A2,A4;
0*b1 + 0*b2 = 0;
hence thesis by A3,A4;
end;
theorem Th6:
u,v are_Ort_wrt w,y implies a*u,b*v are_Ort_wrt w,y
proof
assume u,v are_Ort_wrt w,y;
then consider a1,a2,b1,b2 such that
A1: u = a1*w + a2*y and
A2: v = b1*w + b2*y and
A3: a1*b1 + a2*b2 = 0;
A4: b*v = b*(b1*w) + b*(b2*y) by A2,RLVECT_1:def 5
.= (b*b1)*w + b*(b2*y) by RLVECT_1:def 7
.= (b*b1)*w + (b*b2)*y by RLVECT_1:def 7;
A5: (a*a1)*(b*b1) + (a*a2)*(b*b2) = b*a*(a1*b1 + a2*b2) .= 0 by A3;
a*u = a*(a1*w) + a*(a2*y) by A1,RLVECT_1:def 5
.= (a*a1)*w + a*(a2*y) by RLVECT_1:def 7
.= (a*a1)*w + (a*a2)*y by RLVECT_1:def 7;
hence thesis by A4,A5;
end;
theorem Th7:
u,v are_Ort_wrt w,y implies a*u,v are_Ort_wrt w,y & u,b*v are_Ort_wrt w,y
proof
A1: v = 1*v & u = 1*u by RLVECT_1:def 8;
assume u,v are_Ort_wrt w,y;
hence thesis by A1,Th6;
end;
theorem Th8:
Gen w,y implies for u ex v st u,v are_Ort_wrt w,y & v<>0.V
proof
assume
A1: Gen w,y;
let u;
consider a1,a2 such that
A2: u = a1*w + a2*y by A1;
A3: now
set v = a2*w + (-a1)*y;
assume
A4: u<>0.V;
take v;
a1*a2 + a2*(-a1) = 0;
hence u,v are_Ort_wrt w,y by A2;
v<>0.V
proof
assume v=0.V;
then a2 = 0 & -a1 = 0 by A1;
then u = 0*w + 0.V by A2,RLVECT_1:10
.= 0*w by RLVECT_1:4
.= 0.V by RLVECT_1:10;
hence contradiction by A4;
end;
hence v<>0.V;
end;
now
assume
A5: u = 0.V;
take v=w;
thus u,v are_Ort_wrt w,y by A1,A5,Th5;
thus v<>0.V by A1,Lm5;
end;
hence thesis by A3;
end;
theorem Th9:
Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v<>0.V
implies ex a,b st a*u1 = b*u2 & (a<>0 or b<>0)
proof
assume that
A1: Gen w,y and
A2: v,u1 are_Ort_wrt w,y and
A3: v,u2 are_Ort_wrt w,y and
A4: v<>0.V;
consider a1,a2,b1,b2 such that
A5: v = a1*w + a2*y and
A6: u1 = b1*w + b2*y and
A7: a1*b1 + a2*b2 = 0 by A2;
consider a19,a29,c1,c2 being Real such that
A8: v = a19*w + a29*y and
A9: u2 = c1*w + c2*y and
A10: a19*c1 + a29*c2 = 0 by A3;
A11: a2 = a29 by A1,A5,A8,Lm4;
A12: a1 = a19 by A1,A5,A8,Lm4;
A13: now
assume
A14: a1=0;
then
A15: a2<>0 by A4,A5,Lm2;
then c2 = 0 by A10,A12,A11,A14,XCMPLX_1:6;
then u2 = c1*w + 0.V by A9,RLVECT_1:10;
then
A16: u2 = c1*w by RLVECT_1:4;
b2 = 0 by A7,A14,A15,XCMPLX_1:6;
then
A17: u1 = b1*w + 0.V by A6,RLVECT_1:10;
then
A18: u1 = b1*w by RLVECT_1:4;
A19: now
assume b1=0;
then 1*u1 = 0*w by A18,RLVECT_1:def 8
.= 0.V by RLVECT_1:10
.= 0*u2 by RLVECT_1:10;
hence thesis;
end;
c1*u1 = c1*(b1*w) by A17,RLVECT_1:4
.= (b1*c1)*w by RLVECT_1:def 7
.= b1*u2 by A16,RLVECT_1:def 7;
hence thesis by A19;
end;
now
A20: c2*(((-a2)*b2)*a1") = b2*(((-a2)*c2)*a1");
assume
A21: a1<>0;
A22: b1 = 1*b1 .= (a1*a1")*b1 by A21,XCMPLX_0:def 7
.= (a1*b1)*a1"
.= ((-a2)*b2)*a1" by A7;
A23: c1 = 1*c1 .= (a1*a1")*c1 by A21,XCMPLX_0:def 7
.= (a1*c1)*a1"
.= ((-a2)*c2)*a1" by A1,A5,A8,A10,A11,Lm4;
then
A24: b2*u2 = (b2*(((-a2)*c2)*a1"))*w + (b2*c2)*y by A9,Lm3;
A25: now
assume
A26: c2<>0 or b2<>0;
take a=c2,b=b2;
thus a*u1 = b*u2 & (a<>0 or b<>0) by A6,A22,A24,A20,A26,Lm3;
end;
now
assume b2=0 & c2=0;
then 1*u1 = 1*u2 by A6,A9,A22,A23;
hence thesis;
end;
hence thesis by A25;
end;
hence thesis by A13;
end;
theorem Th10:
Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies u,
v1+v2 are_Ort_wrt w,y & u,v1-v2 are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u,v1 are_Ort_wrt w,y and
A3: u,v2 are_Ort_wrt w,y;
consider a1,a2,b1,b2 such that
A4: u = a1*w + a2*y and
A5: v1 = b1*w + b2*y and
A6: a1*b1 + a2*b2 = 0 by A2;
consider a19,a29,c1,c2 being Real such that
A7: u = a19*w + a29*y and
A8: v2 = c1*w + c2*y and
A9: a19*c1 + a29*c2 = 0 by A3;
A10: a1 = a19 & a2 = a29 by A1,A4,A7,Lm4;
then
A11: a1*(b1+c1) + a2*(b2+c2) = 0 by A6,A9;
A12: a1*(b1-c1) + a2*(b2-c2) = 0 by A6,A9,A10;
v1 + v2 = (b1 + c1)*w + (b2 + c2)*y by A5,A8,Lm1;
hence u,v1+v2 are_Ort_wrt w,y by A4,A11;
v1 - v2 = (b1 - c1)*w + (b2 - c2)*y by A5,A8,Lm1;
hence thesis by A4,A12;
end;
theorem Th11:
Gen w,y & u,u are_Ort_wrt w,y implies u = 0.V
proof
A1: now
let a such that
A2: a<>0;
0 < a implies 0 < a*a by XREAL_1:129;
hence 0 < a*a by A2,XREAL_1:130;
end;
assume that
A3: Gen w,y and
A4: u,u are_Ort_wrt w,y;
consider a1,a2,b1,b2 such that
A5: u = a1*w + a2*y and
A6: u = b1*w + b2*y and
A7: a1*b1 + a2*b2 = 0 by A4;
A8: a1=b1 & a2=b2 by A3,A5,A6,Lm4;
A9: a2 = 0
proof
assume a2<>0;
then 0 < a2*a2 by A1;
hence contradiction by A7,A8,XREAL_1:29,63;
end;
a1 = 0
proof
assume a1<>0;
then 0 < a1*a1 by A1;
hence contradiction by A7,A8,XREAL_1:29,63;
end;
hence u = 0*w + 0.V by A5,A9,RLVECT_1:10
.= 0*w by RLVECT_1:4
.= 0.V by RLVECT_1:10;
end;
theorem Th12:
Gen w,y & u,u1-u2 are_Ort_wrt w,y & u1,u2-u are_Ort_wrt w,y
implies u2,u-u1 are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u,u1-u2 are_Ort_wrt w,y and
A3: u1,u2-u are_Ort_wrt w,y;
consider a1,a2 such that
A4: u = a1*w + a2*y by A1;
consider c1,c2 such that
A5: u2 = c1*w + c2*y by A1;
consider b1,b2 such that
A6: u1 = b1*w + b2*y by A1;
A7: u-u1 = (a1-b1)*w + (a2-b2)*y by A4,A6,Lm1;
u2-u = (c1-a1)*w + (c2-a2)*y by A4,A5,Lm1;
then
A8: b1*(c1-a1) + b2*(c2-a2) = 0 by A1,A3,A6,Th1;
u1-u2 = (b1-c1)*w + (b2-c2)*y by A6,A5,Lm1;
then a1*(b1-c1) + a2*(b2-c2) = 0 by A1,A2,A4,Th1;
then 0 = c1*(a1-b1) + c2*(a2-b2) by A8;
hence thesis by A5,A7;
end;
theorem Th13:
Gen w,y & u <> 0.V implies ex a st v - a*u,u are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: u <> 0.V;
consider a1,a2 such that
A3: u = a1*w + a2*y by A1;
consider b1,b2 such that
A4: v = b1*w + b2*y by A1;
set a = (b1*a1 + b2*a2)*(a1*a1 + a2*a2)";
a*u = (a*a1)*w + (a*a2)*y by A3,Lm3;
then
A5: v - a*u = (b1-a*a1)*w + (b2-a*a2)*y by A4,Lm1;
A6: (b1-a*a1)*a1 + (b2-a*a2)*a2 = (a1*b1 + a2*b2) + (-1)*(a1*(a*a1) + a2*(a
*a2));
A7: a1*a1 + a2*a2 <> 0 by A1,A2,Th11,A3,Def2;
(-1)*(a1*(a*a1) + a2*(a*a2)) = (-1)*((b1*a1 + b2*a2)*((a1*a1 + a2*a2)"*
(a1*a1 + a2*a2)))
.= (-1)*((b1*a1 + b2*a2)*1) by A7,XCMPLX_0:def 7
.= -(a1*b1 + a2*b2);
then v - a*u,u are_Ort_wrt w,y by A3,A5,A6;
hence thesis;
end;
theorem Th14:
(u,v // u1,v1 or u,v // v1,u1) iff ex a,b st a*(v-u) = b*(v1-u1)
& (a<>0 or b<>0)
proof
A1: now
let w,y,w1,y1 be VECTOR of V;
given a,b such that
A2: a*(y-w) = b*(y1-w1) & a=0 and
A3: b<>0;
0.V = b*(y1-w1) by A2,RLVECT_1:10;
then y1-w1 = 0.V by A3,RLVECT_1:11;
then y1 = w1 by RLVECT_1:21;
hence w,y // w1,y1 by ANALOAF:9;
end;
A4: now
let w,y,w1,y1 be VECTOR of V;
given a,b such that
A5: a*(y-w) = b*(y1-w1) and
A6: 0<a and
A7: b<0;
A8: a*(y-w) = b*(-(w1-y1)) by A5,RLVECT_1:33
.= (-b)*(w1-y1) by RLVECT_1:24;
0<-b by A7,XREAL_1:58;
hence w,y // y1,w1 by A6,A8,ANALOAF:def 1;
end;
A9: now
given a,b such that
A10: a*(v-u) = b*(v1-u1) and
A11: a<>0 or b<>0;
A12: now
A13: now
assume a<0 & b<0;
then
A14: 0< -a & 0< -b by XREAL_1:58;
(-a)*(u-v) = a*(-(u-v)) by RLVECT_1:24
.= b*(v1-u1) by A10,RLVECT_1:33
.= b*(-(u1-v1)) by RLVECT_1:33
.= (-b)*(u1-v1) by RLVECT_1:24;
then v,u // v1,u1 by A14,ANALOAF:def 1;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:12;
end;
A15: now
assume a<0 & 0<b;
then u1,v1 // v,u by A4,A10;
then v,u // u1, v1 by ANALOAF:12;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:12;
end;
assume
A16: a<>0 & b<>0;
0<a & b<0 implies ( u,v // u1,v1 or u,v // v1,u1) by A4,A10;
hence u,v // u1,v1 or u,v // v1,u1 by A10,A16,A15,A13,ANALOAF:def 1;
end;
now
assume b=0;
then u1,v1 // u,v by A1,A10,A11;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:12;
end;
hence u,v // u1,v1 or u,v // v1,u1 by A1,A10,A12;
end;
A17: now
let w,y,w1,y1 be VECTOR of V such that
A18: w,y // w1,y1;
A19: now
assume w=y;
then 1*(y-w) = 0.V by RLVECT_1:10,15
.= 0*(y1-w1) by RLVECT_1:10;
hence ex a,b st a*(y-w) = b*(y1-w1) & (a<>0 or b<>0);
end;
A20: now
assume w1=y1;
then 1*(y1-w1) = 0.V by RLVECT_1:10,15
.= 0*(y-w) by RLVECT_1:10;
hence ex a,b st a*(y-w) = b*(y1-w1) & (a<>0 or b<>0);
end;
(ex a,b st 0<a & 0<b & a*(y-w)=b*(y1-w1)) implies ex a,b st a*(y-w) =
b*(y1-w1) & (a<>0 or b<>0);
hence ex a,b st a*(y-w) = b*(y1-w1) & (a<>0 or b<>0) by A18,A19,A20,
ANALOAF:def 1;
end;
now
assume u,v // v1,u1;
then consider a,b such that
A21: a*(v-u) = b*(u1-v1) and
A22: a<>0 or b<>0 by A17;
A23: a<>0 or -b<>0 by A22;
(-b)*(v1-u1) = b*(-(v1-u1)) by RLVECT_1:24
.= a*(v-u) by A21,RLVECT_1:33;
hence ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0 ) by A23;
end;
hence thesis by A17,A9;
end;
theorem Th15:
[[u,v],[u1,v1]] in lambda(DirPar(V)) iff ex a,b st a*(v-u) = b*(
v1-u1) & (a<>0 or b<>0)
proof
[[u,v],[u1,v1]] in lambda(DirPar(V)) iff [[u,v],[u1,v1]] in DirPar(V) or
[[u,v],[v1,u1]] in DirPar(V) by DIRAF:def 1;
then
[[u,v],[u1,v1]] in lambda(DirPar(V)) iff (u,v // u1,v1 or u,v // v1,u1)
by ANALOAF:22;
hence thesis by Th14;
end;
definition
let V;
let u,u1,v,v1,w,y;
pred u,u1,v,v1 are_Ort_wrt w,y means
u1-u,v1-v are_Ort_wrt w,y;
end;
definition
let V;
let w,y;
func Orthogonality(V,w,y) -> Relation of [:the carrier of V,the carrier of V
:] means
:Def4:
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_Ort_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_Ort_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_Ort_wrt w,y by A1;
assume ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_Ort_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_Ort_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_Ort_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_Ort_wrt w,y by A2;
hence thesis by A3;
end;
hence thesis by RELAT_1:def 2;
end;
end;
reserve p,p1,q,q1 for Element of Lambda(OASpace(V));
theorem Th16:
the carrier of Lambda(OASpace(V)) = the carrier of V
proof
Lambda(OASpace(V)) = AffinStruct(#the carrier of OASpace(V), lambda(the
CONGR of OASpace(V))#) & OASpace(V) = AffinStruct (#the carrier of V, DirPar(V)
#) by ANALOAF:def 4,DIRAF:def 2;
hence thesis;
end;
theorem Th17:
the CONGR of Lambda(OASpace(V)) = lambda(DirPar(V))
proof
Lambda(OASpace(V)) = AffinStruct(#the carrier of OASpace(V), lambda(the
CONGR of OASpace(V))#) & OASpace(V) = AffinStruct (#the carrier of V, DirPar(V)
#) by ANALOAF:def 4,DIRAF:def 2;
hence thesis;
end;
theorem
p=u & q=v & p1=u1 & q1=v1 implies (p,q // p1,q1 iff ex a,b st a*(v-u)
= b*(v1-u1) & (a<>0 or b<>0) )
proof
assume
A1: p=u & q=v & p1=u1 & q1=v1;
hereby
assume p,q // p1,q1;
then [[p,q],[p1,q1]] in the CONGR of Lambda(OASpace(V)) by ANALOAF:def 2;
then [[u,v],[u1,v1]] in lambda(DirPar(V)) by A1,Th17;
hence ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by Th15;
end;
given a,b such that
A2: a*(v-u) = b*(v1-u1) &( a<>0 or b<>0);
[[u,v],[u1,v1]] in lambda(DirPar(V)) by A2,Th15;
then [[p,q],[p1,q1]] in the CONGR of Lambda(OASpace(V)) by A1,Th17;
hence thesis by ANALOAF:def 2;
end;
definition
struct(1-sorted) OrtStr (# carrier -> set,
orthogonality -> Relation of [:the carrier,the carrier:] #);
end;
definition
struct(AffinStruct,OrtStr) ParOrtStr (# carrier -> set,
CONGR, orthogonality -> Relation of [:the carrier,the carrier:] #);
end;
registration
cluster non empty for ParOrtStr;
existence
proof
set A = the non empty set,C = the Relation of [:A,A:];
take ParOrtStr (#A,C,C#);
thus the carrier of ParOrtStr (#A,C,C#) is non empty;
end;
end;
registration
cluster non empty for OrtStr;
existence
proof
set A = the non empty set,C = the Relation of [:A,A:];
take OrtStr (#A,C#);
thus the carrier of OrtStr (#A,C#) is non empty;
end;
end;
reserve POS for non empty ParOrtStr;
definition
let POS be OrtStr;
let a,b,c,d be Element of POS;
pred a,b _|_ c,d means
[[a,b],[c,d]] in the orthogonality of POS;
end;
definition
let V,w,y;
func AMSpace(V,w,y) -> strict ParOrtStr equals
ParOrtStr(#the carrier of V,
lambda(DirPar(V)),Orthogonality(V,w,y)#);
correctness;
end;
registration
let V,w,y;
cluster AMSpace(V,w,y) -> non empty;
coherence;
end;
theorem
the carrier of AMSpace(V,w,y) = the carrier of V & the CONGR of
AMSpace(V,w,y) = lambda(DirPar(V)) & the orthogonality of AMSpace(V,w,y) =
Orthogonality(V,w,y);
definition
::$CD
end;
registration
let POS;
cluster the AffinStruct of POS -> non empty;
coherence;
end;
theorem Th20:
the AffinStruct of AMSpace(V,w,y) = Lambda(OASpace(V))
proof
set Y = OASpace(V);
the carrier of Lambda(Y) = the carrier of V by Th16;
hence thesis by Th17;
end;
reserve p,p1,p2,q,q1,r,r1,r2 for Element of AMSpace(V,w,y);
theorem Th21:
p=u & p1=u1 & q=v & q1=v1 implies (p,q _|_ p1,q1 iff u,v,u1,v1
are_Ort_wrt w,y)
proof
assume
A1: p=u & p1=u1 & q=v & q1=v1;
hereby
assume p,q _|_ p1,q1;
then consider u9,v9,u19,v19 being VECTOR of V such that
A2: [u,v] = [u9,v9] and
A3: [u1,v1] = [u19,v19] and
A4: u9,v9,u19,v19 are_Ort_wrt w,y by A1,Def4;
A5: u1=u19 by A3,XTUPLE_0:1;
u=u9 & v=v9 by A2,XTUPLE_0:1;
hence u,v,u1,v1 are_Ort_wrt w,y by A3,A4,A5,XTUPLE_0:1;
end;
assume u,v,u1,v1 are_Ort_wrt w,y;
hence thesis by A1,Def4;
end;
theorem Th22:
p=u & q=v & p1=u1 & q1=v1 implies (p,q // p1,q1 iff ex a,b st a*
(v-u) = b*(v1-u1) & (a<>0 or b<>0) )
proof
assume
A1: p=u & q=v & p1=u1 & q1=v1;
hereby
assume p,q // p1,q1;
then [[p,q],[p1,q1]] in the CONGR of AMSpace(V,w,y) by ANALOAF:def 2;
hence ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by A1,Th15;
end;
given a,b such that
A2: a*(v-u) = b*(v1-u1) &( a<>0 or b<>0);
[[u,v],[u1,v1]] in lambda(DirPar(V)) by A2,Th15;
hence thesis by A1,ANALOAF:def 2;
end;
theorem Th23:
p,q _|_ p1,q1 implies p1,q1 _|_ p,q
proof
reconsider u=p,v=q,u1=p1,v1=q1 as Element of V;
assume p,q _|_ p1,q1;
then u,v,u1,v1 are_Ort_wrt w,y by Th21;
then v-u,v1-u1 are_Ort_wrt w,y;
then v1-u1,v-u are_Ort_wrt w,y;
then u1,v1,u,v are_Ort_wrt w,y;
hence thesis by Th21;
end;
theorem Th24:
p,q _|_ p1,q1 implies p,q _|_ q1,p1
proof
reconsider u=p,v=q,u1=p1,v1=q1 as Element of V;
assume p,q _|_ p1,q1;
then u,v,u1,v1 are_Ort_wrt w,y by Th21;
then v-u,v1-u1 are_Ort_wrt w,y;
then
A1: v-u,(-1)*(v1-u1) are_Ort_wrt w,y by Th7;
(-1)*(v1-u1) = -(v1-u1) by RLVECT_1:16
.= u1-v1 by RLVECT_1:33;
then u,v,v1,u1 are_Ort_wrt w,y by A1;
hence thesis by Th21;
end;
theorem Th25:
Gen w,y implies for p,q,r holds p,q _|_ r,r
proof
assume
A1: Gen w,y;
let p,q,r;
reconsider u=p,v=q,u1=r as Element of V;
u1-u1 = 0.V by RLVECT_1:15;
then v-u,u1-u1 are_Ort_wrt w,y by A1,Th5;
then u,v,u1,u1 are_Ort_wrt w,y;
hence thesis by Th21;
end;
theorem Th26:
p,p1 _|_ q,q1 & p,p1 // r,r1 implies p=p1 or q,q1 _|_ r,r1
proof
assume that
A1: p,p1 _|_ q,q1 and
A2: p,p1 // r,r1;
reconsider u=p,v=p1,u1=q,v1=q1,u2=r,v2=r1 as Element of V;
consider a,b such that
A3: a*(v-u) = b*(v2-u2) and
A4: a<>0 or b<>0 by A2,Th22;
assume
A5: p<>p1;
b<>0
proof
assume
A6: b=0;
then a*(v-u) = 0.V by A3,RLVECT_1:10;
then v-u = 0.V by A4,A6,RLVECT_1:11;
hence contradiction by A5,RLVECT_1:21;
end;
then
A7: v2-u2 = b"*(a*(v-u)) by A3,ANALOAF:5
.= (b"*a)*(v-u) by RLVECT_1:def 7;
u,v,u1,v1 are_Ort_wrt w,y by A1,Th21;
then v-u,v1-u1 are_Ort_wrt w,y;
then v2-u2,v1-u1 are_Ort_wrt w,y by A7,Th7;
then v1-u1,v2-u2 are_Ort_wrt w, y;
then u1,v1,u2,v2 are_Ort_wrt w,y;
hence thesis by Th21;
end;
theorem Th27:
Gen w,y implies for p,q,r ex r1 st p,q _|_ r,r1 & r<>r1
proof
assume
A1: Gen w,y;
let p,q,r;
reconsider u=p,v=q,u1=r as Element of V;
consider v2 such that
A2: v-u,v2 are_Ort_wrt w,y and
A3: v2<>0.V by A1,Th8;
set v1 = u1+v2;
reconsider r1=v1 as Element of AMSpace(V,w,y);
A4: v1-u1 = v2+(u1-u1) by RLVECT_1:def 3
.= v2+0.V by RLVECT_1:15
.= v2 by RLVECT_1:4;
then u,v,u1,v1 are_Ort_wrt w,y by A2;
then
A5: p,q _|_ r,r1 by Th21;
r<>r1 by A3,A4,RLVECT_1:15;
hence thesis by A5;
end;
theorem Th28:
Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 implies p=p1 or q,q1 // r,r1
proof
assume that
A1: Gen w,y and
A2: p,p1 _|_ q,q1 and
A3: p,p1 _|_ r,r1;
reconsider u=p,v=p1,u1=q,v1=q1,u2=r,v2=r1 as Element of V;
u,v,u2,v2 are_Ort_wrt w,y by A3,Th21;
then
A4: v-u,v2-u2 are_Ort_wrt w,y;
assume p<>p1;
then
A5: v-u <> 0.V by RLVECT_1:21;
u,v,u1,v1 are_Ort_wrt w,y by A2,Th21;
then v-u,v1-u1 are_Ort_wrt w,y;
then ex a,b st a*(v1-u1) = b*(v2-u2) & (a<>0 or b<>0) by A1,A4,A5,Th9;
hence thesis by Th22;
end;
theorem Th29:
Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2
proof
assume that
A1: Gen w,y and
A2: p,q _|_ r,r1 and
A3: p,q _|_ r,r2;
reconsider u=p,v=q,w1=r,v1=r1,v2=r2 as Element of V;
u,v,w1,v2 are_Ort_wrt w,y by A3,Th21;
then
A4: v-u,v2-w1 are_Ort_wrt w,y;
A5: (v2-w1)-(v1-w1) = v2-((v1-w1)+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;
u,v,w1,v1 are_Ort_wrt w,y by A2,Th21;
then v-u,v1-w1 are_Ort_wrt w,y;
then v-u,(v2-w1)-(v1-w1) are_Ort_wrt w,y by A1,A4,Th10;
then u,v,v1,v2 are_Ort_wrt w,y by A5;
hence thesis by Th21;
end;
theorem Th30:
Gen w,y & p,q _|_ p,q implies p = q
proof
assume that
A1: Gen w,y and
A2: p,q _|_ p,q;
reconsider u=p,v=q as Element of V;
u,v,u,v are_Ort_wrt w,y by A2,Th21;
then v-u,v-u are_Ort_wrt w,y;
then v-u = 0.V by A1,Th11;
hence thesis by RLVECT_1:21;
end;
theorem
Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1
proof
assume that
A1: Gen w,y and
A2: p,q _|_ p1,p2 and
A3: p1,q _|_ p2,p;
reconsider u=p,v=q,u1=p1,u2=p2 as Element of V;
u,v,u1,u2 are_Ort_wrt w,y by A2,Th21;
then
A4: v-u,u2-u1 are_Ort_wrt w,y;
u1,v,u2,u are_Ort_wrt w,y by A3,Th21;
then
A5: v-u1,u-u2 are_Ort_wrt w,y;
A6: now
let u,v,w;
thus (u-v)-(u-w) = (w-u) + (u-v) by RLVECT_1:33
.= w-v by ANALOAF:1;
end;
then
A7: (v-u)-(v-u1)=u1-u;
(v-u1)-(v-u2)=u2-u1 & (v-u2)-(v-u)=u-u2 by A6;
then v-u2,(v-u)-(v-u1) are_Ort_wrt w,y by A1,A4,A5,Th12;
then u2,v,u,u1 are_Ort_wrt w,y by A7;
hence thesis by Th21;
end;
theorem Th32:
Gen w,y & p<>p1 implies for q ex q1 st p,p1 // p,q1 & p,p1 _|_ q1,q
proof
assume that
A1: Gen w,y and
A2: p<>p1;
let q;
reconsider u=p,v=q,u1=p1 as Element of V;
u1-u <> 0.V by A2,RLVECT_1:21;
then consider a such that
A3: (v-u) - a*(u1-u),u1-u are_Ort_wrt w,y by A1,Th13;
set v1 = u + a*(u1-u);
reconsider q1=v1 as Element of AMSpace(V,w,y);
v-v1 = (v-u)- a*(u1-u) by RLVECT_1:27;
then u1-u,v-v1 are_Ort_wrt w,y by A3;
then u,u1,v1,v are_Ort_wrt w,y;
then
A4: p,p1 _|_ q1,q by Th21;
a*(u1-u) = a*(u1-u)+0.V by RLVECT_1:4
.= a*(u1-u)+(u-u) by RLVECT_1:15
.= v1-u by RLVECT_1:def 3
.= 1*(v1-u) by RLVECT_1:def 8;
then p,p1 // p,q1 by Th22;
hence thesis by A4;
end;
consider V0 being RealLinearSpace such that
Lm6: ex w,y being VECTOR of V0 st Gen w,y by Th3;
consider w0,y0 being VECTOR of V0 such that
Lm7: Gen w0,y0 by Lm6;
Lm8: now
set X = AffinStruct(#the carrier of AMSpace(V0,w0,y0), the CONGR of AMSpace(
V0,w0,y0)#);
A1: X = Lambda(OASpace(V0)) by Th20;
for a,b being Real st a*w0 + b*y0 = 0.V0 holds a=0 & b=0 by Lm7;
then OASpace(V0) is OAffinSpace by ANALOAF:26;
hence
AffinStruct(#the carrier of AMSpace(V0,w0,y0), the CONGR of AMSpace(V0,
w0,y0)#) is AffinSpace & (for a,b,c,d,p,q,r,s being Element of AMSpace(V0,w0,y0
) holds (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_
d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a
,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s)) & (for a,b,c being Element of
AMSpace(V0,w0,y0) st a<>b ex x being Element of AMSpace(V0,w0,y0) st a,b // a,x
& a,b _|_ x,c) & for a,b,c being Element of AMSpace(V0,w0,y0) ex x being
Element of AMSpace(V0,w0,y0) st a,b _|_ c,x & c <>x by A1,Lm7,Th23,Th24,Th25
,Th26,Th27,Th29,Th30,Th32,DIRAF:41;
end;
definition
let IT be non empty ParOrtStr;
attr IT is OrtAfSp-like means
:Def7:
AffinStruct(#the carrier of IT,the
CONGR of IT#) is AffinSpace & (for a,b,c,d,p,q,r,s being Element of IT holds (a
,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d
_|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q
& a,b _|_ p,s implies a,b _|_ q,s)) & (for a,b,c being Element of IT st a<>b ex
x being Element of IT st a,b // a,x & a,b _|_ x,c) & for a,b,c being Element of
IT ex x being Element of IT st a,b _|_ c,x & c <>x;
end;
registration
cluster strict OrtAfSp-like for non empty ParOrtStr;
existence by Def7,Lm8;
end;
definition
mode OrtAfSp is OrtAfSp-like non empty ParOrtStr;
end;
theorem
Gen w,y implies AMSpace(V,w,y) is OrtAfSp
proof
set POS = AMSpace(V,w,y);
set X = AffinStruct(#the carrier of POS,the CONGR of POS#);
assume
A1: Gen w,y;
then
A2: for a,b,c be Element of POS holds ex x being Element of POS st a,b _|_ c
,x & c <>x by Th27;
A3: X = Lambda(OASpace(V)) by Th20;
for a,b being Real st a*w + b*y = 0.V holds a=0 & b=0 by A1;
then OASpace(V) is OAffinSpace by ANALOAF:26;
then
A4: X is AffinSpace by A3,DIRAF:41;
( for a,b,c,d,p,q,r,s be Element of POS holds (a,b _|_ a,b implies a=b)
& a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q
& a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ p,s implies a
,b _|_ q,s))& for a,b,c be Element of POS holds a<>b implies ex x being Element
of POS st a,b // a,x & a,b _|_ x,c by A1,Th23,Th24,Th25,Th26,Th29,Th30,Th32;
hence thesis by A2,A4,Def7;
end;
consider V0 being RealLinearSpace such that
Lm9: ex w,y being VECTOR of V0 st Gen w,y by Th3;
consider w0,y0 being VECTOR of V0 such that
Lm10: Gen w0,y0 by Lm9;
Lm11: now
set X = AffinStruct(#the carrier of AMSpace(V0,w0,y0), the CONGR of AMSpace(
V0,w0,y0)#);
A1: X = Lambda(OASpace(V0)) by Th20;
( for a,b being Real st a*w0 + b*y0 = 0.V0 holds a=0 & b=0)& for w1
being VECTOR of V0 ex a,b being Real st w1 = a*w0+b*y0 by Lm10;
then OASpace(V0) is OAffinPlane by ANALOAF:28;
hence
AffinStruct(#the carrier of AMSpace(V0,w0,y0), the CONGR of AMSpace(V0,
w0,y0)#) is AffinPlane & (for a,b,c,d,p,q,r,s being Element of AMSpace(V0,w0,y0
) holds (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_
d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a
,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b)) & for a,b,c being Element
of AMSpace(V0,w0,y0) ex x being Element of AMSpace(V0,w0,y0) st a,b _|_ c,x & c
<>x by A1,Lm10,Th23,Th24,Th25,Th26,Th27,Th28,Th30,DIRAF:45;
end;
definition
let IT be non empty ParOrtStr;
attr IT is OrtAfPl-like means
:Def8:
AffinStruct(#the carrier of IT,the
CONGR of IT#) is AffinPlane & (for a,b,c,d,p,q,r,s being Element of IT holds (a
,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d
_|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q
& a,b _|_ r,s implies p,q // r,s or a=b)) & for a,b,c being Element of IT ex x
being Element of IT st a,b _|_ c,x & c <>x;
end;
registration
cluster strict OrtAfPl-like for non empty ParOrtStr;
existence by Def8,Lm11;
end;
definition
mode OrtAfPl is OrtAfPl-like non empty ParOrtStr;
end;
theorem
Gen w,y implies AMSpace(V,w,y) is OrtAfPl
proof
set POS = AMSpace(V,w,y);
set X = AffinStruct(#the carrier of POS,the CONGR of POS#);
A1: X = Lambda(OASpace(V)) by Th20;
assume
A2: Gen w,y;
then
( for a,b being Real st a*w + b*y = 0.V holds a=0 & b=0)&
for w1 ex a,b being Real st w1 = a*w+b*y;
then OASpace(V) is OAffinPlane by ANALOAF:28;
then
A3: X is AffinPlane by A1,DIRAF:45;
( for a,b,c,d,p,q,r,s be Element of POS holds (a,b _|_ a,b implies a=b)
& a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q
& a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p
,q // r,s or a=b))& for a,b,c be Element of POS holds ex x being Element of POS
st a,b _|_ c,x & c <>x by A2,Th23,Th24,Th25,Th26,Th27,Th28,Th30;
hence thesis by A3,Def8;
end;
theorem
for x being set holds (x is Element of POS iff
x is Element of the AffinStruct of POS);
theorem Th36:
for a,b,c,d being Element of POS, a9,b9,c9,d9 being Element of
the AffinStruct of POS st a=a9& b=b9 & c = c9 & d=d9
holds (a,b // c,d iff a9,b9 // c9,d9)
proof
set AF = the AffinStruct of POS;
let a,b,c,d be Element of POS, a9,b9,c9,d9 be Element of the AffinStruct of
POS such that
A1: a=a9 & b=b9 & c = c9 & d=d9;
hereby
assume a,b // c,d;
then [[a9,b9],[c9,d9]] in the CONGR of AF by A1,ANALOAF:def 2;
hence a9,b9 // c9,d9 by ANALOAF:def 2;
end;
assume a9,b9 // c9,d9;
then [[a,b],[c,d]] in the CONGR of POS by A1,ANALOAF:def 2;
hence thesis by ANALOAF:def 2;
end;
registration
let POS be OrtAfSp;
cluster the AffinStruct of POS -> AffinSpace-like non trivial;
correctness by Def7;
end;
registration
let POS be OrtAfPl;
cluster the AffinStruct of POS -> 2-dimensional AffinSpace-like non trivial;
correctness by Def8;
end;
theorem Th37:
for POS being OrtAfPl holds POS is OrtAfSp
proof
let POS be OrtAfPl;
for a,b,c,d,p,q,r,s being Element of POS holds (a,b _|_ p,q & a,b _|_ p,
s implies a,b _|_ q,s)
proof
let a,b,c,d,p,q,r,s be Element of POS such that
A1: a,b _|_ p,q and
A2: a,b _|_ p,s;
A3: now
reconsider p9=p,q9=q,s9=s as Element of the AffinStruct of POS;
assume that
A4: a<>b and
A5: p<>q;
p,q // p,s by A1,A2,A4,Def8;
then p9,q9 // p9,s9 by Th36;
then q9,p9 // q9,s9 by DIRAF:40;
then p9,q9 // q9,s9 by AFF_1:4;
then
A6: p,q // q,s by Th36;
p,q _|_ a,b by A1,Def8;
hence thesis by A5,A6,Def8;
end;
now
assume a=b;
then q,s _|_ a,b by Def8;
hence thesis by Def8;
end;
hence thesis by A2,A3;
end;
then
A7: for a,b,c,d,p,q,r,s be Element of POS holds (a,b _|_ a,b implies a=b) &
a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q &
a,b // r,s implies p,q _|_ r,s or a=b) &( a,b _|_ p,q & a,b _|_ p,s implies a,b
_|_ q,s) by Def8;
A8: for a,b,c being Element of POS st a<>b ex x being Element of POS st a,b
// a,x & a,b _|_ x,c
proof
let a,b,c be Element of POS such that
A9: a<>b;
consider y being Element of POS such that
A10: a,b _|_ c,y and
A11: c <>y by Def8;
reconsider a9=a,b9=b,c9=c,y9=y as Element of the AffinStruct of POS;
not a9,b9 // c9,y9
proof
assume not thesis;
then a,b // c,y by Th36;
then c,y _|_ c,y by A9,A10,Def8;
hence contradiction by A11,Def8;
end;
then consider x9 being Element of the AffinStruct of POS such that
A12: LIN a9,b9,x9 and
A13: LIN c9,y9,x9 by AFF_1:60;
reconsider x=x9 as Element of POS;
c9,y9 // c9,x9 by A13,AFF_1:def 1;
then
A14: c,y // c,x by Th36;
c,y _|_ a,b by A10,Def8;
then a,b _|_ c,x by A11,A14,Def8;
then
A15: a,b _|_ x,c by Def8;
a9,b9 // a9,x9 by A12,AFF_1:def 1;
then a,b // a,x by Th36;
hence thesis by A15;
end;
the AffinStruct of POS = AffinStruct(#the carrier of POS, the CONGR of POS#)
& for a,b,c being Element of POS ex x being Element of POS st a,b _|_ c,x
& c <>x by Def8;
hence thesis by A8,A7,Def7;
end;
registration
cluster OrtAfPl-like -> OrtAfSp-like for non empty ParOrtStr;
coherence by Th37;
end;
theorem
for POS being OrtAfSp st the AffinStruct of POS is AffinPlane
holds POS is OrtAfPl
proof
let POS be OrtAfSp such that
A1: the AffinStruct of POS is AffinPlane;
A2: now
let a,b,c,d,p,q,r,s be Element of POS;
thus (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b
_|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b)
by Def7;
thus a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b
proof
reconsider a9=a,b9=b,p9=p,q9=q,r9=r,s9=s as
Element of the AffinStruct of POS;
assume that
A3: a,b _|_ p,q and
A4: a,b _|_ r,s;
A5: p,q _|_ a,b by A3,Def7;
A6: r,s _|_ a,b by A4,Def7;
assume
A7: not thesis;
then
A8: not p9,q9 // r9,s9 by Th36;
then
A9: p9<>q9 by AFF_1:3;
consider x9 being Element of the AffinStruct of POS such that
A10: LIN p9,q9,x9 and
A11: LIN r9,s9,x9 by A1,A8,AFF_1:60;
reconsider x=x9 as Element of POS;
A12: r9<>s9 by A8,AFF_1:3;
LIN s9,r9,x9 by A11,AFF_1:6;
then s9,r9 // s9,x9 by AFF_1:def 1;
then
A13: r9,s9 // x9,s9 by AFF_1:4;
then r,s // x,s by Th36;
then a,b _|_ x,s by A12,A6,Def7;
then
A14: x,s _|_ a,b by Def7;
LIN q9,p9,x9 by A10,AFF_1:6;
then q9,p9 // q9,x9 by AFF_1:def 1;
then p9,q9 // x9,q9 by AFF_1:4;
then p,q // x,q by Th36;
then
A15: a,b _|_ x,q by A9,A5,Def7;
A16: now
consider y9 being Element of the AffinStruct of POS such that
A17: a9,b9 // q9,y9 & q9<>y9 by DIRAF:40;
assume that
A18: x<>q and
A19: x<>s;
not q9,y9 // x9,s9
proof
assume not thesis;
then q9,y9 // r9,s9 by A13,A19,AFF_1:5;
then r9,s9 // a9,b9 by A17,AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12,A6,Def7;
hence contradiction by A7,Def7;
end;
then consider z9 being Element of the AffinStruct of POS such that
A20: LIN q9,y9,z9 and
A21: LIN x9,s9,z9 by A1,AFF_1:60;
reconsider z=z9 as Element of POS;
q9,y9 // q9,z9 by A20,AFF_1:def 1;
then a9,b9 // q9,z9 by A17,AFF_1:5;
then
A22: a,b // q,z by Th36;
A23: x9,s9 // x9,z9 by A21,AFF_1:def 1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14,A19,Def7;
then a,b _|_ q,z by A15,Def7;
then q,z _|_ q,z by A7,A22,Def7;
then x9,s9 // x9,q9 by A23,Def7;
then
A24: LIN x9,s9,q9 by AFF_1:def 1;
LIN x9,s9,x9 & LIN x9,q9,p9 by A10,AFF_1:6,7;
then LIN x9,s9,p9 by A18,A24,AFF_1:11;
then x9,s9 // p9,q9 by A24,AFF_1:10;
then p9,q9 // r9,s9 by A13,A19,AFF_1:5;
hence contradiction by A7,Th36;
end;
r9,s9 // r9,x9 by A11,AFF_1:def 1;
then
A25: r9,s9 // x9,r9 by AFF_1:4;
then r,s // x,r by Th36;
then a,b _|_ x,r by A12,A6,Def7;
then
A26: x,r _|_ a,b by Def7;
A27: now
consider y9 being Element of the AffinStruct of POS such that
A28: a9,b9 // q9,y9 & q9<>y9 by DIRAF:40;
assume that
A29: x<>q and
A30: x<>r;
not q9,y9 // x9,r9
proof
assume not thesis;
then q9,y9 // r9,s9 by A25,A30,AFF_1:5;
then r9,s9 // a9,b9 by A28,AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12,A6,Def7;
hence contradiction by A7,Def7;
end;
then consider z9 being Element of the AffinStruct of POS such that
A31: LIN q9,y9,z9 and
A32: LIN x9,r9,z9 by A1,AFF_1:60;
reconsider z=z9 as Element of POS;
q9,y9 // q9,z9 by A31,AFF_1:def 1;
then a9,b9 // q9,z9 by A28,AFF_1:5;
then
A33: a,b // q,z by Th36;
A34: x9,r9 // x9,z9 by A32,AFF_1:def 1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26,A30,Def7;
then a,b _|_ q,z by A15,Def7;
then q,z _|_ q,z by A7,A33,Def7;
then x9,r9 // x9,q9 by A34,Def7;
then
A35: LIN x9,r9,q9 by AFF_1:def 1;
LIN x9,r9,x9 & LIN x9,q9,p9 by A10,AFF_1:6,7;
then LIN x9,r9,p9 by A29,A35,AFF_1:11;
then x9,r9 // p9,q9 by A35,AFF_1:10;
then p9,q9 // r9,s9 by A25,A30,AFF_1:5;
hence contradiction by A7,Th36;
end;
p9,q9 // p9,x9 by A10,AFF_1:def 1;
then p9,q9 // x9,p9 by AFF_1:4;
then p,q // x,p by Th36;
then
A36: a,b _|_ x,p by A9,A5,Def7;
A37: now
consider y9 being Element of the AffinStruct of POS such that
A38: a9,b9 // p9,y9 & p9<>y9 by DIRAF:40;
assume that
A39: x<>p and
A40: x<>s;
not p9,y9 // x9,s9
proof
assume not thesis;
then p9,y9 // r9,s9 by A13,A40,AFF_1:5;
then r9,s9 // a9,b9 by A38,AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12,A6,Def7;
hence contradiction by A7,Def7;
end;
then consider z9 being Element of the AffinStruct of POS such that
A41: LIN p9,y9,z9 and
A42: LIN x9,s9,z9 by A1,AFF_1:60;
reconsider z=z9 as Element of POS;
p9,y9 // p9,z9 by A41,AFF_1:def 1;
then a9,b9 // p9,z9 by A38,AFF_1:5;
then
A43: a,b // p,z by Th36;
A44: x9,s9 // x9,z9 by A42,AFF_1:def 1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14,A40,Def7;
then a,b _|_ p,z by A36,Def7;
then p,z _|_ p,z by A7,A43,Def7;
then x9,s9 // x9,p9 by A44,Def7;
then
A45: LIN x9,s9,p9 by AFF_1:def 1;
LIN x9,s9,x9 & LIN x9,p9,q9 by A10,AFF_1:6,7;
then LIN x9,s9,q9 by A39,A45,AFF_1:11;
then x9,s9 // p9,q9 by A45,AFF_1:10;
then p9,q9 // r9,s9 by A13,A40,AFF_1:5;
hence contradiction by A7,Th36;
end;
now
consider y9 being Element of the AffinStruct of POS such that
A46: a9,b9 // p9,y9 & p9<>y9 by DIRAF:40;
assume that
A47: x<>p and
A48: x<>r;
not p9,y9 // x9,r9
proof
assume not thesis;
then p9,y9 // r9,s9 by A25,A48,AFF_1:5;
then r9,s9 // a9,b9 by A46,AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12,A6,Def7;
hence contradiction by A7,Def7;
end;
then consider z9 being Element of the AffinStruct of POS such that
A49: LIN p9,y9,z9 and
A50: LIN x9,r9,z9 by A1,AFF_1:60;
reconsider z=z9 as Element of POS;
p9,y9 // p9,z9 by A49,AFF_1:def 1;
then a9,b9 // p9,z9 by A46,AFF_1:5;
then
A51: a,b // p,z by Th36;
A52: x9,r9 // x9,z9 by A50,AFF_1:def 1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26,A48,Def7;
then a,b _|_ p,z by A36,Def7;
then p,z _|_ p,z by A7,A51,Def7;
then x9,r9 // x9,p9 by A52,Def7;
then
A53: LIN x9,r9,p9 by AFF_1:def 1;
LIN x9,r9,x9 & LIN x9,p9,q9 by A10,AFF_1:6,7;
then LIN x9,r9,q9 by A47,A53,AFF_1:11;
then x9,r9 // p9,q9 by A53,AFF_1:10;
then p9,q9 // r9,s9 by A25,A48,AFF_1:5;
hence contradiction by A7,Th36;
end;
hence contradiction by A8,A37,A27,A16,AFF_1:3;
end;
end;
for a,b,c being Element of POS ex x being Element of POS st a,b _|_ c,x
& c <>x by Def7;
hence thesis by A1,A2,Def8;
end;
theorem
for POS being non empty ParOrtStr holds POS is OrtAfPl-like iff (ex a,
b being Element of POS st a<>b) & for a,b,c,d,p,q,r,s being Element of POS
holds a,b // b,a & a,b // c,c & (a,b // p,q & a,b // r,s implies p,q // r,s or
a=b) & (a,b // a,c implies b,a // b,c) & (ex x being Element of POS st a,b // c
,x & a,c // b,x) & (ex x,y,z being Element of POS st not x,y // x,z ) & (ex x
being Element of POS st a,b // c,x & c <>x) & (a,b // b,d & b<>a implies ex x
being Element of POS st c,b // b,x & c,a // d,x) & (a,b _|_ a,b implies a=b) &
a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q &
a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p,q
// r,s or a=b) & (ex x being Element of POS st a,b _|_ c,x & c <>x) & (not a,b
// c,d implies ex x being Element of POS st a,b // a,x & c,d // c,x )
proof
let POS be non empty ParOrtStr;
set P = the AffinStruct of POS;
hereby
assume
A1: POS is OrtAfPl-like;
then P is AffinPlane;
hence ex x,y being Element of POS st x<>y by DIRAF:46;
let a,b,c,d,p,q,r,s be Element of POS;
reconsider a9=a,b9=b,c9=c,d9=d,p9=p,q9=q,r9=r,s9=s as Element of P;
consider x9 being Element of P such that
A2: a9,b9 // c9,x9 & a9,c9 // b9,x9 by A1,DIRAF:46;
a9,b9 // b9,a9 & a9,b9 // c9,c9 by A1,DIRAF:46;
hence a,b // b,a & a,b // c,c by Th36;
hereby
assume a,b // p,q & a,b // r,s;
then a9,b9 // p9,q9 & a9,b9 // r9,s9 by Th36;
then p9,q9 // r9,s9 or a9=b9 by A1,DIRAF:46;
hence p,q // r,s or a=b by Th36;
end;
hereby
assume a,b // a,c;
then a9,b9 // a9,c9 by Th36;
then b9,a9 // b9,c9 by A1,DIRAF:46;
hence b,a // b,c by Th36;
end;
reconsider x=x9 as Element of POS;
consider x9,y9,z9 being Element of P such that
A3: not x9,y9 // x9,z9 by A1,DIRAF:46;
a,b // c,x & a,c // b,x by A2,Th36;
hence ex x being Element of POS st a,b // c,x & a,c // b,x;
reconsider x=x9,y=y9,z=z9 as Element of POS;
consider x9 being Element of P such that
A4: a9,b9 // c9,x9 and
A5: c9<>x9 by A1,DIRAF:46;
not x,y // x,z by A3,Th36;
hence ex x,y,z being Element of POS st not x,y // x,z;
reconsider x=x9 as Element of POS;
a,b // c,x by A4,Th36;
hence ex x being Element of POS st a,b // c,x & c <>x by A5;
hereby
assume that
A6: a,b // b,d and
A7: b<>a;
a9,b9 // b9,d9 by A6,Th36;
then consider x9 being Element of P such that
A8: c9,b9 // b9,x9 & c9,a9 // d9,x9 by A1,A7,DIRAF:46;
reconsider x=x9 as Element of POS;
c,b // b,x & c,a // d,x by A8,Th36;
hence ex x being Element of POS st c,b // b,x & c,a // d,x;
end;
thus (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b
_|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b)
& (a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b) & ex x being Element of
POS st a,b _|_ c,x & c <>x by A1;
assume not a,b // c,d;
then not a9,b9 // c9,d9 by Th36;
then consider x9 being Element of P such that
A9: a9,b9 // a9,x9 & c9,d9 // c9,x9 by A1,DIRAF:46;
reconsider x=x9 as Element of POS;
a,b // a,x & c,d // c,x by A9,Th36;
hence ex x being Element of POS st a,b // a,x & c,d // c,x;
end;
given a,b being Element of POS such that
A10: a<>b;
assume
A11: for a,b,c,d,p,q,r,s being Element of POS holds a,b // b,a & a,b //
c,c & (a,b // p,q & a,b // r,s implies p,q // r,s or a=b) & (a,b // a,c implies
b,a // b,c) & (ex x being Element of POS st a,b // c,x & a,c // b,x) & (ex x,y,
z being Element of POS st not x,y // x,z ) & (ex x being Element of POS st a,b
// c,x & c <>x) & (a,b // b,d & b<>a implies ex x being Element of POS st c,b
// b,x & c,a // d,x) & (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d
implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_
r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b) & (ex x
being Element of POS st a,b _|_ c,x & c <>x) & (not a,b // c,d implies ex x
being Element of POS st a,b // a,x & c,d // c,x );
A12: now
let x,y,z be Element of P;
reconsider x9=x,y9=y,z9=z as Element of POS;
consider t9 being Element of POS such that
A13: x9,z9 // y9,t9 and
A14: y9<>t9 by A11;
reconsider t=t9 as Element of P;
x,z // y,t by A13,Th36;
hence ex t being Element of P st x,z // y,t & y<>t by A14;
end;
A15: now
let x,y,z,t,u,w be Element of P;
reconsider a=x,b=y,c =z,d=t,e=u,f=w as Element of POS;
a,b // b,a & a,b // c,c by A11;
hence x,y // y,x & x,y // z,z by Th36;
thus x<>y & x,y // z,t & x,y // u,w implies z,t // u,w
proof
assume that
A16: x<>y and
A17: x,y // z,t & x,y // u,w;
a,b // c,d & a,b // e,f by A17,Th36;
then c,d // e,f by A11,A16;
hence thesis by Th36;
end;
thus x,y // x,z implies y,x // y,z
proof
assume x,y // x,z;
then a,b // a, c by Th36;
then b,a // b,c by A11;
hence thesis by Th36;
end;
end;
A18: now
let x,y,z,t be Element of P such that
A19: not x,y // z,t;
reconsider x9=x,y9=y,z9=z,t9=t as Element of POS;
not x9,y9 // z9,t9 by A19,Th36;
then consider u9 being Element of POS such that
A20: x9,y9 // x9,u9 & z9,t9 // z9,u9 by A11;
reconsider u=u9 as Element of P;
x,y // x,u & z,t // z,u by A20,Th36;
hence ex u being Element of P st x,y // x,u & z,t // z,u;
end;
A21: now
let x,y,z,t be Element of P such that
A22: z,x // x,t and
A23: x<>z;
reconsider x9=x,y9=y,z9=z,t9=t as Element of POS;
z9,x9 // x9,t9 by A22,Th36;
then consider u9 being Element of POS such that
A24: y9,x9 // x9,u9 & y9,z9 // t9,u9 by A11,A23;
reconsider u=u9 as Element of P;
y,x // x,u & y,z // t,u by A24,Th36;
hence ex u being Element of P st y,x // x,u & y,z // t,u;
end;
A25: now
let x,y,z be Element of P;
reconsider x9=x,y9=y,z9=z as Element of POS;
consider t9 being Element of POS such that
A26: x9,y9 // z9,t9 & x9,z9 // y9,t9 by A11;
reconsider t=t9 as Element of P;
x,y // z,t & x,z // y,t by A26,Th36;
hence ex t being Element of P st x,y // z,t & x,z // y,t;
end;
ex x,y,z being Element of P st not x,y // x,z
proof
consider x,y,z being Element of POS such that
A27: not x,y // x,z by A11;
reconsider x9=x,y9=y,z9=z as Element of P;
not x9,y9 // x9,z9 by A27,Th36;
hence thesis;
end;
hence
AffinStruct(#the carrier of POS,the CONGR of POS#) is AffinPlane by A10,A15
,A12,A25,A21,A18,DIRAF:46;
thus for a,b,c,d,p,q,r,s be Element of POS holds (a,b _|_ a,b implies a=b) &
a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q &
a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p,q
// r,s or a=b) by A11;
thus thesis by A11;
end;
reserve x,a,b,c,d,p,q,y for Element of POS;
definition
let POS;
let a,b,c;
pred LIN a,b,c means
a,b // a,c;
end;
definition
let POS,a,b;
func Line(a,b) -> Subset of POS means
:Def10:
for x being Element of POS holds x in it iff LIN a,b,x;
existence
proof
defpred P[set] means for y st y = $1 holds LIN a,b,y;
consider X being Subset of POS such that
A1: for x being set holds x in X iff x in the carrier of POS & P[x]
from SUBSET_1:sch 1;
take X;
let x be Element of POS;
thus x in X implies LIN a,b,x by A1;
assume LIN a,b,x;
then for y st y = x holds LIN a,b,y;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of POS such that
A2: for x holds x in X1 iff LIN a,b,x and
A3: for x holds x in X2 iff LIN a,b,x;
for x being object holds x in X1 iff x in X2 by A2,A3;
hence thesis by TARSKI:2;
end;
end;
reserve A,K,M for Subset of POS;
definition
let POS;
let A;
attr A is being_line means
ex a,b st a<>b & A=Line(a,b);
end;
theorem Th40:
for POS being OrtAfSp for a,b,c being Element of POS, a9,b9,c9
being Element of the AffinStruct of POS st a=a9& b=b9 & c = c9
holds (LIN a,b,c iff LIN a9,b9,c9)
proof
let POS be OrtAfSp;
let a,b,c be Element of POS, a9,b9,c9 be Element of the AffinStruct of POS
such that
A1: a=a9 & b=b9 & c = c9;
hereby
assume LIN a,b,c;
then a,b // a,c;
then a9,b9 // a9,c9 by A1,Th36;
hence LIN a9,b9,c9 by AFF_1:def 1;
end;
assume LIN a9,b9,c9;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b // a,c by A1,Th36;
hence thesis;
end;
theorem Th41:
for POS being OrtAfSp for a,b being Element of POS, a9,b9 being
Element of the AffinStruct of POS st a=a9 & b=b9
holds Line(a,b) = Line(a9,b9)
proof
let POS be OrtAfSp;
let a,b be Element of POS, a9,b9 be Element of the AffinStruct of POS
such that
A1: a=a9 & b=b9;
set X = Line(a,b), Y = Line(a9,b9);
now
let x1 be object;
A2: now
assume
A3: x1 in Y;
then reconsider x9=x1 as Element of the AffinStruct of POS;
reconsider x=x9 as Element of POS;
LIN a9,b9,x9 by A3,AFF_1:def 2;
then LIN a,b,x by A1,Th40;
hence x1 in X by Def10;
end;
now
assume
A4: x1 in X;
then reconsider x=x1 as Element of POS;
reconsider x9=x as Element of the AffinStruct of POS;
LIN a,b,x by A4,Def10;
then LIN a9,b9,x9 by A1,Th40;
hence x1 in Y by AFF_1:def 2;
end;
hence x1 in X iff x1 in Y by A2;
end;
hence thesis by TARSKI:2;
end;
theorem
for X being set holds
X is Subset of POS iff X is Subset of the AffinStruct of POS;
theorem Th43:
for POS being OrtAfSp for X being Subset of POS, Y being Subset
of the AffinStruct of POS st X=Y holds X is being_line iff Y is being_line
proof
let POS be OrtAfSp;
let X be Subset of the carrier of POS, Y be Subset of the AffinStruct of POS
such that
A1: X=Y;
hereby
assume X is being_line;
then consider a,b being Element of POS such that
A2: a<>b and
A3: X = Line(a,b);
reconsider a9=a,b9=b as Element of the AffinStruct of POS;
Y = Line(a9,b9) by A1,A3,Th41;
hence Y is being_line by A2,AFF_1:def 3;
end;
assume Y is being_line;
then consider a9,b9 being Element of the AffinStruct of POS such that
A4: a9<>b9 and
A5: Y = Line(a9,b9) by AFF_1:def 3;
reconsider a=a9,b=b9 as Element of POS;
X = Line(a,b) by A1,A5,Th41;
hence thesis by A4;
end;
definition
let POS;
let a,b,K;
pred a,b _|_ K means
ex p,q st p<>q & K = Line(p,q) & a,b _|_ p,q;
end;
definition
let POS;
let K,M;
pred K _|_ M means
:Def13:
ex p,q st p<>q & K = Line(p,q) & p,q _|_ M;
end;
definition
let POS;
let K,M;
pred K // M means
ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M = Line(c,d) & a,b // c,d;
end;
theorem Th44:
(a,b _|_ K implies K is being_line) &
(K _|_ M implies K is being_line & M is being_line )
proof
for a,b,K st a,b _|_ K holds K is being_line;
then K _|_ M implies K is being_line & M is being_line;
hence thesis;
end;
theorem Th45:
K _|_ M iff ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M =
Line(c,d) & a,b _|_ c,d
proof
hereby
assume K _|_ M;
then consider a,b such that
A1: a<>b & K = Line(a,b) and
A2: a,b _|_ M;
ex c,d st c <>d & M = Line(c,d) & a,b _|_ c,d by A2;
hence ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M = Line(c,d) & a,b _|_
c,d by A1;
end;
given a,b,c,d such that
A3: a<>b and
A4: c <>d and
A5: K = Line(a,b) and
A6: M = Line(c,d) & a,b _|_ c,d;
a,b _|_ M by A4,A6;
hence thesis by A3,A5;
end;
theorem Th46:
for POS being OrtAfSp for M,N being Subset of POS, M9,N9 being
Subset of the AffinStruct of POS st M = M9 & N = N9
holds M // N iff M9 // N9
proof
let POS be OrtAfSp;
let M,N be Subset of POS, M9,N9 be Subset of the AffinStruct of POS such that
A1: M = M9 & N = N9;
hereby
assume M // N;
then consider a,b,c,d being Element of POS such that
A2: a<>b & c <>d and
A3: M = Line(a,b) & N = Line(c,d) and
A4: a,b // c,d;
reconsider a9=a,b9=b,c9=c,d9=d as Element of the AffinStruct of POS;
A5: a9,b9 // c9,d9 by A4,Th36;
M9=Line(a9,b9) & N9=Line(c9,d9) by A1,A3,Th41;
hence M9 // N9 by A2,A5,AFF_1:37;
end;
assume M9 // N9;
then consider a9,b9,c9,d9 being Element of the AffinStruct of POS such that
A6: a9<>b9 & c9<>d9 and
A7: a9,b9 // c9,d9 and
A8: M9 = Line(a9,b9) & N9 = Line(c9,d9) by AFF_1:37;
reconsider a=a9,b=b9,c =c9,d=d9 as Element of POS;
A9: a,b // c,d by A7,Th36;
M=Line(a,b) & N=Line(c,d) by A1,A8,Th41;
hence thesis by A6,A9;
end;
reserve POS for OrtAfSp;
reserve A,K,M,N for Subset of POS;
reserve a,b,c,d,p,q,r,s for Element of POS;
theorem
K is being_line implies a,a _|_ K
proof
assume K is being_line;
then consider p,q such that
A1: p<>q & K = Line(p,q);
p,q _|_ a,a by Def7;
then a,a _|_ p,q by Def7;
hence thesis by A1;
end;
theorem
a,b _|_ K & (a,b // c,d or c,d // a,b) & a<>b implies c,d _|_ K
proof
assume that
A1: a,b _|_ K and
A2: a,b // c,d or c,d // a,b and
A3: a<>b;
reconsider a9=a,b9=b,c9=c,d9=d as Element of the AffinStruct of POS;
consider p,q such that
A4: p<>q & K = Line(p,q) and
A5: a,b _|_ p,q by A1;
a9,b9 // c9,d9 or c9,d9 // a9,b9 by A2,Th36;
then a9,b9 // c9,d9 by AFF_1:4;
then a,b // c,d by Th36;
then p,q _|_ c,d by A3,A5,Def7;
then c,d _|_ p,q by Def7;
hence thesis by A4;
end;
theorem
a,b _|_ K implies b,a _|_ K
proof
assume a,b _|_ K;
then consider p,q such that
A1: p<>q & K = Line(p,q) and
A2: a,b _|_ p,q;
p,q _|_ a,b by A2,Def7;
then p,q _|_ b,a by Def7;
then b,a _|_ p,q by Def7;
hence thesis by A1;
end;
definition
let POS;
let K,M be Subset of POS;
redefine pred K // M; :: redefines // (ANALMETR, definition)
symmetry
proof
let K,M be Subset of POS;
assume K // M;
then consider a,b,c,d such that
A1: a<>b & c <>d & K = Line(a,b) & M = Line(c,d) and
A2: a,b // c,d;
reconsider a9=a,b9=b,c9=c,d9=d as Element of the AffinStruct of POS;
a9,b9 // c9,d9 by A2,Th36;
then c9,d9 // a9,b9 by AFF_1:4;
then c,d // a,b by Th36;
hence thesis by A1;
end;
end;
theorem Th50:
r,s _|_ K & K // M implies r,s _|_ M
proof
assume that
A1: r,s _|_ K and
A2: K // M;
consider p,q such that
A3: p<>q and
A4: K = Line(p,q) and
A5: r,s _|_ p,q by A1;
consider a,b,c,d such that
A6: a<>b and
A7: c <>d and
A8: K = Line(a,b) and
A9: M = Line(c,d) and
A10: a,b // c,d by A2;
reconsider p9=p,q9=q,a9=a,b9=b,c9=c,d9=d
as Element of the AffinStruct of POS;
A11: K = Line(a9,b9) by A8,Th41;
A12: K = Line(p9,q9) by A4,Th41;
then q9 in K by AFF_1:15;
then
A13: LIN a9,b9,q9 by A11,AFF_1:def 2;
p9 in K by A12,AFF_1:15;
then LIN a9,b9,p9 by A11,AFF_1:def 2;
then
A14: a9,b9 // p9,q9 by A13,AFF_1:10;
A15: p,q _|_ r,s by A5,Def7;
a9,b9 // c9,d9 by A10,Th36;
then p9,q9 // c9,d9 by A6,A14,AFF_1:5;
then p,q // c,d by Th36;
then r,s _|_ c,d by A3,A15,Def7;
hence thesis by A7,A9;
end;
theorem Th51:
a in K & b in K & a,b _|_ K implies a=b
proof
assume that
A1: a in K and
A2: b in K and
A3: a,b _|_ K;
consider p,q such that
A4: p<>q and
A5: K = Line(p,q) and
A6: a,b _|_ p,q by A3;
reconsider a9=a,b9=b,p9=p,q9=q as Element of the AffinStruct of POS;
set K9 = Line(p9,q9);
b9 in K9 by A2,A5,Th41;
then
A7: LIN p9,q9,b9 by AFF_1:def 2;
a9 in K9 by A1,A5,Th41;
then LIN p9,q9,a9 by AFF_1:def 2;
then p9,q9 // a9,b9 by A7,AFF_1:10;
then
A8: p,q // a,b by Th36;
p,q _|_ a,b by A6,Def7;
then a,b _|_ a,b by A4,A8,Def7;
hence thesis by Def7;
end;
definition
let POS;
let K,M be Subset of POS;
redefine pred K _|_ M; :: redefines _|_ (ANALMETR, definition)
irreflexivity
proof
let K be Subset of POS;
assume not thesis;
then consider a,b such that
A1: a<>b and
A2: K = Line(a,b) and
A3: a,b _|_ K;
reconsider a9=a,b9=b as Element of the AffinStruct of POS;
K = Line(a9,b9) by A2,Th41;
then a in K & b in K by AFF_1:15;
hence contradiction by A1,A3,Th51;
end;
symmetry
proof
let K,M be Subset of POS;
assume K _|_ M;
then consider a,b,c,d such that
A4: a<>b & c <>d & K = Line(a,b) & M = Line(c,d) and
A5: a,b _|_ c,d by Th45;
c,d _|_ a,b by A5,Def7;
hence thesis by A4,Th45;
end;
end;
theorem Th52:
K _|_ M & K // N implies N _|_ M
proof
assume that
A1: K _|_ M and
A2: K // N;
consider r,s such that
A3: r<>s & M = Line(r,s) and
A4: r,s _|_ K by A1,Def13;
r,s _|_ N by A2,A4,Th50;
hence thesis by A3,Def13;
end;
theorem
a in K & b in K & c,d _|_ K implies c,d _|_ a,b & a,b _|_ c,d
proof
assume that
A1: a in K and
A2: b in K and
A3: c,d _|_ K;
consider p,q such that
A4: p<>q and
A5: K = Line(p,q) and
A6: c,d _|_ p,q by A3;
reconsider a9=a,b9=b, p9=p,q9=q as Element of the AffinStruct of POS;
LIN p,q, b by A2,A5,Def10;
then
A7: LIN p9,q9,b9 by Th40;
LIN p,q,a by A1,A5,Def10;
then LIN p9,q9,a9 by Th40;
then p9,q9 // a9, b9 by A7,AFF_1:10;
then
A8: p,q // a,b by Th36;
p,q _|_ c,d by A6,Def7;
hence c,d _|_ a,b by A4,A8,Def7;
hence thesis by Def7;
end;
theorem Th54:
a in K & b in K & a<>b & K is being_line implies K =Line(a,b)
proof
assume that
A1: a in K & b in K & a<>b and
A2: K is being_line;
reconsider a9=a,b9=b as Element of the AffinStruct of POS;
reconsider K9=K as Subset of the AffinStruct of POS;
K9 is being_line by A2,Th43;
then K9 = Line(a9,b9) by A1,AFF_1:57;
hence thesis by Th41;
end;
theorem
a in K & b in K & a<>b & K is being_line & (a,b _|_ c,d or c,d _|_ a,b
) implies c,d _|_ K
proof
assume that
A1: a in K & b in K and
A2: a<>b and
A3: K is being_line &( a,b _|_ c,d or c,d _|_ a,b);
c,d _|_ a,b & K = Line(a,b) by A1,A2,A3,Def7,Th54;
hence thesis by A2;
end;
theorem Th56:
a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d
proof
assume that
A1: a in M and
A2: b in M and
A3: c in N and
A4: d in N and
A5: M _|_ N;
consider p1,q1,p2,q2 being Element of POS such that
A6: p1<>q1 and
A7: p2<>q2 and
A8: M = Line(p1,q1) and
A9: N = Line(p2,q2) and
A10: p1,q1 _|_ p2,q2 by A5,Th45;
reconsider a9=a,b9=b,c9=c,d9=d,p19=p1,q19=q1,p29=p2,q29=q2
as Element of the AffinStruct of POS;
LIN p1,q1,b by A2,A8,Def10;
then
A11: LIN p19,q19,b9 by Th40;
LIN p1,q1,a by A1,A8,Def10;
then LIN p19,q19,a9 by Th40;
then p19,q19 // a9,b9 by A11,AFF_1:10;
then p1,q1 // a,b by Th36;
then
A12: p2,q2 _|_ a,b by A6,A10,Def7;
LIN p2,q2,d by A4,A9,Def10;
then
A13: LIN p29,q29,d9 by Th40;
LIN p2,q2,c by A3,A9,Def10;
then LIN p29,q29,c9 by Th40;
then p29,q29 // c9,d9 by A13,AFF_1:10;
then p2,q2 // c,d by Th36;
hence thesis by A7,A12,Def7;
end;
theorem
p in M & p in N & a in M & b in N & a<>b & a in K & b in K & A _|_ M &
A _|_ N & K is being_line implies A _|_ K
proof
assume that
A1: p in M & p in N & a in M & b in N and
A2: a<>b and
A3: a in K & b in K and
A4: A _|_ M and
A5: A _|_ N and
A6: K is being_line;
A is being_line by A4;
then consider q,r such that
A7: q<>r and
A8: A = Line(q,r);
reconsider q9=q,r9=r as Element of the AffinStruct of POS;
Line(q,r) = Line(q9,r9) by Th41;
then q in A & r in A by A8,AFF_1:15;
then q,r _|_ p,a & q,r _|_ p,b by A1,A4,A5,Th56;
then
A9: q,r _|_ a,b by Def7;
K = Line(a,b) by A2,A3,A6,Th54;
hence thesis by A2,A7,A8,A9,Th45;
end;
theorem Th58:
b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c
proof
reconsider a9=a,b9=b,c9=c as Element of the AffinStruct of POS;
thus b,c _|_ a,a by Def7;
hence a,a _|_ b,c by Def7;
b9,c9 // a9,a9 & a9,a9 // b9,c9 by AFF_1:3;
hence thesis by Th36;
end;
theorem Th59:
a,b // c,d implies a,b // d,c & b,a // c,d & b,a // d,c & c,d //
a,b & c,d // b,a & d,c // a,b & d,c // b,a
proof
reconsider a9=a,b9=b,c9= c,d9=d as Element of the AffinStruct of POS;
assume a,b // c,d;
then
A1: a9,b9 // c9,d9 by Th36;
then
A2: b9,a9 // d9,c9 & c9,d9 // a9,b9 by AFF_1:4;
A3: d9,c9 // b9,a9 by A1,AFF_1:4;
A4: c9,d9 // b9,a9 & d9,c9 // a9,b9 by A1,AFF_1:4;
a9,b9 // d9,c9 & b9,a9 // c9,d9 by A1,AFF_1:4;
hence thesis by A2,A4,A3,Th36;
end;
theorem
p<>q & ( p,q // a,b & p,q // c,d or p,q // a,b & c,d // p,q or a,b //
p,q & c,d // p,q or a,b // p,q & p,q // c,d ) implies a,b // c,d
proof
assume that
A1: p<>q and
A2: p,q // a,b & p,q // c,d or p,q // a,b & c,d // p,q or a,b // p,q & c
,d // p,q or a,b // p,q & p,q // c,d;
reconsider p9=p,q9=q,a9=a, b9=b,c9= c,d9=d
as Element of the AffinStruct of POS;
p9,q9 // a9,b9 & p9,q9 // c9,d9 or p9,q9 // a9,b9 & c9,d9 // p9,q9 or a9
,b9 // p9,q9 & c9,d9 // p9,q9 or a9,b9 // p9,q9 & p9,q9 // c9,d9 by A2,Th36;
then a9,b9 // c9,d9 by A1,AFF_1:5;
hence thesis by Th36;
end;
theorem Th61:
a,b _|_ c,d implies a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,
d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a
proof
assume
A1: a,b _|_ c,d;
then a,b _|_ d,c by Def7;
then
A2: d,c _|_ a,b by Def7;
then d,c _|_ b,a by Def7;
then b,a _|_ d,c by Def7;
then b,a _|_ c,d by Def7;
hence thesis by A1,A2,Def7;
end;
theorem Th62:
p<>q & ( p,q // a,b & p,q _|_ c,d or p,q // c,d & p,q _|_ a,b or
p,q // a,b & c,d _|_ p,q or p,q // c,d & a,b _|_ p,q or a,b // p,q & c,d _|_ p,
q or c,d // p,q & a,b _|_ p,q or a,b // p,q & p,q _|_ c,d or c,d // p,q & p,q
_|_ a,b ) implies a,b _|_ c,d
proof
assume that
A1: p<>q and
A2: p,q // a,b & p,q _|_ c,d or p,q // c,d & p,q _|_ a,b or p,q // a,b &
c,d _|_ p,q or p,q // c,d & a,b _|_ p,q or a,b // p,q & c,d _|_ p,q or c,d // p
,q & a,b _|_ p,q or a,b // p,q & p,q _|_ c,d or c,d // p,q & p,q _|_ a,b;
A3: now
assume p,q // a,b & p,q _|_ c,d or p,q // a,b & c,d _|_ p,q or a,b // p,q
& c,d _|_ p,q or a,b // p,q & p,q _|_ c,d;
then p,q // a,b & p,q _|_ c,d by Th59,Th61;
then c,d _|_ a,b by A1,Def7;
hence thesis by Th61;
end;
now
assume p,q // c,d & p,q _|_ a,b or p,q // c,d & a,b _|_ p,q or c,d // p,
q & a,b _|_ p,q or c,d // p,q & p,q _|_ a,b;
then p,q // c,d & p,q _|_ a,b by Th59,Th61;
hence thesis by A1,Def7;
end;
hence thesis by A2,A3;
end;
reserve POS for OrtAfPl;
reserve K,M,N for Subset of POS;
reserve x,a,b,c,d,p,q for Element of POS;
theorem Th63:
p<>q & ( p,q _|_ a,b & p,q _|_ c,d or p,q _|_ a,b & c,d _|_ p,q
or a,b _|_ p,q & c,d _|_ p,q or a,b _|_ p,q & p,q _|_ c,d ) implies a,b // c,d
proof
assume that
A1: p<>q and
A2: p,q _|_ a,b & p,q _|_ c,d or p,q _|_ a,b & c,d _|_ p,q or a,b _|_ p,
q & c,d _|_ p,q or a,b _|_ p,q & p,q _|_ c,d;
p,q _|_ a,b & p,q _|_ c,d by A2,Th61;
hence thesis by A1,Def8;
end;
theorem
a in M & b in M & a<>b & M is being_line & c in N & d in N & c <>d & N
is being_line & a,b // c,d implies M // N
proof
assume that
A1: a in M & b in M and
A2: a<>b and
A3: M is being_line & c in N & d in N and
A4: c <>d and
A5: N is being_line and
A6: a,b // c,d;
M = Line(a,b) & N = Line(c,d) by A1,A2,A3,A4,A5,Th54;
hence thesis by A2,A4,A6;
end;
theorem
M _|_ K & N _|_ K implies M // N
proof
assume that
A1: M _|_ K and
A2: N _|_ K;
consider p1,q1,a,b being Element of POS such that
A3: p1<>q1 and
A4: a<>b and
A5: K = Line(p1,q1) and
A6: M = Line(a,b) and
A7: p1,q1 _|_ a,b by A1,Th45;
consider p2,q2,c,d being Element of POS such that
A8: p2<>q2 and
A9: c <>d and
A10: K = Line(p2,q2) and
A11: N = Line(c,d) and
A12: p2,q2 _|_ c,d by A2,Th45;
reconsider p19=p1,p29=p2,q19=q1,q29=q2 as Element of the AffinStruct of POS;
A13: Line(p19,q19) = Line(p2,q2) by A5,A10,Th41
.= Line(p29,q29) by Th41;
then q29 in Line(p19,q19) by AFF_1:15;
then
A14: LIN p19,q19,q29 by AFF_1:def 2;
p29 in Line(p19,q19) by A13,AFF_1:15;
then LIN p19,q19,p29 by AFF_1:def 2;
then p19,q19 // p29,q29 by A14,AFF_1:10;
then p1,q1 // p2,q2 by Th36;
then a,b _|_ p2,q2 by A3,A7,Th62;
then a,b // c,d by A8,A12,Th63;
hence thesis by A4,A6,A9,A11;
end;
theorem Th66:
M _|_ N implies ex p st p in M & p in N
proof
reconsider M9=M,N9=N as Subset of the AffinStruct of POS;
assume
A1: M _|_ N;
then M is being_line;
then
A2: M9 is being_line by Th43;
N is being_line by A1,Th44;
then
A3: N9 is being_line by Th43;
not M // N by A1,Th52;
then not M9 // N9 by Th46;
hence thesis by A2,A3,AFF_1:58;
end;
theorem Th67:
a,b _|_ c,d implies ex p st LIN a,b,p & LIN c,d,p
proof
reconsider a9=a,b9=b,c9=c,d9=d as Element of the AffinStruct of POS;
assume
A1: a,b _|_ c,d;
A2: now
set M = Line(a,b),N = Line(c,d);
assume a<>b & c <>d;
then M _|_ N by A1,Th45;
then consider p such that
A3: p in M & p in N by Th66;
LIN a,b,p & LIN c,d,p by A3,Def10;
hence thesis;
end;
LIN a9,b9,a9 by AFF_1:7;
then
A4: LIN a,b,a by Th40;
A5: now
assume c =d;
then c,d // c,a by Th58;
then LIN c,d,a;
hence thesis by A4;
end;
LIN c9,d9,c9 by AFF_1:7;
then
A6: LIN c,d,c by Th40;
now
assume a=b;
then a,b // a,c by Th58;
then LIN a,b,c;
hence thesis by A6;
end;
hence thesis by A5,A2;
end;
theorem
a,b _|_ K implies ex p st LIN a,b,p & p in K
proof
assume a,b _|_ K;
then consider p,q such that
p<>q and
A1: K = Line(p,q) and
A2: a,b _|_ p,q;
consider c such that
A3: LIN a,b,c and
A4: LIN p,q,c by A2,Th67;
c in K by A1,A4,Def10;
hence thesis by A3;
end;
theorem Th69:
ex x st a,x _|_ p,q & LIN p,q,x
proof
A1: now
assume p<>q;
then consider x such that
A2: p,q // p,x & p,q _|_ x,a by Def7;
take x;
thus a,x _|_ p,q & LIN p,q,x by A2,Th61;
end;
now
assume
A3: p=q;
take x=a;
p,q // p,a by A3,Th58;
hence a,x _|_ p,q & LIN p,q,x by Th58;
end;
hence thesis by A1;
end;
theorem
K is being_line implies ex x st a,x _|_ K & x in K
proof
assume K is being_line;
then consider p,q such that
A1: p<>q and
A2: K = Line(p,q);
consider x such that
A3: a,x _|_ p,q and
A4: LIN p,q,x by Th69;
take x;
thus a,x _|_ K by A1,A2,A3;
thus thesis by A2,A4,Def10;
end;