Copyright (c) 1990 Association of Mizar Users
environ
vocabulary RLVECT_1, ARYTM_1, RELAT_1, ANALOAF, DIRAF, SYMSP_1, REALSET1,
INCSP_1, AFF_1, ANALMETR;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, DOMAIN_1, REAL_1,
STRUCT_0, DIRAF, RELSET_1, RLVECT_1, AFF_1, ANALOAF, REALSET1;
constructors DOMAIN_1, REAL_1, AFF_1, XREAL_0, MEMBERED, XBOOLE_0;
clusters DIRAF, ANALOAF, RELSET_1, STRUCT_0, SUBSET_1, XREAL_0, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0;
theorems REAL_1, RLVECT_1, ZFMISC_1, RELAT_1, AFF_1, FUNCSDOM, SQUARE_1,
DIRAF, ANALOAF, TARSKI, XCMPLX_0, XCMPLX_1;
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 that A1: v1 = b1*w + b2*y and A2: v2 = c1*w + c2*y;
thus v1 + v2 = ((b1*w + b2*y) + c1*w) + c2*y by A1,A2,RLVECT_1:def 6
.= ((b1*w + c1*w) + b2*y) + c2*y by RLVECT_1:def 6
.= ((b1 + c1)*w + b2*y) + c2*y by RLVECT_1:def 9
.= (b1 + c1)*w + (b2*y + c2*y) by RLVECT_1:def 6
.= (b1 + c1)*w + (b2 + c2)*y by RLVECT_1:def 9;
thus v1 - v2 = (b1*w + b2*y)+(-(c1*w + c2*y)) by A1,A2,RLVECT_1:def 11
.= (b1*w + b2*y)+(-(c1*w) + -(c2*y)) by RLVECT_1:45
.= (b1*w + b2*y)+(c1*(-w) + -(c2*y)) by RLVECT_1:39
.= (b1*w + b2*y)+(c1*(-w) + c2*(-y)) by RLVECT_1:39
.= (b1*w + b2*y)+((-c1)*w + c2*(-y)) by RLVECT_1:38
.= (b1*w + b2*y)+((-c1)*w + (-c2)*y) by RLVECT_1:38
.= ((b1*w + b2*y) + (-c1)*w) + (-c2)*y by RLVECT_1:def 6
.= ((b1*w + (-c1)*w) + b2*y) + (-c2)*y by RLVECT_1:def 6
.= ((b1 + (-c1))*w + b2*y) + (-c2)*y by RLVECT_1:def 9
.= (b1 + (-c1))*w + (b2*y + (-c2)*y) by RLVECT_1:def 6
.= (b1 + (-c1))*w + (b2 + (-c2))*y by RLVECT_1:def 9
.= (b1 - c1)*w + (b2 + (-c2))*y by XCMPLX_0:def 8
.= (b1 - c1)*w + (b2 - c2)*y by XCMPLX_0:def 8; end;
Lm2: a*(-b) = (-1)*(a*b)
proof thus a*(-b) = - 1*(a*b) by XCMPLX_1:175
.= (-1)*(a*b) by XCMPLX_1:175; end;
Lm3: a1*(b1-c1) + a2*(b2-c2) = (a1*b1 + a2*b2) + (-1)*(a1*c1 + a2*c2) proof
thus a1*(b1-c1) + a2*(b2-c2) = (a1*b1 - a1*c1) + a2*(b2-c2) by XCMPLX_1:40
.= (a1*b1 - a1*c1) + (a2*b2 - a2*c2) by XCMPLX_1:40
.= (a1*b1 + -a1*c1) + (a2*b2 - a2*c2) by XCMPLX_0:def 8
.= (a1*b1 + -a1*c1) + (a2*b2 + -a2*c2) by XCMPLX_0:def 8
.= (a1*b1 + a1*(-c1)) + (a2*b2 + -a2*c2) by XCMPLX_1:175
.= (a1*b1 + a1*(-c1)) + (a2*b2 + a2*(-c2)) by XCMPLX_1:175
.= ((a1*b1 + a1*(-c1)) + a2*b2) + a2*(-c2) by XCMPLX_1:1
.= ((a1*b1 + a2*b2) + a1*(-c1)) + a2*(-c2) by XCMPLX_1:1
.= (a1*b1 + a2*b2) + (a1*(-c1) + a2*(-c2)) by XCMPLX_1:1
.= (a1*b1 + a2*b2) + ((-1)*(a1*c1) + a2*(-c2)) by Lm2
.= (a1*b1 + a2*b2) + ((-1)*(a1*c1) + (-1)*(a2*c2)) by Lm2
.= (a1*b1 + a2*b2) + (-1)*(a1*c1 + a2*c2) by XCMPLX_1:8; end;
Lm4: 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:23 .=0.V + 0.V by RLVECT_1:23
.= 0.V by RLVECT_1:10; end;
Lm5: 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 9 .= (a*b1)*w + a*(b2*y) by RLVECT_1:def 9
.= (a*b1)*w + (a*b2)*y by RLVECT_1:def 9; 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;
Lm6: 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:28 .= (a1-b1)*w+(a2-b2)*y by
Lm1
;
then a1-b1=0 & a2-b2=0 by A1,Def1;
then -b1 + a1 =0 & -b2 + a2 = 0 by XCMPLX_0:def 8;
then a1=-(-b1) & a2=-(-b2) by XCMPLX_0:def 6; hence thesis; end;
canceled 4;
theorem Th5: 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 & v = b1*w + b2*y and
A3: a1*b1 + a2*b2 = 0 by Def2; let a1',a2',b1',b2' be Real;
assume u = a1'*w + a2'*y & v = b1'*w + b2'*y;
then a1=a1' & a2=a2' & b1=b1' & b2=b2' by A1,A2,Lm6; hence
0 = a1'*b1' + a2'*b2' by A3; end;
assume A4: for a1,a2,b1,b2 st u = a1*w + a2*y & v = b1*w + b2*y
holds a1*b1 + a2*b2 = 0; consider a1,a2 such that
A5: u = a1*w + a2*y by A1,Def1; consider b1,b2 such that
A6: v = b1*w + b2*y by A1,Def1; a1*b1 + a2*b2 = 0 by A4,A5,A6;
hence u,v are_Ort_wrt w,y by A5,A6,Def2;
end;
Lm7: 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 9
.= 1*w + 0.V by RLVECT_1:10 .= 1*w + 0*y by RLVECT_1:23;
hence contradiction by A1,Def1; end;
thus y<>0.V proof assume y=0.V; then 0.V = 1*y by RLVECT_1:def 9
.= 0.V + 1*y by RLVECT_1:10 .= 0*w + 1*y by RLVECT_1:23;
hence contradiction by A1,Def1; end; end;
theorem
w,y are_Ort_wrt w,y proof
A1: w = w + 0.V by RLVECT_1:10 .= 1*w + 0.V by RLVECT_1:def 9
.= 1*w + 0*y by RLVECT_1:23;
A2: y = 0.V + y by RLVECT_1:10 .= 0.V + 1*y by RLVECT_1:def 9
.= 0*w + 1*y by RLVECT_1:23;
1*0 + 0*1 = 0;
hence thesis by A1,A2,Def2; end;
theorem Th7: ex V st ex w,y st Gen w,y proof consider V such that
A1: ex u,v st (for a,b st a*u + b*v = 0.V holds a=0 & b=0) &
(for w ex a,b st w = a*u + b*v) by FUNCSDOM:37;
consider u,v such that
A2: (for a,b st a*u + b*v = 0.V holds a=0 & b=0) &
(for w ex a,b st w = a*u + b*v) by A1;
take V; take u,v; thus Gen u,v by A2,Def1; end;
theorem Th8: u,v are_Ort_wrt w,y implies v,u 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 & v = b1*w + b2*y and A2: a1*b1 + a2*b2 = 0 by Def2;
thus thesis by A1,A2,Def2; end;
theorem Th9: 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,Def1; consider b1,b2 such that
A3: v = b1*w + b2*y by A1,Def1;
A4: 0.V = 0.V + 0.V by RLVECT_1:10 .= 0*w + 0.V by RLVECT_1:23
.= 0*w + 0*y by RLVECT_1:23;
a1*0 + a2*0 = 0;
hence u,0.V are_Ort_wrt w,y by A2,A4,Def2;
0*b1 + 0*b2 = 0;
hence 0.V,v are_Ort_wrt w,y by A3,A4,Def2; end;
theorem Th10: 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 & v = b1*w + b2*y and A2: a1*b1 + a2*b2 = 0 by Def2;
A3: a*u = a*(a1*w) + a*(a2*y) by A1,RLVECT_1:def 9
.= (a*a1)*w + a*(a2*y) by RLVECT_1:def 9 .= (a*a1)*w + (a*a2)*y by RLVECT_1:
def 9;
A4: b*v = b*(b1*w) + b*(b2*y) by A1,RLVECT_1:def 9
.= (b*b1)*w + b*(b2*y) by RLVECT_1:def 9 .= (b*b1)*w + (b*b2)*y by RLVECT_1:
def 9;
(a*a1)*(b*b1) + (a*a2)*(b*b2) = a*(a1*(b*b1)) + (a*a2)*(b*b2) by XCMPLX_1:4
.= a*(a1*(b*b1)) + a*(a2*(b*b2)) by XCMPLX_1:4 .=a*(a1*(b*b1) + a2*(b*b2))
by XCMPLX_1:8 .= a*((a1*b)*b1 + a2*(b*b2)) by XCMPLX_1:4
.= a*((b*a1)*b1 + (b*a2)*b2) by XCMPLX_1:4
.= a*(b*(a1*b1) + (b*a2)*b2) by XCMPLX_1:4 .= a*(b*(a1*b1) + b*(a2*b2))
by XCMPLX_1:4 .= a*(b*0) by A2,XCMPLX_1:8
.= 0;
hence thesis by A3,A4,Def2; end;
theorem Th11: 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 assume A1: u,v are_Ort_wrt w,y; v = 1*v & u = 1*u by RLVECT_1:def 9;
hence thesis by A1,Th10; end;
theorem Th12: 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,Def1;
A3: now assume A4: u = 0.V; take v=w; thus u,v are_Ort_wrt w,y by A1,A4,Th9;
thus v<>0.V by A1,Lm7; end;
now assume A5: u<>0.V; set v = a2*w + (-a1)*y;
A6: v<>0.V proof assume v=0.V; then a2 = 0 & -a1 = 0 by A1,Def1;
then u = 0*w + 0*y by A2,XCMPLX_1:135 .= 0*w + 0.V by RLVECT_1:23 .= 0*w
by RLVECT_1:10 .= 0.V by RLVECT_1:23; hence contradiction by A5; end;
A7: a1*a2 + a2*(-a1) = a1*a2 + (-(a1*a2)) by XCMPLX_1:175
.= 0 by XCMPLX_0:def 6; take v;
thus u,v are_Ort_wrt w,y by A2,A7,Def2; thus v<>0.V by A6; end;
hence thesis by A3; end;
theorem Th13: 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 & u1 = b1*w + b2*y and A6: a1*b1 + a2*b2 = 0 by A2,Def2;
consider a1',a2',c1,c2 being Real such that
A7: v = a1'*w + a2'*y & u2 = c1*w + c2*y and
A8: a1'*c1 + a2'*c2 = 0 by A3,Def2;
A9: a1 = a1' & a2 = a2' by A1,A5,A7,Lm6;
A10: now assume A11: a1=0;
then A12: a2<>0 by A4,A5,Lm4;
then A13: c2 = 0 by A8,A9,A11,XCMPLX_1:6;
b2 = 0 by A6,A11,A12,XCMPLX_1:6;
then A14:u1 = b1*w + 0.V & u2 = c1*w + 0.V by A5,A7,A13,RLVECT_1:23;
then A15: u1 = b1*w & u2 = c1*w by RLVECT_1:10;
A16: c1*u1 = c1*(b1*w) by A14,RLVECT_1:10
.= (b1*c1)*w by RLVECT_1:def 9 .= b1*u2 by A15,RLVECT_1:def 9;
now assume b1=0;
then 1*u1 = 0*w by A15,RLVECT_1:def 9 .= 0.V by RLVECT_1:23 .= 0*u2
by RLVECT_1:23; hence ex a,b st a*u1 = b*u2 & (a<>0 or b<>0); end;
hence ex a,b st a*u1 = b*u2 & (a<>0 or b<>0) by A16; end;
now assume A17: a1<>0;A18: a1*b1 = - a2*b2 & a1*c1 = - a2*c2 by A6,A8,A9,
XCMPLX_0:def 6;
A19: b1 = 1*b1 .= (a1*a1")*b1 by A17,XCMPLX_0:def 7
.= (a1*b1)*a1" by XCMPLX_1:4
.= ((-a2)*b2)*a1" by A18,XCMPLX_1:175;
A20: c1 = 1*c1 .= (a1*a1")*c1 by A17,XCMPLX_0:def 7
.= (a1*c1)*a1" by XCMPLX_1:4
.= ((-a2)*c2)*a1" by A18,XCMPLX_1:175;
then A21: b2*u2 = (b2*(((-a2)*c2)*a1"))*w + (b2*c2)*y by A7,Lm5;
A22: c2*(((-a2)*b2)*a1") = (c2*(b2*(-a2)))*a1" by XCMPLX_1:4 .=
(b2*(c2*(-a2)))*a1" by XCMPLX_1:4
.= b2*(((-a2)*c2)*a1") by XCMPLX_1:4;
A23: now assume A24: c2<>0 or b2<>0; take a=c2,b=b2;
thus a*u1 = b*u2 & (a<>0 or b<>0) by A5,A19,A21,A22,A24,Lm5; end;
now assume b2=0 & c2=0;
then 1*u1 = 1*u2 by A5,A7,A19,A20;
hence ex a,b st a*u1 = b*u2 & (a<>0 or b<>0); end;
hence ex a,b st a*u1 = b*u2 & (a<>0 or b<>0) by A23; end;
hence thesis by A10; end;
theorem Th14: 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 & v1 = b1*w + b2*y and A5: a1*b1 + a2*b2 = 0 by A2,Def2;
consider a1',a2',c1,c2 being Real such that
A6: u = a1'*w + a2'*y & v2 = c1*w + c2*y and
A7: a1'*c1 + a2'*c2 = 0 by A3,Def2;
A8: a1 = a1' & a2 = a2' by A1,A4,A6,Lm6;
A9: v1 + v2 = (b1 + c1)*w + (b2 + c2)*y by A4,A6,Lm1;
a1*(b1+c1) + a2*(b2+c2) = (a1*b1 + a1*c1) + a2*(b2+c2) by XCMPLX_1:8
.= (a1*b1 + a1*c1) + (a2*b2 + a2*c2) by XCMPLX_1:8
.= ((a1*b1 + a1*c1) + a2*b2) + a2*c2 by XCMPLX_1:1
.= ((a1*b1 + a2*b2) + a1*c1) + a2*c2 by XCMPLX_1:1
.= 0 by A5,A7,A8;
hence u,v1+v2 are_Ort_wrt w,y by A4,A9,Def2;
A10: v1 - v2 = (b1 - c1)*w + (b2 - c2)*y by A4,A6,Lm1;
a1*(b1-c1) + a2*(b2-c2) = 0 + (-1)*0 by A5,A7,A8,Lm3 .= 0;
hence u,v1-v2 are_Ort_wrt w,y by A4,A10,Def2;
end;
theorem Th15: Gen w,y & u,u are_Ort_wrt w,y implies u = 0.V
proof assume that A1: Gen w,y and A2: u,u are_Ort_wrt w,y;
consider a1,a2,b1,b2 such that A3: u = a1*w + a2*y & u = b1*w + b2*y
and A4: a1*b1 + a2*b2 = 0 by A2,Def2;
A5: a1=b1 & a2=b2 by A1,A3,Lm6;
A6: now let a such that A7: a<>0;
0 < a implies 0 < a*a by SQUARE_1:21;
hence 0 < a*a by A7,SQUARE_1:22; end;
A8: a1 = 0 proof assume a1<>0; then 0 < a1*a1 by A6;
then a2*a2 < a1*a1 + a2*a2 by REAL_1:69;
hence contradiction by A4,A5,REAL_1:93; end;
a2 = 0 proof assume a2<>0; then A9: 0 < a2*a2 by A6;
0 <= a1*a1 by REAL_1:93;
hence contradiction by A4,A5,A9,REAL_1:69; end;
hence u = 0*w + 0.V by A3,A8,RLVECT_1:23 .= 0*w
by RLVECT_1:10 .= 0.V by RLVECT_1:23; end;
theorem Th16: 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,Def1;
consider b1,b2 such that A5: u1 = b1*w + b2*y by A1,Def1;
consider c1,c2 such that A6: u2 = c1*w + c2*y by A1,Def1;
A7: u1-u2 = (b1-c1)*w + (b2-c2)*y & u2-u = (c1-a1)*w + (c2-a2)*y
& u-u1 = (a1-b1)*w + (a2-b2)*y by A4,A5,A6,Lm1;
then a1*(b1-c1) + a2*(b2-c2) = 0 & b1*(c1-a1) + b2*(c2-a2) = 0
by A1,A2,A3,A4,A5,Th5;
then A8: (a1*b1 + a2*b2) + (-1)*(a1*c1 + a2*c2) = 0 &
(b1*c1 + b2*c2) + (-1)*(b1*a1 + b2*a2) = 0 by Lm3;
set d1 = a1*b1 + a2*b2, d2= a1*c1 + a2*c2, d3 = b1*c1 + b2*c2;
A9: 0 =
(((-1)*d2 + d1) + d3) + (-1)*d1 by A8
.= ((-1)*d2 + (d3 + d1)) +
(-1)*d1 by XCMPLX_1:1 .=
(-1)*d2 + ((d3 + d1) + (-1)*d1) by XCMPLX_1:1 .= (-1)*d2 + (d3 + (d1 +
(-1)*d1)) by XCMPLX_1:1 .= (-1)*d2 + (d3 + (d1 + -1*d1)) by XCMPLX_1:175
.= (-1)*d2 + (d3 + 0)
by XCMPLX_0:def 6 .= (-1)*(c1*a1 + c2*a2) +
(c1*b1 + c2*b2);
A10: (-1)*(-1) = 1;
0 = (-1)*((-1)*(c1*a1 + c2*a2) + (c1*b1 + c2*b2)) by A9
.= (-1)*((-1)*(c1*a1 + c2*a2)) + (-1)*(c1*b1 + c2*b2) by XCMPLX_1:8
.= 1*(c1*a1 + c2*a2) + (-1)*(c1*b1 + c2*b2) by A10,XCMPLX_1:4
.= c1*(a1-b1) + c2*(a2-b2) by Lm3;
hence thesis by A6,A7,Def2; end;
theorem Th17: (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,Def1;
consider b1,b2 such that A4: v = b1*w + b2*y by A1,Def1;
set a = (b1*a1 + b2*a2)*(a1*a1 + a2*a2)";
A5: a1*a1 + a2*a2 <> 0 proof assume a1*a1 + a2*a2 = 0;
then u,u are_Ort_wrt w,y by A3,Def2; hence contradiction by A1,A2,Th15; end
;
a*u = (a*a1)*w + (a*a2)*y by A3,Lm5;
then A6: v - a*u = (b1-a*a1)*w + (b2-a*a2)*y by A4,Lm1;
A7: (b1-a*a1)*a1 + (b2-a*a2)*a2 = (a1*b1 + a2*b2) +
(-1)*(a1*(a*a1) + a2*(a*a2)) by Lm3; (-1)*(a1*(a*a1) + a2*(a*a2)) =
(-1)*(a*(a1*a1) + (a*a2)*a2) by XCMPLX_1:4
.= (-1)*(a*(a1*a1) + a*(a2*a2)) by XCMPLX_1:4
.= (-1)*(a*(a1*a1 + a2*a2)) by XCMPLX_1:8
.= (-1)*((b1*a1 + b2*a2)*((a1*a1 + a2*a2)"*(a1*a1 + a2*a2)))
by XCMPLX_1:4 .= (-1)*((b1*a1 + b2*a2)*1) by A5,XCMPLX_0:def 7 .=
-(a1*b1 + a2*b2) by XCMPLX_1:175; then (b1-a*a1)*a1 + (b2-a*a2)*a2 = 0
by A7,XCMPLX_0:def 6; then v - a*u,u are_Ort_wrt w,y by A3,A6,Def2;
hence thesis; end;
theorem Th18: (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 such that A2: w,y // w1,y1;
A3: now assume w=y; then y - w = 0.V by RLVECT_1:28;
then 1*(y-w) = 0.V by RLVECT_1:23 .= 0*(y1-w1) by RLVECT_1:23;
hence ex a,b st a*(y-w) = b*(y1-w1) & (a<>0 or b<>0); end;
A4: now assume w1=y1; then y1-w1 = 0.V by RLVECT_1:28;
then 1*(y1-w1) = 0.V by RLVECT_1:23 .= 0*(y-w) by RLVECT_1:23;
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 A2,A3,A4,ANALOAF:def 1
; end;
A5: now assume u,v // v1,u1; then consider a,b such that
A6: a*(v-u) = b*(u1-v1) and A7: a<>0 or b<>0 by A1;
A8: (-b)*(v1-u1) = b*(-(v1-u1)) by RLVECT_1:38 .= b*(u1 + (-v1)) by RLVECT_1
:47 .= a*(v-u) by A6,RLVECT_1:def 11;
a<>0 or -b<>0 by A7,XCMPLX_1:135; hence
ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by A8; end;
A9: now let w,y,w1,y1 be VECTOR of V; given a,b such that
A10: a*(y-w) = b*(y1-w1) and A11: a=0 & b<>0;
0.V = b*(y1-w1) by A10,A11,RLVECT_1:23;
then y1-w1 = 0.V by A11,RLVECT_1:24; then y1 = w1 by RLVECT_1:35;
hence w,y // w1,y1 by ANALOAF:18; end;
A12: now let w,y,w1,y1 be VECTOR of V; given a,b such that
A13: a*(y-w) = b*(y1-w1) and A14: 0<a & b<0;
A15: 0<-b by A14,REAL_1:66;
a*(y-w) = b*((-w1)+y1) by A13,RLVECT_1:def 11
.= b*(-(w1-y1)) by RLVECT_1:47 .= (-b)*(w1-y1) by RLVECT_1:38;
hence w,y // y1,w1 by A14,A15,ANALOAF:def 1; end;
now given a,b such that A16: a*(v-u) = b*(v1-u1) and A17: (a<>0 or b<>0);
A18: now assume b=0; then u1,v1 // u,v by A9,A16,A17;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:21; end;
now assume A19: a<>0 & b<>0;
A20: 0<a & b<0 implies ( u,v // u1,v1 or u,v // v1,u1) by A12,A16;
A21: now assume a<0 & 0<b; then u1,v1 // v,u by A12,A16; then v,u // u1,
v1
by ANALOAF:21;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:21; end;
now assume a<0 & b<0; then A22: 0< -a & 0< -b by REAL_1:66;
(-a)*(u-v) = a*(-(u-v)) by RLVECT_1:38 .= a*(v+(-u)) by RLVECT_1:47
.= b*(v1-u1) by A16,RLVECT_1:def 11
.= b*((-u1)+v1) by RLVECT_1:def 11
.= b*(-(u1-v1)) by RLVECT_1:47 .= (-b)*(u1-v1) by RLVECT_1:38;
then v,u // v1,u1 by A22,ANALOAF:def 1;
hence u,v // u1,v1 or u,v // v1,u1 by ANALOAF:21; end;
hence u,v // u1,v1 or u,v // v1,u1 by A16,A19,A20,A21,ANALOAF:def 1; end;
hence u,v // u1,v1 or u,v // v1,u1 by A9,A16,A18; end;
hence thesis by A1,A5; end;
theorem Th19: [[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:33; hence thesis by Th18; end;
definition let V; let u,u1,v,v1,w,y;
pred u,u1,v,v1 are_Ort_wrt w,y means
:Def3: 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: [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 set VV = [:the carrier of V,the carrier of V:];
defpred P[set, set] means ex u,u1,v,v1 st
$1=[u,u1] & $2=[v,v1] & u,u1,v,v1 are_Ort_wrt w,y;
consider P being Relation of VV,VV such that
A1: for x,z holds ([x,z] in P iff
x in VV & z in VV & P[x,z]) from Rel_On_Set_Ex;
take P; let x,z;
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 [x,z] in P by A1; end;
uniqueness proof let P,Q be Relation of [:the carrier of V,the carrier of V:]
such that
A2: [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: [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 holds [x,z] in P iff [x,z] in Q proof let x,z;
[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));
canceled 2;
theorem Th22: the carrier of Lambda(OASpace(V)) = the carrier of V proof
A1: Lambda(OASpace(V)) = AffinStruct(#the carrier of OASpace(V),
lambda(the CONGR of OASpace(V))#) by DIRAF:def 2;
OASpace(V) = AffinStruct (#the carrier of V, DirPar(V)#) by ANALOAF:def 4;
hence the carrier of Lambda(OASpace(V)) = the carrier of V by A1; end;
theorem Th23: the CONGR of Lambda(OASpace(V)) = lambda(DirPar(V)) proof
A1: Lambda(OASpace(V)) = AffinStruct(#the carrier of OASpace(V),
lambda(the CONGR of OASpace(V))#) by DIRAF:def 2;
OASpace(V) = AffinStruct (#the carrier of V, DirPar(V)#) by ANALOAF:def 4;
hence thesis by A1; 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,Th23;
hence ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by Th19; 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,Th19;
then [[p,q],[p1,q1]] in the CONGR of Lambda(OASpace(V)) by A1,Th23;
hence p,q // p1,q1 by ANALOAF:def 2;
end;
definition
struct(AffinStruct) ParOrtStr (# carrier -> set,
CONGR -> (Relation of [:the carrier,the carrier:]),
orthogonality -> Relation of [:the carrier,the carrier:] #);
end;
definition
cluster non empty ParOrtStr;
existence
proof
consider A being non empty set,
C,o being Relation of [:A,A:];
take ParOrtStr (#A,C,o#);
thus the carrier of ParOrtStr (#A,C,o#) is non empty;
end;
end;
reserve POS for non empty ParOrtStr;
definition let POS; let a,b,c,d be Element of POS;
pred a,b // c,d means :Def5: [[a,b],[c,d]] in the CONGR of POS;
pred a,b _|_ c,d means :Def6: [[a,b],[c,d]] in the orthogonality of POS;
end;
definition let V,w,y;
func AMSpace(V,w,y) -> strict ParOrtStr equals
:Def7:
ParOrtStr(#the carrier of V,lambda(DirPar(V)),Orthogonality(V,w,y)#);
correctness;
end;
definition let V,w,y;
cluster AMSpace(V,w,y) -> non empty;
coherence
proof
AMSpace(V,w,y)
= ParOrtStr(#the carrier of V,lambda(DirPar(V)),Orthogonality(V,w,y)#)
by Def7;
hence the carrier of AMSpace(V,w,y) is non empty;
end;
end;
canceled 3;
theorem Th28:
(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)) proof
AMSpace(V,w,y) = ParOrtStr(#the carrier of V,
lambda(DirPar(V)),Orthogonality(V,w,y)#) by Def7; hence thesis; end;
definition let POS; func Af(POS) -> strict AffinStruct equals
:Def8: AffinStruct (# the carrier of POS, the CONGR of POS #);
correctness; end;
definition let POS;
cluster Af POS -> non empty;
coherence
proof
Af POS = AffinStruct (# the carrier of POS, the CONGR of POS #) by Def8;
hence the carrier of Af POS is non empty;
end;
end;
canceled;
theorem Th30: Af(AMSpace(V,w,y)) = Lambda(OASpace(V))
proof
A1: AMSpace(V,w,y)
= ParOrtStr(#the carrier of V,lambda(DirPar(V)),Orthogonality(V,w,y)#)
by Def7;
set Y = OASpace(V);
the carrier of Lambda(Y) = the carrier of V & the CONGR of Lambda(Y) =
lambda(DirPar(V)) by Th22,Th23;
hence thesis by A1,Def8; end;
reserve p,p1,p2,q,q1,r,r1,r2 for Element of AMSpace(V,w,y);
theorem Th31: 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 that A1: p=u & p1=u1 & q=v & q1=v1;
A2: p,q _|_ p1,q1 iff [[p,q],[p1,q1]] in the orthogonality of AMSpace(V,w,y)
by Def6;
hereby assume p,q _|_ p1,q1; then [[u,v],[u1,v1]] in
Orthogonality(V,w,y) by A1,A2,Th28;
then consider u',v',u1',v1' being VECTOR of V such that
A3: [u,v] = [u',v'] & [u1,v1] = [u1',v1'] and
A4: u',v',u1',v1' are_Ort_wrt w,y by Def4;
u=u' & v=v' & u1=u1' & v1=v1' by A3,ZFMISC_1:33;
hence u,v,u1,v1 are_Ort_wrt w,y by A4; end;
assume u,v,u1,v1 are_Ort_wrt w,y;
then [[u,v],[u1,v1]] in Orthogonality(V,w,y) by Def4;
hence p,q _|_ p1,q1 by A1,A2,Th28;
end;
theorem Th32: 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 that 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 Def5;
then [[u,v],[u1,v1]] in lambda(DirPar(V)) by A1,Th28;
hence ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by Th19; 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,Th19;
then [[p,q],[p1,q1]] in the CONGR of AMSpace(V,w,y) by A1,Th28;
hence p,q // p1,q1 by Def5;
end;
theorem Th33: p,q _|_ p1,q1 implies p1,q1 _|_ p,q
proof assume that A1: p,q _|_ p1,q1;
reconsider u=p,v=q,u1=p1,v1=q1 as Element of V by Th28;
u,v,u1,v1 are_Ort_wrt w,y
by A1,Th31; then v-u,v1-u1 are_Ort_wrt w,y by Def3;
then v1-u1,v-u are_Ort_wrt w,y by Th8; then u1,v1,u,v are_Ort_wrt w,y
by Def3; hence thesis by Th31; end;
theorem Th34: p,q _|_ p1,q1 implies p,q _|_ q1,p1
proof assume that A1: p,q _|_ p1,q1;
reconsider u=p,v=q,u1=p1,v1=q1 as Element of V by Th28;
u,v,u1,v1 are_Ort_wrt w,y
by A1,Th31; then v-u,v1-u1 are_Ort_wrt w,y by Def3;
then A2: v-u,(-1)*(v1-u1) are_Ort_wrt w,y by Th11;
(-1)*(v1-u1) = -(v1-u1) by RLVECT_1:29 .= u1+(-v1) by RLVECT_1:47
.= u1-v1 by RLVECT_1:def 11;
then u,v,v1,u1 are_Ort_wrt w,y by A2,Def3;
hence thesis by Th31; end;
theorem Th35: 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 by Th28;
u1-u1 = 0.V by RLVECT_1:28;
then v-u,u1-u1 are_Ort_wrt w,y by A1,Th9; then u,v,u1,u1 are_Ort_wrt w,y
by Def3; hence thesis by Th31; end;
theorem
Th36: 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;
assume A3: p<>p1;
reconsider u=p,v=p1,u1=q,v1=q1,u2=r,v2=r1 as Element of V by
Th28;
u,v,u1,v1 are_Ort_wrt w,y by A1,Th31;
then A4: v-u,v1-u1 are_Ort_wrt w,y by Def3;
consider a,b such that A5: a*(v-u) = b*(v2-u2) and A6: a<>0 or b<>0
by A2,Th32; b<>0 proof assume b=0;
then a*(v-u) = 0.V & a<>0 by A5,A6,RLVECT_1:23; then v-u = 0.V
by RLVECT_1:24; hence contradiction by A3,RLVECT_1:35; end;
then v2-u2 = b"*(a*(v-u)) by A5,ANALOAF:12 .= (b"*a)*(v-u) by RLVECT_1:def 9;
then v2-u2,v1-u1 are_Ort_wrt w,y by A4,Th11; then v1-u1,v2-u2 are_Ort_wrt w,
y
by Th8; then u1,v1,u2,v2 are_Ort_wrt w,y by Def3;
hence thesis by Th31; end;
theorem Th37: 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 by Th28;
consider v2 such that
A2: v-u,v2 are_Ort_wrt w,y & v2<>0.V by A1,Th12; set v1 = u1+v2;
A3: v1-u1 = v2+(u1-u1)
by RLVECT_1:42 .= v2+0.V by RLVECT_1:28 .= v2 by RLVECT_1:10;
then A4: u,v,u1,v1 are_Ort_wrt w,y by A2,Def3;
reconsider r1=v1 as Element of AMSpace(V,w,y) by Th28;
p,q _|_ r,r1 & r<>r1 by A2,A3,A4,Th31,RLVECT_1:28; hence thesis; end;
theorem Th38: 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;
assume A4: p<>p1;
reconsider u=p,v=p1,u1=q,v1=q1,u2=r,v2=r1 as Element of V by
Th28;
u,v,u1,v1 are_Ort_wrt w,y & u,v,u2,v2 are_Ort_wrt w,y by A2,A3,Th31;
then A5: v-u,v1-u1 are_Ort_wrt w,y & v-u,v2-u2 are_Ort_wrt w,y by Def3;
v-u <> 0.V by A4,RLVECT_1:35; then ex a,b st
a*(v1-u1) = b*(v2-u2) & (a<>0 or b<>0) by A1,A5,Th13;
hence thesis by Th32; end;
theorem Th39: 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 by Th28;
u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y by A2,A3,Th31;
then v-u,v1-w1 are_Ort_wrt w,y & v-u,v2-w1 are_Ort_wrt w,y by Def3;
then A4: v-u,(v2-w1)-(v1-w1) are_Ort_wrt w,y by A1,Th14;
(v2-w1)-(v1-w1) = v2-((v1-w1)+w1) by RLVECT_1:41
.= v2-(v1-(w1-w1)) by RLVECT_1:43 .= v2-(v1-0.V) by RLVECT_1:28
.= v2-v1 by RLVECT_1:26;
then u,v,v1,v2 are_Ort_wrt w,y by A4,Def3; hence thesis by Th31; end;
theorem Th40: 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 by Th28;
u,v,u,v are_Ort_wrt w,y by A2,Th31;
then v-u,v-u are_Ort_wrt w,y by Def3; then v-u = 0.V by A1,Th15;
hence thesis by RLVECT_1:35; 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 by Th28;
u,v,u1,u2 are_Ort_wrt w,y
& u1,v,u2,u are_Ort_wrt w,y by A2,A3,Th31;
then A4: v-u,u2-u1 are_Ort_wrt w,y & v-u1,u-u2 are_Ort_wrt w,y by Def3;
A5: now let u,v,w; thus (u-v)-(u-w) = (w-u) +
(u-v) by ANALOAF:6 .= w-v by ANALOAF:4; end;
then A6: (v-u1)-(v-u2)=u2-u1; A7: (v-u2)-(v-u)=u-u2 by A5;
A8: (v-u)-(v-u1)=u1-u by A5; v-u2,(v-u)-(v-u1) are_Ort_wrt w,y by A1,A4,A6,A7,
Th16; then u2,v,u,u1 are_Ort_wrt w,y by A8,Def3; hence thesis by Th31; end;
theorem
Th42: 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 by Th28;
u1-u <> 0.V by A2,RLVECT_1:35;
then consider a such that
A3: (v-u) - a*(u1-u),u1-u are_Ort_wrt w,y by A1,Th17; set v1 = u + a*(u1-u);
reconsider q1=v1 as Element of AMSpace(V,w,y) by Th28;
a*(u1-u) = a*(u1-u)+0.V by RLVECT_1:10 .= a*(u1-u)+(u-u)
by RLVECT_1:28 .= v1-u by RLVECT_1:42
.= 1*(v1-u) by RLVECT_1:def 9;
then A4: p,p1 // p,q1 by Th32;
v-v1 = (v-u)- a*(u1-u) by RLVECT_1:41;
then u1-u,v-v1 are_Ort_wrt w,y by A3,Th8;
then u,u1,v1,v are_Ort_wrt w,y by Def3;
then p,p1 _|_ q1,q by Th31; hence thesis by A4; end;
consider V0 being RealLinearSpace such that
Lm8: ex w,y being VECTOR of V0 st Gen w,y by Th7;
consider w0,y0 being VECTOR of V0 such that Lm9: Gen w0,y0 by Lm8;
Lm10: now
set X = AffinStruct(#the carrier of AMSpace(V0,w0,y0),
the CONGR of AMSpace(V0,w0,y0)#);
X = Af(AMSpace(V0,w0,y0))
by Def8; then A1: X = Lambda(OASpace(V0)) by Th30;
for a,b being Real st a*w0 + b*y0 = 0.V0 holds a=0 & b=0 by Def1,Lm9;
then OASpace(V0) is OAffinSpace by ANALOAF:38;
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,Lm9,Th33,Th34,Th35,Th36,Th37,Th39,Th40,Th42,DIRAF:48;
end;
definition let IT be non empty ParOrtStr;
attr IT is OrtAfSp-like means
:Def9: 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;
definition
cluster strict OrtAfSp-like (non empty ParOrtStr);
existence
proof
AMSpace(V0,w0,y0) is OrtAfSp-like by Def9,Lm10;
hence thesis;
end;
end;
definition
mode OrtAfSp is OrtAfSp-like (non empty ParOrtStr);
end;
canceled;
theorem Gen w,y implies AMSpace(V,w,y) is OrtAfSp
proof assume A1: Gen w,y; set POS = AMSpace(V,w,y);
A2: 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 A1,Th33,Th34,Th35,Th36,
Th39,Th40;
A3: 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,Th42;
A4: for a,b,c be Element of POS holds ( ex x being
Element of POS st a,b _|_ c,x & c <>x) by A1,Th37;
set X = AffinStruct(#the carrier of POS,the CONGR of POS#); X = Af(POS)
by Def8; then A5: X = Lambda(OASpace(V)) by Th30;
for a,b being Real st a*w + b*y = 0.V holds a=0 & b=0 by A1,Def1;
then OASpace(V) is OAffinSpace by ANALOAF:38; then X is AffinSpace
by A5,DIRAF:48; hence thesis by A2,A3,A4,Def9; end;
consider V0 being RealLinearSpace such that
Lm11: ex w,y being VECTOR of V0 st Gen w,y by Th7;
consider w0,y0 being VECTOR of V0 such that Lm12: Gen w0,y0 by Lm11;
Lm13:
now
set X = AffinStruct(#the carrier of AMSpace(V0,w0,y0),
the CONGR of AMSpace(V0,w0,y0)#);
X = Af(AMSpace(V0,w0,y0))
by Def8; then A1: X = Lambda(OASpace(V0)) by Th30;
(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 Def1,Lm12;
then OASpace(V0) is OAffinPlane by ANALOAF:51;
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,Lm12,Th33,Th34,Th35,Th36,Th37,Th38,Th40,DIRAF:53;
end;
definition let IT be non empty ParOrtStr;
attr IT is OrtAfPl-like means
:Def10: 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;
definition
cluster strict OrtAfPl-like (non empty ParOrtStr);
existence
proof
AMSpace(V0,w0,y0) is OrtAfPl-like by Def10,Lm13;
hence thesis;
end;
end;
definition
mode OrtAfPl is OrtAfPl-like (non empty ParOrtStr);
end;
canceled;
theorem Gen w,y implies AMSpace(V,w,y) is OrtAfPl
proof assume A1: Gen w,y; set POS = AMSpace(V,w,y);
A2: 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 A1,Th33,Th34,Th35,Th36,Th38,Th40;
A3: for a,b,c be Element of POS holds ( ex x being
Element of POS st a,b _|_ c,x & c <>x) by A1,Th37;
set X = AffinStruct(#the carrier of POS,the CONGR of POS#); X = Af(POS)
by Def8; then A4: X = Lambda(OASpace(V)) by Th30;
(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) by A1,Def1;
then OASpace(V) is OAffinPlane by ANALOAF:51;
then X is AffinPlane by A4,DIRAF:53; hence thesis by A2,A3,Def10;end;
theorem
Th47: for x being set holds (x is Element of POS iff
x is Element of Af(POS))
proof let x be set;
Af(POS) = AffinStruct(#the carrier of POS, the CONGR of POS#) by Def8;
hence thesis; end;
theorem
Th48: for a,b,c,d being Element of POS, a',b',c',d' being
Element of Af(POS) st a=a'& b=b' & c = c' & d=d' holds
(a,b // c,d iff a',b' // c',d')
proof let a,b,c,d be Element of POS, a',b',c',d' be Element
of the carrier of Af(POS) such that
A1: a=a' & b=b' & c = c' & d=d'; set AF = Af(POS);
A2: AF = AffinStruct(#the carrier of POS, the CONGR of POS#) by Def8;
hereby assume a,b // c,d; then [[a',b'],[c',d']] in the CONGR of AF by A1,A2,
Def5;
hence a',b' // c',d' by ANALOAF:def 2; end;
assume a',b' // c',d';
then [[a,b],[c,d]] in the CONGR of POS by A1,A2,ANALOAF:def 2;
hence a,b // c,d by Def5; end;
Lm14: for POS being OrtAfSp holds Af(POS) is AffinSpace
proof let POS be OrtAfSp;
Af(POS) = AffinStruct(#the carrier of POS,the CONGR of POS#) by Def8;
hence thesis by Def9; end;
definition let POS be OrtAfSp;
cluster Af(POS) -> AffinSpace-like non trivial;
correctness by Lm14;
end;
Lm15: for POS being OrtAfPl holds Af(POS) is AffinPlane
proof let POS be OrtAfPl;
Af(POS) = AffinStruct(#the carrier of POS,the CONGR of POS#) by Def8;
hence thesis by Def10; end;
definition let POS be OrtAfPl;
cluster Af(POS) -> 2-dimensional AffinSpace-like non trivial;
correctness by Lm15;
end;
theorem Th49: for POS being OrtAfPl holds POS is OrtAfSp
proof let POS be OrtAfPl;
A1: Af(POS)
= AffinStruct(#the carrier of POS, the CONGR of POS#) by Def8;
A2:for a,b,c being Element of POS ex x being Element
of the carrier of POS st a,b _|_ c,x & c <>x by Def10;
A3: 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 A4: a,b _|_ p,q & a,b _|_ p,s;
A5: now assume a=b; then q,s _|_ a,b by Def10; hence a,b _|_ q,s by Def10
; end;
now assume A6: a<>b & p<>q; then A7: p,q // p,s by A4,Def10;
reconsider p'=p,q'=q,s'=s as Element of Af(POS) by Th47;
A8: p,q _|_ a,b by A4,Def10;
p',q' // p',s' by A7,Th48; then q',p' // q',s' by DIRAF:47;
then p',q' // q',s' by AFF_1:13; then p,q // q,s by Th48; hence a,b _|_
q,s
by A6,A8,Def10; end;
hence thesis by A4,A5; end;
A9: 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 A10: a<>b;
consider y being Element of POS such that
A11: a,b _|_ c,y & c <>y by Def10; reconsider a'=a,b'=b,c'=c,y'=y
as Element of Af(POS) by Th47;
not a',b' // c',y' proof assume not thesis; then a,b // c,y by Th48;
then c,y _|_ c,y by A10,A11,Def10; hence contradiction by A11,Def10; end;
then consider x' being Element of Af(POS) such that
A12: LIN a',b',x' & LIN c',y',x' by AFF_1:74;
reconsider x=x' as Element of POS by Th47;
a',b' // a',x' & c',y' // c',x' by A12,AFF_1:def 1;
then A13: a,b // a,x & c,y // c,x by Th48; c,y _|_ a,b by A11,Def10;
then a,b _|_ c,x by A11,A13,Def10; then a,b _|_ x,c by Def10
; hence thesis by A13; end;
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 A3,Def10;
hence POS is OrtAfSp by A1,A2,A9,Def9; end;
definition
cluster OrtAfPl-like -> OrtAfSp-like (non empty ParOrtStr);
coherence by Th49; end;
theorem for POS being OrtAfSp st Af(POS) is AffinPlane
holds POS is OrtAfPl
proof let POS be OrtAfSp such that A1: Af(POS) is AffinPlane;
A2: Af(POS) = AffinStruct(#the carrier of POS,the CONGR of POS#) by Def8;
A3: for a,b,c being Element of POS
ex x being Element of POS st a,b _|_ c,x & c <>x by Def9;
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 Def9;
thus a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b proof assume
A4: a,b _|_ p,q & a,b _|_ r,s; assume A5:
not thesis;
reconsider a'=a,b'=b,p'=p,q'=q,r'=r,s'=s as Element of Af(POS)
by Th47; A6: not p',q' // r',s' by A5,Th48;
then A7: p'<>q' & r'<>s' by AFF_1:12;
consider x' being Element of Af(POS) such that
A8: LIN p',q',x' & LIN r',s',x' by A1,A6,AFF_1:74;
reconsider x=x' as Element of POS by Th47;
A9: p,q _|_ a,b & r,s _|_ a,b by A4,Def9; LIN q',p',x' & LIN s',r',x'
by A8,AFF_1:15; then q',p' // q',x' & s',r' // s',x' & p',q' // p',x' &
r',s' // r',x' by A8,AFF_1:def 1; then A10: p',q' // x',q' & r',s' // x',s' &
p',q' // x',p' & r',s' // x',r' by AFF_1:13; then p,q // x,q & r,s // x,s
&
p,q // x,p & r,s // x,r by Th48; then A11: a,b _|_ x,q & a,b _|_ x,p & a,b
_|_ x,r
& a,b _|_ x,s by A7,A9,Def9; then A12: x,q _|_ a,b & x,p _|_ a,b & x,r _|_
a,b
& x,s _|_ a,b by Def9;
A13: now assume A14: x<>p & x<>r; consider y' being Element of
Af(POS) such that A15: a',b' // p',y' & p'<>y' by DIRAF:47;
not p',y' // x',r' proof assume not thesis;
then p',y' // r',s' by A10,A14,AFF_1:14;
then r',s' // a',b' by A15,AFF_1:14;
then r,s // a,b by Th48; then a,b _|_ a,b by A7,A9,Def9;
hence contradiction by A5,Def9; end;
then consider z' being Element of Af(POS) such that
A16: LIN p',y',z' & LIN
x',r',z' by A1,AFF_1:74; reconsider z=z' as Element of
the carrier of POS by Th47; A17: p',y' // p',z' & x',r' // x',z'
by A16,AFF_1:def 1;
then a',b' // p',z' by A15,AFF_1:14; then A18: a,b // p,z by Th48;
x,r // x,z by A17,Th48; then a,b _|_ x,z by A12,A14,Def9; then a,b _|_
p,z by A11,Def9; then p,z _|_ p,z by A5,A18,Def9; then x',r' // x',p'
by A17,Def9; then A19: LIN x',r',p' by AFF_1:def 1;
LIN x',r',x' & LIN x',p',q' by A8,AFF_1:15,16;
then LIN x',r',q' by A14,A19,AFF_1:20; then x',r' // p',q' by A19,AFF_1:19
;
then p',q' // r',s' by A10,A14,AFF_1:14; hence contradiction by A5,Th48
; end;
A20: now assume A21: x<>p & x<>s; consider y' being Element of
Af(POS) such that A22: a',b' // p',y' & p'<>y' by DIRAF:47;
not p',y' // x',s' proof assume not thesis;
then p',y' // r',s' by A10,A21,AFF_1:14;
then r',s' // a',b' by A22,AFF_1:14;
then r,s // a,b by Th48; then a,b _|_ a,b by A7,A9,Def9;
hence contradiction by A5,Def9; end;
then consider z' being Element of Af(POS) such that
A23: LIN p',y',z' & LIN
x',s',z' by A1,AFF_1:74; reconsider z=z' as Element of
the carrier of POS by Th47; A24: p',y' // p',z' & x',s' // x',z'
by A23,AFF_1:def 1;
then a',b' // p',z' by A22,AFF_1:14; then A25: a,b // p,z by Th48;
x,s // x,z by A24,Th48; then a,b _|_ x,z by A12,A21,Def9; then a,b _|_
p,z by A11,Def9; then p,z _|_ p,z by A5,A25,Def9; then x',s' // x',p'
by A24,Def9; then A26: LIN x',s',p' by AFF_1:def 1;
LIN x',s',x' & LIN x',p',q' by A8,AFF_1:15,16;
then LIN x',s',q' by A21,A26,AFF_1:20; then x',s' // p',q' by A26,AFF_1:19
;
then p',q' // r',s' by A10,A21,AFF_1:14; hence contradiction by A5,Th48
; end;
A27: now assume A28: x<>q & x<>r; consider y' being Element of
Af(POS) such that A29: a',b' // q',y' & q'<>y' by DIRAF:47;
not q',y' // x',r' proof assume not thesis;
then q',y' // r',s' by A10,A28,AFF_1:14;
then r',s' // a',b' by A29,AFF_1:14;
then r,s // a,b by Th48; then a,b _|_ a,b by A7,A9,Def9;
hence contradiction by A5,Def9; end;
then consider z' being Element of Af(POS) such that
A30: LIN q',y',z' & LIN
x',r',z' by A1,AFF_1:74; reconsider z=z' as Element of
the carrier of POS by Th47; A31: q',y' // q',z' & x',r' // x',z'
by A30,AFF_1:def 1;
then a',b' // q',z' by A29,AFF_1:14; then A32: a,b // q,z by Th48;
x,r // x,z by A31,Th48; then a,b _|_ x,z by A12,A28,Def9; then a,b _|_
q,z by A11,Def9; then q,z _|_ q,z by A5,A32,Def9; then x',r' // x',q'
by A31,Def9; then A33: LIN x',r',q' by AFF_1:def 1;
LIN x',r',x' & LIN x',q',p' by A8,AFF_1:15,16;
then LIN x',r',p' by A28,A33,AFF_1:20; then x',r' // p',q' by A33,AFF_1:19
;
then p',q' // r',s' by A10,A28,AFF_1:14; hence contradiction by A5,Th48
; end;
now assume A34: x<>q & x<>s; consider y' being Element of
Af(POS) such that A35: a',b' // q',y' & q'<>y' by DIRAF:47;
not q',y' // x',s' proof assume not thesis;
then q',y' // r',s' by A10,A34,AFF_1:14; then r',s' // a',b'
by A35,AFF_1:14;
then r,s // a,b by Th48; then a,b _|_ a,b by A7,A9,Def9;
hence contradiction by A5,Def9; end;
then consider z' being Element of Af(POS) such that
A36: LIN q',y',z' & LIN
x',s',z' by A1,AFF_1:74; reconsider z=z' as Element of
the carrier of POS by Th47; A37: q',y' // q',z' & x',s' // x',z'
by A36,AFF_1:def 1;
then a',b' // q',z' by A35,AFF_1:14; then A38: a,b // q,z by Th48;
x,s // x,z by A37,Th48; then a,b _|_ x,z by A12,A34,Def9; then a,b _|_
q,z by A11,Def9; then q,z _|_ q,z by A5,A38,Def9; then x',s' // x',q'
by A37,Def9; then A39: LIN x',s',q' by AFF_1:def 1;
LIN x',s',x' & LIN x',q',p' by A8,AFF_1:15,16;
then LIN x',s',p' by A34,A39,AFF_1:20; then x',s' // p',q' by A39,AFF_1:19
;
then p',q' // r',s' by A10,A34,AFF_1:14; hence contradiction by A5,Th48;
end;
hence contradiction by A6,A13,A20,A27,AFF_1:12; end; end;
hence POS is OrtAfPl by A1,A2,A3,Def10; 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 = Af(POS);
A1: P = AffinStruct(#the carrier of POS,the CONGR of POS#) by Def8;
hereby assume A2: POS is OrtAfPl-like;
then A3: P is AffinPlane by A1,Def10;
thus ex x,y being Element of POS st x<>y proof
consider a,b being Element of P such that
A4: a<>b by A3,DIRAF:54;
reconsider a'=a,b'=b as Element of POS by Th47; a'<>b' by A4
;
hence thesis; end;
let a,b,c,d,p,q,r,s be Element of POS;
reconsider a'=a,b'=b,c'=c,d'=d,p'=p,q'=q,r'=r,s'=s as Element of the carrier
of P by Th47;
a',b' // b',a' & a',b' // c',c' by A3,DIRAF:54;
hence a,b // b,a & a,b // c,c by Th48;
hereby assume a,b // p,q & a,b // r,s;
then a',b' // p',q' & a',b' // r',s' by Th48; then p',q' // r',s' or a'=b'
by A3,DIRAF:54;
hence p,q // r,s or a=b by Th48; end;
hereby assume a,b // a,c; then a',b' // a',c' by Th48; then b',a' // b',c'
by A3,DIRAF:54; hence b,a // b,c by Th48; end;
consider x' being Element of P such that
A5: a',b' // c',x' & a',c' // b',x' by A3,DIRAF:54;
reconsider x=x' as Element
of the carrier of POS by Th47;
a,b // c,x & a,c // b,x by A5,Th48;
hence ex x being Element of POS st
a,b // c,x & a,c // b,x;
consider x',y',z' being Element of the
carrier of P such that A6: not x',y' // x',z' by A3,DIRAF:54; reconsider
x=x',y=y',z=z' as Element of POS by Th47;
not x,y // x,z by A6,Th48;
hence ex x,y,z being Element of POS st not x,y // x,z;
consider x' being Element of P such that A7: a',b' // c',x' &
c'<>x' by A3,DIRAF:54; reconsider x=x' as Element of POS by
Th47;
a,b // c,x & c <>x by A7,Th48;
hence ex x being Element of POS st a,b // c,x & c <>x;
hereby assume a,b // b,d & b<>a; then a',b' // b',d' & b'<>a' by Th48;
then consider x' being Element of P such that
A8: c',b' // b',x' & c',a' // d',x' by A3,DIRAF:54; reconsider x=x' as
Element of POS by Th47; c,b // b,x & c,a // d,x by A8,Th48;
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 A2,Def10;
assume not a,b // c,d; then not a',b' // c',d' by Th48;
then consider x' being Element of the
carrier of P such that A9: a',b' // a',x' & c',d' // c',x' by A3,DIRAF:54;
reconsider x=x' as Element of POS by Th47;
a,b // a,x & c,d // c,x by A9,Th48; 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: ex x,y being Element of P st x<>y proof
reconsider a'=a,b'=b as Element of P by Th47; a'<>b' by A10
;
hence thesis; end;
A13: 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
by Th47;
thus x,y // y,x & x,y // z,z proof a,b // b,a & a,b // c,c by A11;
hence thesis by Th48; end;
thus x<>y & x,y // z,t & x,y // u,w implies z,t // u,w proof assume
x<>y & x,y // z,t & x,y // u,w; then a,b // c,d & a,b // e,f & a<>b by
Th48
;
then c,d // e,f by A11; hence z,t // u,w by Th48; end;
thus x,y // x,z implies y,x // y,z proof assume x,y // x,z; then a,b // a,
c
by Th48; then b,a // b,c by A11; hence y,x // y,z by Th48; end; end;
A14: 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
A15: not x,y // x,z by A11
; reconsider x'=x,y'=y,z'=z as Element of the carrier
of P by Th47; not x',y' // x',z' by A15,Th48; hence thesis; end;
A16: now let x,y,z be Element of P; reconsider
x'=x,y'=y,z'=z as Element of POS by Th47;
consider t' being Element of POS such that
A17: x',z' // y',t' & y'<>t' by A11
; reconsider t=t' as Element of the carrier
of P by Th47; x,z // y,t & y<>t by A17,Th48;
hence ex t being Element of P st x,z // y,t & y<>t; end;
A18: now let x,y,z be Element of P; reconsider
x'=x,y'=y,z'=z as Element of POS by Th47;
consider t' being Element of POS such that
A19: x',y' // z',t' & x',z' // y',t' by A11; reconsider t=t'
as Element of the
carrier of P by Th47; x,y // z,t & x,z // y,t by A19,Th48;
hence ex t being Element of P st x,y // z,t & x,z // y,t; end;
A20: now let x,y,z,t be Element of P such that
A21: z,x // x,t & x<>z; reconsider x'=x,y'=y,z'=z,t'=t as Element of the
carrier of POS by Th47; z',x' // x',t' & x'<>z' by A21,Th48;
then consider u'
being Element of POS such that A22: y',x' // x',u' &
y',z' // t',u' by A11; reconsider u=u' as Element of P
by Th47;
y,x // x,u & y,z // t,u by A22,Th48;
hence ex u being Element of P st y,x // x,u & y,z // t,u; end;
now let x,y,z,t be Element of P such that
A23: not x,y // z,t; reconsider x'=x,y'=y,z'=z,t'=t as Element of the
carrier of POS by Th47; not x',y' // z',t' by A23,Th48;
then consider u' being Element of the
carrier of POS such that A24: x',y' // x',u' & z',t' // z',u' by A11;
reconsider u=u' as Element of P by Th47;
x,y // x,u & z,t // z,u by A24,Th48;
hence ex u being Element of P st x,y // x,u & z,t // z,u; end;
hence AffinStruct(#the carrier of POS,the CONGR of POS#) is AffinPlane by A1,
A12,A13,A14,A16,A18,A20,DIRAF:54;
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 for a,b,c be Element of POS holds (
ex x being Element of POS st a,b _|_ c,x & c <>x) 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 :Def11:
a,b // a,c;
end;
definition let POS,a,b;
func Line(a,b) -> Subset of POS means
:Def12: 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_Ex;
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 x in the carrier of POS & 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 set holds x in X1 iff x in X2 proof let x be set;
thus x in X1 implies x in X2 proof assume A4:x in X1;
then reconsider x' = x as Element of POS;
LIN a,b,x' by A2,A4; hence thesis by A3; end;
assume A5: x in X2;
then reconsider x' = x as Element of POS;
LIN a,b,x' by A3,A5; hence thesis by A2; end;
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
:Def13: ex a,b st a<>b & A=Line(a,b);
synonym A is_line;
end;
canceled 3;
theorem
Th55: for POS being OrtAfSp for a,b,c being Element of POS,
a',b',c' being Element of Af(POS) st a=a'& b=b' & c = c' holds
(LIN a,b,c iff LIN a',b',c') proof let POS be OrtAfSp;
let a,b,c be Element of POS, a',b',c' be Element of the carrier
of Af(POS) such that A1: a=a'& b=b' & c = c';
hereby assume LIN a,b,c; then a,b // a,c by Def11; then a',b' // a',c'
by A1,Th48; hence LIN a',b',c' by AFF_1:def 1; end;
assume LIN a',b',c'; then a',b' // a',c' by AFF_1:def 1; then a,b // a,c
by A1,Th48; hence LIN a,b,c by Def11; end;
theorem
Th56: for POS being OrtAfSp for a,b being Element of POS,
a',b' being Element of Af(POS) st a=a' & b=b' holds
Line(a,b) = Line(a',b') proof let POS be OrtAfSp;
let a,b be Element of POS, a',b' be Element of the carrier
of Af(POS) such that A1: a=a' & b=b'; set X = Line(a,b), Y = Line(a',b');
now let x1 be set; A2: now assume A3: x1 in X; then reconsider x=x1 as
Element of POS; reconsider x'=x as Element of
the carrier of Af(POS) by Th47; LIN a,b,x by A3,Def12; then LIN a',b',x'
by A1,Th55; hence x1 in Y by AFF_1:def 2; end;
now assume A4: x1 in Y; then reconsider x'=x1 as Element of
Af(POS); reconsider x=x' as Element of POS by Th47
; LIN a',b',x' by A4,AFF_1:def 2; then LIN
a,b,x by A1,Th55;hence x1 in X by Def12; end; hence x1 in X iff x1 in Y by A2
; end;
hence thesis by TARSKI:2; end;
theorem
Th57: for X being set holds ( X is Subset of POS iff
X is Subset of Af(POS)) proof let X be set;
Af(POS) = AffinStruct(#the carrier of POS, the CONGR of POS#) by Def8;
hence thesis; end;
theorem
Th58: for POS being OrtAfSp for X being Subset of POS,
Y being Subset of Af(POS) st X=Y holds
( X is_line iff Y is_line) proof let POS be OrtAfSp; let X be Subset of the
carrier of POS, Y be Subset of Af(POS) such that A1: X=Y;
hereby assume X is_line; then consider a,b being Element of
POS
such that A2: a<>b & X = Line(a,b) by Def13; reconsider a'=a,b'=b as
Element of Af(POS) by Th47; Y = Line(a',b') by A1,A2,Th56;
hence Y is_line by A2,AFF_1:def 3; end;
assume Y is_line; then consider a',b' being Element of
Af(POS) such that A3: a'<>b' & Y = Line(a',b') by AFF_1:def 3; reconsider
a=a',b=b' as Element of POS by Th47; X = Line(a,b)
by A1,A3,Th56; hence X is_line by A3,Def13; end;
definition let POS; let a,b,K; pred a,b _|_ K means
:Def14: 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
:Def15: ex p,q st p<>q & K = Line(p,q) & p,q _|_ M; end;
definition let POS; let K,M; pred K // M means
:Def16: ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M = Line(c,d)
& a,b // c,d; end;
canceled 3;
theorem Th62:
(a,b _|_ K implies K is_line) & (K _|_ M implies (K is_line & M is_line))
proof A1: now let a,b,K; assume a,b _|_ K; then ex p,q st p<>q &
K = Line(p,q) & a,b _|_ p,q by Def14; hence K is_line by Def13; end;
now assume K _|_ M; then A2: ex p,q st p<>q & K = Line(p,q)
& p,q _|_ M by Def15; hence K is_line by Def13; thus M is_line
by A1,A2; end;
hence thesis by A1; end;
theorem Th63:
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 by Def15; ex c,d st c <>d &
M = Line(c,d) & a,b _|_ c,d by A2,Def14; 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,Def14; hence
K _|_ M by A3,A5,Def15;
end;
theorem Th64: for POS being OrtAfSp for M,N being Subset of POS,
M',N' being Subset of Af(POS) st M = M' & N = N' holds
(M // N iff M' // N')
proof let POS be OrtAfSp; let M,N be Subset of POS,
M',N' be Subset of Af(POS) such that A1: M = M' and A2: N = N';
hereby assume M // N;
then consider a,b,c,d being Element of POS
such that A3: a<>b & c <>d & M = Line(a,b) & N = Line(c,d) and A4: a,b // c,d
by Def16; reconsider a'=a,b'=b,c'=c,d'=d as Element of
Af(POS) by Th47; A5: M'=Line(a',b') by A1,A3,Th56;
A6: N'=Line(c',d') by A2,A3,Th56; a',b' // c',d'
by A4,Th48; hence M' // N' by A3,A5,A6,AFF_1:51; end;
assume M' // N';
then consider a',b',c',d' being Element of the carrier
of Af(POS) such that A7: a'<>b' & c'<>d' and A8: a',b' // c',d' and
A9: M' = Line(a',b') & N' = Line(c',d') by AFF_1:51;
reconsider a=a',b=b',c =c',d=d' as Element of POS by Th47;
A10: M=Line(a,b) by A1,A9,Th56; A11: N=Line(c,d) by A2,A9,Th56; a,b // c,d
by A8,Th48;
hence M // N by A7,A10,A11,Def16;
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_line implies a,a _|_ K proof assume K is_line; then consider p,q
such that A1: p<>q & K = Line(p,q) by Def13; p,q _|_ a,a by Def9;
then a,a _|_ p,q by Def9; hence thesis by A1,Def14; 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;
consider p,q such that A4: p<>q & K = Line(p,q) and A5: a,b _|_ p,q
by A1,Def14;
reconsider a'=a,b'=b,c'=c,d'=d as Element of Af(POS) by Th47;
a',b' // c',d' or c',d' // a',b' by A2,Th48; then a',b' // c',d' by AFF_1:13
;
then a,b // c,d by Th48; then p,q _|_ c,d by A3,A5,Def9; then c,d _|_ p,q
by Def9; hence thesis by A4,Def14; 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 by Def14; p,q _|_ a,b by A2,Def9
; then p,q _|_ b,a by Def9; then b,a _|_ p,q by Def9; hence thesis
by A1,Def14; end;
theorem Th68:
K // M implies M // K proof 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 by Def16;
reconsider a'=a,b'=b,c'=c,d'=d as Element of Af(POS) by Th47;
a',b' // c',d' by A2,Th48; then c',d' // a',b' by AFF_1:13; then c,d // a,b
by Th48; hence thesis by A1,Def16; end;
theorem Th69:
r,s _|_ K & (K // M or M // K) implies r,s _|_ M proof assume that A1: r,s _|_
K and
A2: K // M or M // K; A3: K // M by A2,Th68; consider p,q such that
A4: p<>q & K = Line(p,q) & r,s _|_ p,q by A1,Def14; consider a,b,c,d such
that A5: a<>b & c <>d and A6: K = Line(a,b) and A7: M = Line(c,d) & a,b // c,d
by A3,Def16; reconsider p'=p,q'=q,a'=a,b'=b,c'=c,d'=d as Element of the
carrier of Af(POS) by Th47; A8: K = Line(a',b') & K = Line(p',q')
by A4,A6,Th56; then p' in K & q' in K by AFF_1:26; then LIN a',b',p' & LIN
a',b',q'
by A8,AFF_1:def 2; then A9: a',b' // p',q' by AFF_1:19; a',b' // c',d'
by A7,Th48; then p',q' // c',d' by A5,A9,AFF_1:14;
then A10: p,q // c,d by Th48;
p,q _|_ r,s by A4,Def9; then r,s _|_ c,d by A4,A10,Def9;
hence thesis by A5,A7,Def14; end;
theorem Th70:
K _|_ M implies M _|_ K proof 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 by Th63;
c,d _|_ a,b by A2,Def9; hence thesis by A1,Th63; end;
definition let POS be OrtAfSp; let K,M be Subset of POS;
redefine pred K // M;
symmetry by Th68;
redefine pred K _|_ M;
symmetry by Th70;
end;
theorem Th71:
a in K & b in K & a,b _|_ K implies a=b proof assume that A1: a in K & b in
K and
A2: a,b _|_ K; consider p,q such that A3: p<>q & K = Line(p,q) & a,b _|_ p,q
by A2,Def14; reconsider a'=a,b'=b,p'=p,q'=q as Element of
Af(POS) by Th47; set K' = Line(p',q');
a' in K' & b' in K' by A1,A3,Th56
; then LIN p',q',a' & LIN p',q',b' by AFF_1:def 2;
then p',q' // a',b' by AFF_1:19; then A4: p,q // a,b by Th48; p,q _|_ a,b
by A3,Def9; then a,b _|_ a,b by A3,A4,Def9; hence thesis by Def9; end;
theorem Th72:
not K _|_ K proof
assume not thesis;
then consider a,b such that A1: a<>b & K = Line(a,b) & a,b _|_ K
by Def15; reconsider a'=a,b'=b as Element of Af(POS)
by Th47; K = Line(a',b') by A1,Th56; then a in K & b in K by AFF_1:26;
hence contradiction by A1,Th71; end;
theorem Th73:
(K _|_ M or M _|_ K) & (K // N or N // K) implies (M _|_ N & N _|_ M)
proof assume that A1: K _|_ M or M _|_ K and A2: K // N or N // K;
M _|_ K by A1; then consider r,s such that
A3: r<>s & M = Line(r,s) & r,s _|_ K by Def15; r,s _|_ N by A2,A3,Th69;
hence M _|_ N by A3,Def15; hence N _|_ M; end;
theorem Th74:
K // N implies not K _|_ N proof assume A1: K // N; assume not thesis;
then K _|_ K by A1,Th73;
hence contradiction by Th72; 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 & b in
K and A2: c,d _|_ K; consider p,q such that
A3: p<>q & K = Line(p,q) & c,d _|_ p,q by A2,Def14; reconsider a'=a,b'=b,
p'=p,q'=q as Element of Af(POS) by Th47; LIN p,q,a & LIN p,q,
b
by A1,A3,Def12; then LIN p',q',a' & LIN p',q',b' by Th55; then p',q' // a',
b'
by AFF_1:19; then A4: p,q // a,b by Th48; p,q _|_ c,d by A3,Def9; hence
c,d _|_ a,b by A3,A4,Def9; hence thesis by Def9; end;
theorem Th76: a in K & b in K & a<>b & K is_line implies K =Line(a,b)
proof assume that A1: a in K & b in K and A2: a<>b and A3: K is_line;
reconsider K'=K as Subset of Af(POS) by Th57;
reconsider a'=a,b'=b as Element of Af(POS) by Th47;
K' is_line by A3,Th58; then K' = Line(a',b')
by A1,A2,AFF_1:71; hence K = Line(a,b) by Th56; end;
theorem
a in K & b in
K & a<>b & K is_line & (a,b _|_ c,d or c,d _|_ a,b) implies c,d _|_ K
proof assume that A1: a in K & b in K & a<>b & K is_line and
A2: a,b _|_ c,d or c,d _|_ a,b; A3: c,d _|_ a,b by A2,Def9;
K = Line(a,b) by A1,Th76; hence thesis by A1,A3,Def14; end;
theorem Th78: 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 & b in M and A2: c in N & d in N and A3: M _|_ N;
consider p1,q1,p2,q2 being Element of POS such that
A4: p1<>q1 & p2<>q2 and A5: M = Line(p1,q1) & N = Line(p2,q2) & p1,q1 _|_
p2,q2
by A3,Th63; reconsider a'=a,b'=b,c'=c,d'=d,p1'=p1,q1'=q1,p2'=p2,q2'=q2
as Element of Af(POS) by Th47;
LIN p1,q1,a & LIN p1,q1,b & LIN p2,q2,c & LIN p2,q2,d by A1,A2,A5,Def12;
then LIN p1',q1',a' & LIN p1',q1',b' & LIN p2',q2',c' & LIN
p2',q2',d' by Th55;
then p1',q1' // a',b' & p2',q2' // c',d' by AFF_1:19;
then A6: p1,q1 // a,b & p2,q2 // c,d by Th48; then p2,q2 _|_ a,b by A4,A5,Def9
;
hence thesis by A4,A6,Def9; 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_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 & A _|_ N and A5: K is_line;
A6: K = Line(a,b) by A2,A3,A5,Th76; A is_line by A4,Th62;
then consider q,r such that A7: q<>r & A = Line(q,r) by Def13;
reconsider q'=q,r'=r as Element of Af(POS) by Th47;
Line(q,r) = Line(q',r') by Th56;
then q in A & r in A by A7,AFF_1:26
; then q,r _|_ p,a & q,r _|_ p,b by A1,A4,Th78;
then q,r _|_ a,b by Def9; hence A _|_ K by A2,A6,A7,Th63; end;
theorem Th80:
b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c
proof thus b,c _|_ a,a by Def9; hence a,a _|_ b,c by Def9;
reconsider a'=a,b'=b,c'=c as Element of Af(POS) by Th47;
b',c' // a',a' & a',a' // b',c' by AFF_1:12; hence thesis by Th48; end;
theorem Th81:
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; reconsider a'=a,b'=b,c'= c,d'=d as Element of the
carrier of Af(POS) by Th47; a',b' // c',d' by A1,Th48; then 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' by AFF_1:13; hence thesis by Th48; 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 p'=p,q'=q,a'=a, b'=b,c'= c,d'=d as Element of the carrier
of Af(POS) by Th47; (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') by A2,Th48; then a',b' // c',d' by A1,AFF_1:14;
hence thesis by Th48; end;
theorem Th83:
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 Def9; then A2: d,c _|_ a,b
by Def9; then d,c _|_ b,a by Def9; then b,a _|_ d,c by Def9;
then b,a _|_ c,d by Def9;
hence thesis by A1,A2,Def9; end;
theorem Th84:
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 Th81,Th83; then c,d _|_ a,b by A1,Def9;
hence a,b _|_ c,d by Th83; 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 Th81,Th83; hence a,b _|_ c,d by A1,Def9;
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 Th85:
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,Th83; hence thesis by A1,Def10; end;
theorem
a in M & b in M & a<>b & M is_line & c in N & d in N & c <>d & N is_line &
a,b // c,d implies M // N
proof assume that A1: a in M & b in M & a<>b & M is_line and
A2: c in N & d in N & c <>d & N is_line and A3: a,b // c,d;
M = Line(a,b) & N = Line(c,d) by A1,A2,Th76;
hence thesis by A1,A2,A3,Def16; end;
theorem (K _|_ M or M _|_ K) & (K _|_ N or N _|_ K) implies (M // N & N // M
)
proof assume that A1: K _|_ M or M _|_ K and A2: K _|_ N or N _|_ K; A3: K _|_
M & K _|_ N
by A1,A2; then consider p1,q1,a,b being Element of POS such
that A4: p1<>q1 & a<>b & K = Line(p1,q1) & M = Line(a,b) and A5: p1,q1 _|_ a,b
by Th63; consider p2,q2,c,d being Element of POS such that
A6: p2<>q2 & c <>d & K = Line(p2,q2) & N = Line(c,d) and A7: p2,q2 _|_ c,d
by A3,Th63; reconsider p1'=p1,p2'=p2,q1'=q1,q2'=q2 as Element of the carrier
of Af(POS) by Th47; Line(p1',q1') = Line(p2,q2)
by A4,A6,Th56 .= Line(p2',q2') by Th56; then p2' in Line(p1',q1') &
q2' in Line(p1',q1') by AFF_1:26; then LIN p1',q1',p2' & LIN p1',q1',q2'
by AFF_1:def 2; then p1',q1' // p2',q2' by AFF_1:19; then p1,q1 // p2,q2
by Th48; then a,b _|_ p2,q2 by A4,A5,Th84; then a,b // c,d by A6,A7,Th85;
hence M // N by A4,A6,Def16; hence N // M; end;
theorem Th88: M _|_ N implies ex p st p in M & p in N
proof assume A1: M _|_ N;
then A2: not M // N by Th74;
reconsider M'=M,N'=N as Subset of Af(POS) by Th57;
M is_line & N is_line by A1,Th62; then A3: M' is_line & N' is_line by Th58;
not M' // N' by A2,Th64; then consider p' being Element of
Af(POS) such that A4: p' in M' & p' in N' by A3,AFF_1:72; thus thesis by A4;
end;
theorem Th89: a,b _|_ c,d implies ex p st LIN a,b,p & LIN c,d,p
proof assume A1: a,b _|_ c,d; reconsider a'=a,b'=b,c'=c,d'=d as Element of the
carrier of Af(POS) by Th47; LIN c',d',c' & LIN a',b',a' by AFF_1:16;
then A2: LIN c,d,c & LIN a,b,a by Th55;
A3: now assume a=b; then a,b // a,c by Th80; then LIN a,b,c by Def11; hence
ex p st LIN a,b,p & LIN c,d,p by A2; end;
A4: now assume c =d; then c,d // c,a by Th80; then LIN c,d,a by Def11;
hence
ex p st LIN a,b,p & LIN c,d,p by A2; end;
now assume A5: a<>b & c <>d;
set M = Line(a,b),N = Line(c,d); M _|_ N by A1,A5,Th63; then consider p
such
that A6: p in M & p in N by Th88;
LIN a,b,p & LIN c,d,p by A6,Def12; hence ex p st LIN a,b,p & LIN c,d,p;
end
;
hence thesis by A3,A4; 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 A1: p<>q & K = Line(p,q) &
a,b _|_ p,q by Def14; consider c such that A2: LIN a,b,c & LIN
p,q,c by A1,Th89;
c in K by A1,A2,Def12; hence thesis by A2; end;
theorem Th91: ex x st a,x _|_ p,q & LIN p,q,x
proof A1: now assume p=q; then A2: p,q // p,a & a,a _|_ p,q by Th80; take x=a;
thus a,x _|_ p,q & LIN p,q,x by A2,Def11; end;
now assume p<>q; then consider x such that
A3: p,q // p,x & p,q _|_ x,a by Def9; take x; thus
a,x _|_ p,q & LIN p,q,x by A3,Def11,Th83; end;
hence thesis by A1; end;
theorem K is_line implies ex x st a,x _|_ K & x in K
proof assume K is_line; then consider p,q such that A1: p<>q & K = Line(p,q)
by Def13; consider x such that A2: a,x _|_ p,q and A3: LIN p,q,x by Th91;
take x; thus a,x _|_ K by A1,A2,Def14; thus x in K by A1,A3,Def12; end;