ANALOAF

:: Analytical Ordered Affine Spaces
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 11, 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, CARD_1, ARYTM_3, RELAT_1, ARYTM_1,
      SUPINF_2, STRUCT_0, ZFMISC_1, XBOOLE_0, SUBSET_1, ANALOAF;
 notations TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, DOMAIN_1, XXREAL_0, XCMPLX_0,
      XREAL_0, REAL_1, RELSET_1, NUMBERS, STRUCT_0, RLVECT_1;
 constructors XXREAL_0, REAL_1, MEMBERED, DOMAIN_1, RLVECT_1;
 registrations SUBSET_1, RELSET_1, XXREAL_0, STRUCT_0, ZFMISC_1, XREAL_0,
      ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 equalities RLVECT_1;
 theorems RLVECT_1, RELAT_1, FUNCSDOM, RLSUB_2, XCMPLX_0, XCMPLX_1, XREAL_1,
      STRUCT_0, XTUPLE_0;
 schemes RELSET_1;

begin

reserve V for RealLinearSpace;
reserve p,q,u,v,w,y for VECTOR of V;
reserve a,b,c,d for Real;

definition
  let V;
  let u,v,w,y;
  pred u,v // w,y means

  u=v or w=y or ex a,b st 0<a & 0<b & a*(v-u)=b*( y-w);
end;

theorem Th1:
  (w-v)+(v-u) = w-u
proof
  thus (w-v)+(v-u) = w-(v-(v-u)) by RLVECT_1:29
    .= w-((v-v)+u) by RLVECT_1:29
    .= w-(0.V+u) by RLVECT_1:15
    .= w-u by RLVECT_1:4;
end;

theorem Th2:
  y+u = v+w implies y-w = v-u
proof
  assume
A1: y+u=v+w;
  thus y-w = (y+0.V)-w by RLVECT_1:4
    .= (y+(u-u))-w by RLVECT_1:15
    .=((v+w)+(-u))-w by A1,RLVECT_1:def 3
    .= (-u)+((v+w)-w) by RLVECT_1:def 3
    .= v-u by RLSUB_2:61;
end;

theorem Th3:
  a*(u-v) = -(a*(v-u))
proof
  a*(v-u) + a*(u-v) = a*(v-u) + a*(-(v-u)) by RLVECT_1:33
    .= a*(v-u)-a*(v-u) by RLVECT_1:25
    .= 0.V by RLVECT_1:15;
  hence thesis by RLVECT_1:def 10;
end;

theorem Th4:
  (a-b)*(u-v) = (b-a)*(v-u)
proof
  thus (a-b)*(u-v)=(-(b-a))*(-(v-u)) by RLVECT_1:33
    .=(b-a)*(v-u) by RLVECT_1:26;
end;

theorem Th5:
  a<>0 & a*u=v implies u=a"*v
proof
  assume that
A1: a<>0 and
A2: a*u=v;
  thus u=1*u by RLVECT_1:def 8
    .=(a"*a)*u by A1,XCMPLX_0:def 7
    .=a"*v by A2,RLVECT_1:def 7;
end;

theorem Th6:
  (a<>0 & a*u=v implies u=a"*v) & (a<>0 & u=a"*v implies a*u=v)
proof
  now
    assume a<>0 & u=a"*v;
    hence v=(a")"*u by Th5,XCMPLX_1:202
      .=a*u;
  end;
  hence thesis by Th5;
end;

theorem
  u,v // w,y & u<>v & w<>y implies ex a,b st a*(v-u)=b*(y-w) & 0<a & 0<b;

reconsider jj=1 as Real;

theorem Th8:
  u,v // u,v
proof
  jj*(v-u)=jj*(v-u);
  hence thesis;
end;

theorem
  u,v // w,w & u,u // v,w;

theorem Th10:
  u,v // v,u implies u=v
proof
  assume
A1: u,v // v,u;
  assume
A2: u<>v;
  then consider a,b such that
A3: a*(v-u)=b*(u-v) and
A4: 0<a & 0<b by A1;
  a*(v-u)=-b*(v-u) by A3,Th3;
  then b*(v-u)+a*(v-u)=0.V by RLVECT_1:5;
  then (b+a)*(v-u)=0.V by RLVECT_1:def 6;
  then v-u=0.V or b+a=0 by RLVECT_1:11;
  then 0.V=(-u)+v by A4;
  then v=-(-u) by RLVECT_1:def 10
    .=u by RLVECT_1:17;
  hence contradiction by A2;
end;

theorem Th11:
  p<>q & p,q // u,v & p,q // w,y implies u,v // w,y
proof
  assume that
A1: p<>q and
A2: p,q // u,v and
A3: p,q // w,y;
  now
    assume that
A4: u<>v and
A5: w<>y;
    consider a,b such that
A6: a*(q-p)=b*(v-u) and
A7: 0<a and
A8: 0<b by A1,A2,A4;
    0<a" by A7;
    then
A9: 0<a"*b by A8,XREAL_1:129;
    consider c,d such that
A10: c*(q-p)=d*(y-w) and
A11: 0<c and
A12: 0<d by A1,A3,A5;
A13: q-p=(c")*(d*(y-w)) by A10,A11,Th6
      .=(c"*d)*(y-w) by RLVECT_1:def 7;
    0<c" by A11;
    then
A14: 0<c"*d by A12,XREAL_1:129;
    q-p=(a")*(b*(v-u)) by A6,A7,Th6
      .=(a"*b)*(v-u) by RLVECT_1:def 7;
    hence thesis by A13,A9,A14;
  end;
  hence thesis;
end;

theorem Th12:
  u,v // w,y implies v,u // y,w & w,y // u,v
proof
  assume
A1: u,v // w,y;
  now
    assume u<>v & w<>y;
    then consider a,b such that
A2: a*(v-u)=b*(y-w) and
A3: 0<a & 0<b by A1;
    a*(u-v)=-b*(y-w) by A2,Th3
      .=b*(w-y) by Th3;
    hence thesis by A2,A3;
  end;
  hence thesis;
end;

theorem Th13:
  u,v // v,w implies u,v // u,w
proof
  assume
A1: u,v // v,w;
  now
    assume u<>v & v<>w;
    then consider a,b such that
A2: a*(v-u)=b*(w-v) and
A3: 0<a and
A4: 0<b by A1;
A5: 0<a+b by A3,A4;
    b*(w-u)=b*((w-v)+(v-u)) by Th1
      .=a*(v-u)+b*(v-u) by A2,RLVECT_1:def 5
      .=(a+b)*(v-u) by RLVECT_1:def 6;
    hence thesis by A4,A5;
  end;
  hence thesis by Th8;
end;

theorem Th14:
  u,v // u,w implies u,v // v,w or u,w // w,v
proof
  assume
A1: u,v // u,w;
  now
    assume u<>v & u<>w;
    then consider a,b such that
A2: a*(v-u)=b*(w-u) and
A3: 0<a and
A4: 0<b by A1;
    w-v=(w-u)+(u-v) by Th1
      .=(w-u)-(v-u) by RLVECT_1:33;
    then
A5: a*(w-v)=a*(w-u)-b*(w-u) by A2,RLVECT_1:34
      .=(a-b)*(w-u) by RLVECT_1:35
      .=(b-a)*(u-w) by Th4;
    v-w=(v-u)+(u-w) by Th1
      .=(v-u)-(w-u) by RLVECT_1:33;
    then
A6: b*(v-w)=b*(v-u)-a*(v-u) by A2,RLVECT_1:34
      .=(b-a)*(v-u) by RLVECT_1:35
      .=(a-b)*(u-v) by Th4;
A7: now
      assume a<>b;
      then 0<a-b or 0<b-a by XREAL_1:55;
      then v,u // w,v or w,u // v,w by A3,A4,A6,A5;
      hence thesis by Th12;
    end;
    now
      assume a=b;
      then (-u)+v= (-u)+w by A2,A3,RLVECT_1:36;
      then v=w by RLVECT_1:8;
      hence thesis;
    end;
    hence thesis by A7;
  end;
  hence thesis;
end;

theorem Th15:
  v-u=y-w implies u,v // w,y
proof
  assume v-u=y-w;
  then jj*(v-u)=jj*(y-w);
  hence thesis;
end;

theorem Th16:
  y=(v+w)-u implies u,v // w,y & u,w // v,y
proof
  set y=(v+w)-u;
  y+u=v+w by RLSUB_2:61;
  then y-v=w-u & y-w=v-u by Th2;
  hence thesis by Th15;
end;

theorem Th17:
  (ex p,q st p<>q) implies for u,v,w ex y st u,v // w,y & u,w // v ,y & v<>y
proof
  given p,q such that
A1: p<>q;
  let u,v,w;
A2: now
    assume
A3: u<>w;
    take y=(v+w)-u;
A4: now
      assume v=y;
      then v=v+(w-u) by RLVECT_1:def 3;
      then w-u=0.V by RLVECT_1:9;
      hence contradiction by A3,RLVECT_1:21;
    end;
    u,v // w,y & u,w // v,y by Th16;
    hence thesis by A4;
  end;
  now
    assume
A5: u=w;
A6: now
      assume u=v;
      then
A7:   u,v // w,p & u,v // w,q;
A8:   v<>p or v<>q by A1;
      u,w // v,p & u,w // v,q by A5;
      hence thesis by A8,A7;
    end;
    u,v // w,u & u,w // v,u by A5;
    hence thesis by A6;
  end;
  hence thesis by A2;
end;

theorem Th18:
  p<>v & v,p // p,w implies ex y st u,p // p,y & u,v // w,y
proof
  assume
A1: p<>v & v,p // p,w;
A2: now
    assume p<>w;
    then consider a,b such that
A3: a*(p-v)=b*(w-p) and
A4: 0<a and
A5: 0<b by A1;
    set y=(b"*a)*(p-u)+p;
A6: y-p=(b"*a)*(p-u) by RLSUB_2:61
      .=b"*(a*(p-u)) by RLVECT_1:def 7;
A7: y-w=(y-p)+(p-w) by Th1
      .=(y-p)-(w-p) by RLVECT_1:33;
    v-u=(p-u)+(v-p) by Th1
      .=(p-u)-(p-v) by RLVECT_1:33;
    then a*(v-u)=a*(p-u)-a*(p-v) by RLVECT_1:34
      .=b*(y-p)-b*(w-p) by A3,A5,A6,Th6
      .=b*(y-w) by A7,RLVECT_1:34;
    then
A8: u,v // w,y by A4,A5;
    0<b" by A5;
    then
A9: 0<b"*a by A4,XREAL_1:129;
    jj*(y-p)=y-p by RLVECT_1:def 8
      .=(b"*a)*(p-u) by RLSUB_2:61;
    then u,p // p,y by A9;
    hence thesis by A8;
  end;
  now
    assume
A10: p=w;
    take y=p;
    thus u,p // p,y & u,v // w,y by A10;
  end;
  hence thesis by A2;
end;

theorem Th19:
  (for a,b st a*u + b*v=0.V holds a=0 & b=0) implies u<>v & u<>0.V & v<>0.V
proof
  assume
A1: for a,b st a*u + b*v=0.V holds a=0 & b=0;
  thus u<>v
  proof
    assume u=v;
    then u - v = 0.V by RLVECT_1:15;
    then 1*u + (-v) = 0.V by RLVECT_1:def 8;
    then 1*u + ((-jj)*v) = 0.V by RLVECT_1:16;
    hence contradiction by A1;
  end;
  thus u<>0.V
  proof
    assume u=0.V;
    then 1*u = 0.V by RLVECT_1:10;
    then 1*u + 0.V = 0.V by RLVECT_1:4;
    then jj*u + 0*v =0.V by RLVECT_1:10;
    hence contradiction by A1;
  end;
  thus v<>0.V
  proof
    assume v=0.V;
    then 1*v = 0.V by RLVECT_1:10;
    then 0.V + 1*v = 0.V by RLVECT_1:4;
    then 0*u + jj*v =0.V by RLVECT_1:10;
    hence contradiction by A1;
  end;
end;

theorem Th20:
  (ex u,v st (for a,b st a*u + b*v=0.V holds a=0 & b=0)) implies
  ex u,v,w,y st not u,v // w,y & not u,v // y,w
proof
  given u,v such that
A1: for a,b st a*u + b*v=0.V holds a=0 & b=0;
A2: u<>0.V & v<>0.V by A1,Th19;
A3: not 0.V,u // v,0.V
  proof
A4: now
      given a,b such that
A5:   0<a and
      0<b and
A6:   a*(u-0.V) = b*(0.V-v);
      a*u = a*(u-0.V) & b*(0.V-v)=b*(-v) by RLVECT_1:13,14;
      then a*u = -(b*v) by A6,RLVECT_1:25;
      then a*u + b*v = 0.V by RLVECT_1:5;
      hence contradiction by A1,A5;
    end;
    assume 0.V,u // v,0.V;
    hence contradiction by A2,A4;
  end;
  not 0.V,u // 0.V,v
  proof
A7: now
      given a,b such that
A8:   0<a and
      0<b and
A9:   a*(u-0.V) = b*(v-0.V);
      a*u = a*(u-0.V) & b*(v-0.V)=b*v by RLVECT_1:13;
      then 0.V = a*u - (b*v) by A9,RLVECT_1:15
        .= a*u + (b*(-v)) by RLVECT_1:25
        .= a*u + ((-b)*v) by RLVECT_1:24;
      hence contradiction by A1,A8;
    end;
    assume 0.V,u // 0.V,v;
    hence contradiction by A2,A7;
  end;
  hence thesis by A3;
end;

Lm1: a*(v-u) = b*(w-y) & (a<>0 or b<>0) implies u,v // w,y or u,v // y,w
proof
  assume that
A1: a*(v-u) = b*(w-y) and
A2: a<>0 or b<>0;
A3: now
    assume
A4: b=0;
    then 0.V = a*(v-u) by A1,RLVECT_1:10;
    then v-u = 0.V by A2,A4,RLVECT_1:11;
    then u=v by RLVECT_1:21;
    hence u,v // w,y;
  end;
A5: now
A6: now
A7:   a*(v-u) = -(-(b*(w-y))) by A1,RLVECT_1:17
        .= -(b*(-(w-y))) by RLVECT_1:25
        .= -(b*(y-w)) by RLVECT_1:33
        .= b*(-(y-w)) by RLVECT_1:25
        .= (-b)*(y-w) by RLVECT_1:24;
      assume that
A8:   0<a and
A9:   b<0;
      0<-b by A9,XREAL_1:58;
      hence u,v // w,y by A8,A7;
    end;
A10: now
A11:  (-a)*(v-u) = a*(-(v-u)) by RLVECT_1:24
        .= -(b*(w-y)) by A1,RLVECT_1:25
        .=b*(-(w-y)) by RLVECT_1:25
        .= b*(y-w) by RLVECT_1:33;
      assume that
A12:  a<0 and
A13:  0<b;
      0<-a by A12,XREAL_1:58;
      hence u,v // w,y by A13,A11;
    end;
A14: now
      assume a<0 & b<0;
      then
A15:  0<-a & 0<-b by XREAL_1:58;
      (-a)*(v-u) = a*(-(v-u)) by RLVECT_1:24
        .= -(b*(w-y)) by A1,RLVECT_1:25
        .=b*(-(w-y)) by RLVECT_1:25
        .= (-b)*(w-y) by RLVECT_1:24;
      hence u,v // y,w by A15;
    end;
    assume a<>0 & b<>0;
    hence thesis by A1,A14,A10,A6;
  end;
  now
    assume
A16: a=0;
    then 0.V = b*(w-y) by A1,RLVECT_1:10;
    then w-y = 0.V by A2,A16,RLVECT_1:11;
    then w=y by RLVECT_1:21;
    hence u,v // w,y;
  end;
  hence thesis by A3,A5;
end;

theorem Th21:
  (ex p,q st (for w ex a,b st a*p + b*q=w)) implies for u,v,w,y st
not u,v // w,y & not u,v // y,w ex z being VECTOR of V st (u,v // u,z or u,v //
  z,u) & (w,y // w,z or w,y // z,w)
proof
  given p,q such that
A1: for w ex a,b st a*p + b*q=w;
  let u,v,w,y such that
A2: not u,v // w,y and
A3: not u,v // y,w;
  consider r1,s1 being Real such that
A4: r1*p + s1*q = v-u by A1;
  consider r2,s2 being Real such that
A5: r2*p + s2*q = y-w by A1;
  set r = r1*s2 - r2*s1;
A6: now
    assume
A7: r = 0;
A8: now
      assume that
A9:   r1<>0 and
A10:  r2=0;
      s2<>0
      proof
        assume s2=0;
        then y-w = 0.V + 0*q by A5,A10,RLVECT_1:10
          .= 0.V + 0.V by RLVECT_1:10
          .= 0.V by RLVECT_1:4;
        then y=w by RLVECT_1:21;
        hence contradiction by A2;
      end;
      hence contradiction by A7,A9,A10,XCMPLX_1:6;
    end;
A11: now
      assume
A12:  r1=0;
A13:  s1<>0
      proof
        assume s1=0;
        then v-u = 0.V + 0*q by A4,A12,RLVECT_1:10
          .= 0.V + 0.V by RLVECT_1:10
          .= 0.V by RLVECT_1:4;
        then u=v by RLVECT_1:21;
        hence contradiction by A2;
      end;
      then
A14:  r2=0 by A7,A12,XCMPLX_1:6;
A15:  s2<>0
      proof
        assume s2=0;
        then y-w = 0.V + 0*q by A5,A14,RLVECT_1:10
          .= 0.V + 0.V by RLVECT_1:10
          .= 0.V by RLVECT_1:4;
        then y=w by RLVECT_1:21;
        hence contradiction by A2;
      end;
      y-w = 0.V + s2*q by A5,A14,RLVECT_1:10
        .= s2*q by RLVECT_1:4;
      then
A16:  (s2)"*(y-w) = ((s2)"*s2)*q by RLVECT_1:def 7
        .= 1*q by A15,XCMPLX_0:def 7
        .= q by RLVECT_1:def 8;
      v-u = 0.V + s1*q by A4,A12,RLVECT_1:10
        .= s1*q by RLVECT_1:4;
      then
A17:  (s1)"*(v-u) = ((s1)"*s1)*q by RLVECT_1:def 7
        .= 1*q by A13,XCMPLX_0:def 7
        .= q by RLVECT_1:def 8;
      s1"<>0 by A13,XCMPLX_1:202;
      hence contradiction by A2,A3,A17,A16,Lm1;
    end;
A18: now
      assume that
A19:  r1<>0 and
A20:  r2<>0 and
A21:  s1 = 0;
      v-u = r1*p + 0.V by A4,A21,RLVECT_1:10
        .= r1*p by RLVECT_1:4;
      then
A22:  (r1)"*(v-u) = ((r1)"*r1)*p by RLVECT_1:def 7
        .= 1*p by A19,XCMPLX_0:def 7
        .= p by RLVECT_1:def 8;
      s2 = 0 by A7,A19,A21,XCMPLX_1:6;
      then y-w = r2*p + 0.V by A5,RLVECT_1:10
        .= r2*p by RLVECT_1:4;
      then
A23:  (r2)"*(y-w) = ((r2)"*r2)*p by RLVECT_1:def 7
        .= 1*p by A20,XCMPLX_0:def 7
        .= p by RLVECT_1:def 8;
      r1"<>0 by A19,XCMPLX_1:202;
      hence contradiction by A2,A3,A22,A23,Lm1;
    end;
    now
      assume that
A24:  r1<>0 and
      r2<>0 and
      s1<>0 and
      s2<>0;
      r2*(v-u) = r2*(r1*p) + r2*(s1*q) by A4,RLVECT_1:def 5
        .=(r2*r1)*p + r2*(s1*q) by RLVECT_1:def 7
        .= (r1*r2)*p + (r1*s2)*q by A7,RLVECT_1:def 7
        .= r1*(r2*p) + (r1*s2)*q by RLVECT_1:def 7
        .= r1*(r2*p) + r1*(s2*q) by RLVECT_1:def 7
        .= r1*(y-w) by A5,RLVECT_1:def 5;
      hence contradiction by A2,A3,A24,Lm1;
    end;
    hence contradiction by A7,A11,A8,A18,XCMPLX_1:6;
  end;
  consider r3,s3 being Real such that
A25: r3*p + s3*q = u-w by A1;
  set a= r2*s3 - r3*s2, b= r1*s3 - r3*s1;
A26: b*r2 = r1*a + r3*r;
  set z = u + (r"*a)*(v-u);
A27: r*(z-u) = r*z - r*u by RLVECT_1:34
    .= r*u + r*((r"*a)*(v-u)) - r*u by RLVECT_1:def 5
    .= r*u + (r*(r"*a))*(v-u) - r*u by RLVECT_1:def 7
    .= r*u + ((r*r")*a)*(v-u) - r*u
    .= r*u + (1*a)*(v-u) - r*u by A6,XCMPLX_0:def 7
    .= a*(v-u) + (r*u - r*u) by RLVECT_1:def 3
    .= a*(v-u) + 0.V by RLVECT_1:15
    .= a*(v-u) by RLVECT_1:4;
A28: r*(z-w) = r*z - r*w by RLVECT_1:34
    .= r*u + r*((r"*a)*(v-u)) - r*w by RLVECT_1:def 5
    .= r*u + (r*(r"*a))*(v-u) - r*w by RLVECT_1:def 7
    .= r*u + ((r*r")*a)*(v-u) - r*w
    .= r*u + (1*a)*(v-u) - r*w by A6,XCMPLX_0:def 7
    .= a*(v-u) + (r*u - r*w) by RLVECT_1:def 3
    .= a*(r1*p + s1*q) + r*(r3*p + s3*q) by A4,A25,RLVECT_1:34
    .= a*(r1*p) + a*(s1*q) + r*(r3*p + s3*q) by RLVECT_1:def 5
    .= a*(r1*p) + a*(s1*q) + (r*(r3*p) + r*(s3*q)) by RLVECT_1:def 5
    .= (a*r1)*p + a*(s1*q) + (r*(r3*p) + r*(s3*q)) by RLVECT_1:def 7
    .= (a*r1)*p + (a*s1)*q + (r*(r3*p) + r*(s3*q)) by RLVECT_1:def 7
    .= (a*r1)*p + (a*s1)*q + ((r*r3)*p + r*(s3*q)) by RLVECT_1:def 7
    .= (a*r1)*p + (a*s1)*q + ((r*s3)*q + (r*r3)*p) by RLVECT_1:def 7
    .= (a*r1)*p + (a*s1)*q + (r*s3)*q + (r*r3)*p by RLVECT_1:def 3
    .= ((a*s1)*q + (r*s3)*q) + (a*r1)*p + (r*r3)*p by RLVECT_1:def 3
    .= ((a*s1)*q + (r*s3)*q) + ((a*r1)*p + (r*r3)*p) by RLVECT_1:def 3
    .= (a*s1 + r*s3)*q + ((a*r1)*p + (r*r3)*p) by RLVECT_1:def 6
    .= (b*s2)*q + (b*r2)*p by A26,RLVECT_1:def 6
    .= b*(s2*q) + (b*r2)*p by RLVECT_1:def 7
    .= b*(s2*q) + b*(r2*p) by RLVECT_1:def 7
    .= b*(y-w) by A5,RLVECT_1:def 5;
A29: b*s2 = s1*a + s3*r;
   per cases;
   suppose that
A30: a=0 and
A31: b<>0;
    r*(z-u)=0.V by A27,A30,RLVECT_1:10;
    then z-u=0.V by A6,RLVECT_1:11;
    then z=u by RLVECT_1:21;
    then
A32: u,v // u,z;
    w,y // w,z or w,y // z,w by A28,A31,Lm1;
    hence thesis by A32;
  end;
  suppose a=0 & b=0;
    then r3=0 & s3=0 by A6,A26,A29,XCMPLX_1:6;
    then 0.V + 0*q = u-w by A25,RLVECT_1:10;
    then 0.V + 0.V = u-w by RLVECT_1:10;
    then 0.V=u-w by RLVECT_1:4;
    then u=w by RLVECT_1:21;
    then
A33: w,y // w,u;
    u,v // u,u;
    hence thesis by A33;
  end;
  suppose that
A34: a<>0 and
A35: b=0;
    r*(z-w)=0.V by A28,A35,RLVECT_1:10;
    then z-w=0.V by A6,RLVECT_1:11;
    then z=w by RLVECT_1:21;
    then
A36: w,y // w,z;
    u,v // u,z or u,v // z,u by A27,A34,Lm1;
    hence thesis by A36;
  end;
  suppose that
A37: a<>0 and
A38: b<>0;
A39: w,y // w,z or w,y // z,w by A28,A38,Lm1;
    u,v // u,z or u,v // z,u by A27,A37,Lm1;
    hence thesis by A39;
  end;
end;

definition
  struct(1-sorted) AffinStruct
  (#carrier -> set, CONGR -> Relation of [:the carrier,the carrier:]#);
end;

registration
  cluster non trivial strict for AffinStruct;
  existence
  proof
    set A = the non trivial set, R = the Relation of [:A,A:];
    take AffinStruct(#A,R#);
    thus thesis;
  end;
end;

reserve AS for non empty AffinStruct;
reserve a,b,c,d for Element of AS;
reserve x,z for object;

definition
  let AS,a,b,c,d;
  pred a,b // c,d means

  [[a,b],[c,d]] in the CONGR of AS;
end;

definition
  let V;
  func DirPar(V) -> Relation of [:the carrier of V,the carrier of V:] means
:Def3: [x,z] in it iff ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // w,y;
  existence
  proof
    defpred P[object,object] means
ex u,v,w,y st $1=[u,v] & $2=[w,y] & u,v // 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;
    thus [x,z] in P implies ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // w,y by A1;
    assume ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // 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: [x,z] in P iff ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // w,y and
A3: [x,z] in Q iff ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // 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,v,w,y st x=[u,v] & z=[w,y] & u,v // w,y by A2;
      hence thesis by A3;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

theorem Th22:
  [[u,v],[w,y]] in DirPar(V) iff u,v // w,y
proof
  thus [[u,v],[w,y]] in DirPar(V) implies u,v // w,y
  proof
    assume [[u,v],[w,y]] in DirPar(V);
    then consider u9,v9,w9,y9 being VECTOR of V such that
A1: [u,v]=[u9,v9] and
A2: [w,y]=[w9,y9] and
A3: u9,v9 // w9,y9 by Def3;
A4: w = w9 by A2,XTUPLE_0:1;
    u = u9 & v = v9 by A1,XTUPLE_0:1;
    hence thesis by A2,A3,A4,XTUPLE_0:1;
  end;
  thus thesis by Def3;
end;

definition
  let V;
  func OASpace(V) -> strict AffinStruct equals
  AffinStruct (#the carrier of V,
    DirPar(V)#);
  correctness;
end;

registration
  let V;
  cluster OASpace V -> non empty;
  coherence;
end;

theorem Th23:
  (ex u,v st for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0
  ) implies (ex a,b being Element of OASpace(V) st a<>b) & (for a,b,c,d,p,q,r,s
being Element of OASpace(V) holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b
& a,b // p,q & a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c)
& (a,b // b,c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,
b)) & (ex a,b,c,d being Element of OASpace(V) st not a,b // c,d & not a,b // d,
c) & (for a,b,c being Element of OASpace(V) ex d being Element of OASpace(V) st
a,b // c,d & a,c // b,d & b<>d) & for p,a,b,c being Element of OASpace(V) st p
  <>b & b,p // p,c ex d being Element of OASpace(V) st a,p // p,d & a,b // c,d
proof
  given u,v such that
A1: for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0;
  set S = OASpace(V);
A2: u<>v by A1,Th19;
  hence ex a,b being Element of S st a<>b;
  thus for a,b,c,d,p,q,r,s being Element of S holds a,b // c,c & (a,b // b,a
implies a=b) & (a<>b & a,b // p,q & a,b // r,s implies p,q // r,s) & (a,b // c,
d implies b,a // d,c) & (a,b // b,c implies a,b // a,c) & (a,b // a,c implies a
  ,b // b,c or a,c // c,b)
  proof
    let a,b,c,d,p,q,r,s be Element of S;
    reconsider a9=a,b9=b,c9=c,d9=d,p9=p,q9=q,r9=r,s9=s as Element of V;
    a9,b9 // c9,c9;
    hence [[a,b],[c,c]] in the CONGR of S by Def3;
    thus a,b // b,a implies a=b
    by Th22,Th10;
    thus a<>b & a,b // p,q & a,b // r,s implies p,q // r,s
    proof
      assume that
A3:   a<>b and
A4:   [[a,b],[p,q]] in the CONGR of S & [[a,b],[r,s]] in the CONGR of S;
      a9,b9 // p9,q9 & a9,b9 // r9,s9 by A4,Th22;
      then p9,q9 // r9,s9 by A3,Th11;
      then [[p,q],[r,s]] in the CONGR of S by Th22;
      hence thesis;
    end;
    thus a,b // c,d implies b,a // d,c
    proof
      assume [[a,b],[c,d]] in the CONGR of S;
      then a9,b9 // c9,d9 by Th22;
      then b9,a9 // d9,c9 by Th12;
      then [[b,a],[d,c]] in the CONGR of S by Th22;
      hence thesis;
    end;
    thus a,b // b,c implies a,b // a,c
    proof
      assume [[a,b],[b,c]] in the CONGR of S;
      then a9,b9 // b9,c9 by Th22;
      then a9,b9 // a9,c9 by Th13;
      then [[a,b],[a,c]] in the CONGR of S by Th22;
      hence thesis;
    end;
    thus a,b // a,c implies a,b // b,c or a,c // c,b
    proof
      assume [[a,b],[a,c]] in the CONGR of S;
      then a9,b9 // a9,c9 by Th22;
      then a9,b9 // b9,c9 or a9,c9 // c9,b9 by Th14;
      then [[a,b],[b,c]] in the CONGR of S or [[a,c],[c,b]] in the CONGR of S
      by Th22;
      hence thesis;
    end;
  end;
  thus ex a,b,c,d being Element of S st not a,b // c,d & not a,b // d,c
  proof
    consider a9,b9,c9,d9 being VECTOR of V such that
A5: not a9,b9 // c9,d9 and
A6: not a9,b9 // d9,c9 by A1,Th20;
    reconsider a=a9,b=b9,c = c9,d=d9 as Element of S;
    not [[a,b],[d,c]] in the CONGR of S by A6,Th22;
    then
A7: not a,b // d,c;
    not [[a,b],[c,d]] in the CONGR of S by A5,Th22;
    then not a,b // c,d;
    hence thesis by A7;
  end;
  thus for a,b,c being Element of S ex d being Element of S st a,b // c,d & a,
  c // b,d & b<>d
  proof
    let a,b,c be Element of S;
    reconsider a9=a,b9=b,c9=c as Element of V;
    consider d9 being VECTOR of V such that
A8: a9,b9 // c9,d9 and
A9: a9,c9 // b9,d9 and
A10: b9<>d9 by A2,Th17;
    reconsider d=d9 as Element of S;
    [[a,c],[b,d]] in the CONGR of S by A9,Th22;
    then
A11: a,c // b,d;
    [[a,b],[c,d]] in the CONGR of S by A8,Th22;
    then a,b // c,d;
    hence thesis by A10,A11;
  end;
  thus for p,a,b,c being Element of S st p<>b & b,p // p,c holds ex d being
  Element of S st a,p // p,d & a,b // c,d
  proof
    let p,a,b,c be Element of S;
    assume that
A12: p<>b and
A13: [[b,p],[p,c]] in the CONGR of S;
    reconsider p9=p,a9=a,b9=b,c9=c as Element of V;
    b9,p9 // p9,c9 by A13,Th22;
    then consider d9 being VECTOR of V such that
A14: a9,p9 // p9,d9 and
A15: a9,b9 // c9,d9 by A12,Th18;
    reconsider d=d9 as Element of S;
    [[a,b],[c,d]] in the CONGR of S by A15,Th22;
    then
A16: a,b // c,d;
    [[a,p],[p,d]] in the CONGR of S by A14,Th22;
    then a,p // p,d;
    hence thesis by A16;
  end;
end;

theorem Th24:
  (ex p,q being VECTOR of V st (for w being VECTOR of V ex a,b
being Real st a*p + b*q=w)) implies
 for a,b,c,d being Element of OASpace(V) st
not a,b // c,d & not a,b // d,c ex t being Element of OASpace(V) st (a,b // a,t
  or a,b // t,a) & (c,d // c,t or c,d // t,c)
proof
  assume
A1: ex p,q being VECTOR of V st for w being VECTOR of V ex a,b being
  Real st a*p + b*q=w;
  set S = OASpace(V);
  let a,b,c,d be Element of OASpace(V);
  reconsider a9=a,b9=b,c9 = c,d9=d as Element of V;
  assume
  ( not [[a,b],[c,d]] in the CONGR of S)& not [[a,b],[d,c]] in the CONGR of S;
  then ( not a9,b9 // c9,d9)& not a9,b9 // d9,c9 by Th22;
  then consider t9 being VECTOR of V such that
A2: a9,b9 // a9,t9 or a9,b9 // t9,a9 and
A3: c9,d9 // c9,t9 or c9,d9 // t9,c9 by A1,Th21;
  reconsider t=t9 as Element of S;
  [[c,d],[c,t]] in the CONGR of S or [[c,d],[t,c]] in the CONGR of S by A3,Th22
;
  then
A4: c,d // c,t or c,d // t,c;
  [[a,b],[a,t]] in the CONGR of S or [[a,b],[t,a]] in the CONGR of S by A2,Th22
;
  then a,b // a,t or a,b // t,a;
  hence thesis by A4;
end;

definition
  let IT be non empty AffinStruct;
  attr IT is OAffinSpace-like means
  :Def5:
  (for a,b,c,d,p,q,r,s being Element
of IT holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q & a,b //
r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,c implies
  a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,b,c,d
  being Element of IT st not a,b // c,d & not a,b // d,c) & (for a,b,c being
Element of IT ex d being Element of IT st a,b // c,d & a,c // b,d & b<>d) & for
p,a,b,c being Element of IT st p<>b & b,p // p,c ex d being Element of IT st a,
  p // p,d & a,b // c,d;
end;

registration
  cluster strict OAffinSpace-like for non trivial AffinStruct;
  existence
  proof
    consider V,u,v such that
A1: for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0 and
    for w ex a,b being Real st w = a*u + b*v by FUNCSDOM:23;
A2: ( ex a,b,c,d being Element of OASpace(V) st not a,b // c,d & not a,b
// d,c)& for a,b,c being Element of OASpace(V) ex d being Element of OASpace(V
    ) st a,b // c,d & a,c // b,d & b<>d by A1,Th23;
A3: for p,a,b,c being Element of OASpace(V) st p<>b & b,p // p,c ex d
    being Element of OASpace(V) st a,p // p,d & a,b // c,d by A1,Th23;
    ( ex a,b being Element of OASpace(V) st a<>b)& for a,b,c,d,p,q,r,s
being Element of OASpace(V) holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b
& a,b // p,q & a,b // r,s implies p,q // r,s) & (a, b // c,d implies b,a // d,c
) & (a,b // b,c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c //
    c,b) by A1,Th23;
    then OASpace(V) is non trivial OAffinSpace-like by A2,A3,
STRUCT_0:def 10;
    hence thesis;
  end;
end;

definition
  mode OAffinSpace is OAffinSpace-like non trivial AffinStruct;
end;

theorem
  (ex a,b being Element of AS st a<>b) & (for a,b,c,d,p,q,r,s being
Element of AS holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q
& a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,
c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,
  b,c,d being Element of AS st not a,b // c,d & not a,b // d,c) & (for a,b,c
being Element of AS ex d being Element of AS st a,b // c,d & a,c // b,d & b<>d)
  & (for p,a,b,c being Element of AS st p<>b & b,p // p,c ex d being Element of
  AS st a,p // p,d & a,b // c,d) iff AS is OAffinSpace by Def5,STRUCT_0:def 10;

theorem Th26:
  (ex u,v st for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0
  ) implies OASpace(V) is OAffinSpace
proof
  assume
A1: ex u,v st for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0;
  then
A2: ( ex a,b,c,d being Element of OASpace(V) st not a,b // c,d & not a,b //
  d,c)& for a,b,c being Element of OASpace(V) ex d being Element of OASpace(V)
  st a,b // c,d & a,c // b,d & b<>d by Th23;
A3: for p,a,b,c being Element of OASpace(V) st p<>b & b,p // p,c ex d being
  Element of OASpace(V) st a,p // p,d & a,b // c,d by A1,Th23;
  ( ex a,b being Element of OASpace(V) st a<>b)& for a,b,c,d,p,q,r,s being
Element of OASpace(V) holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b
// p,q & a,b // r,s implies p,q // r,s) & (a, b // c,d implies b,a // d,c) & (a
  ,b // b,c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)
  by A1,Th23;
  hence thesis by A2,A3,Def5,STRUCT_0:def 10;
end;

definition
  let IT be OAffinSpace;
  attr IT is 2-dimensional means
  :Def6:
  for a,b,c,d being Element of IT st not
a,b // c,d & not a,b // d,c holds ex p being Element of IT st (a,b // a,p or a,
  b // p,a) & (c,d // c,p or c,d // p,c);
end;

registration
  cluster strict 2-dimensional for OAffinSpace;
  existence
  proof
    consider V such that
A1: ex u,v st (for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0)
    & for w ex a,b being Real st w = a*u + b*v by FUNCSDOM:23;
    reconsider S = OASpace(V) as OAffinSpace by A1,Th26;
    for a,b,c,d being Element of S st not a,b // c,d & not a,b // d,c
holds ex p being Element of S st (a,b // a,p or a,b // p,a) & (c,d // c,p or c,
    d // p,c) by A1,Th24;
    then S is 2-dimensional;
    hence thesis;
  end;
end;

definition
  mode OAffinPlane is 2-dimensional OAffinSpace;
end;

theorem
  (ex a,b being Element of AS st a<>b) & (for a,b,c,d,p,q,r,s being
Element of AS holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q
& a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,
c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,
  b,c,d being Element of AS st not a,b // c,d & not a,b // d,c) & (for a,b,c
being Element of AS ex d being Element of AS st a,b // c,d & a,c // b,d & b<>d)
  & (for p,a,b,c being Element of AS st p<>b & b,p // p,c ex d being Element of
AS st a,p // p,d & a,b // c,d) & (for a,b,c,d being Element of AS st not a,b //
c,d & not a,b // d,c holds ex p being Element of AS st (a,b // a,p or a,b // p,
  a) & (c,d // c,p or c,d // p,c)) iff AS is OAffinPlane by Def5,Def6,
STRUCT_0:def 10;

theorem
  (ex u,v st (for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0) &
  (for w ex a,b being Real st w = a*u + b*v)) implies
   OASpace(V) is OAffinPlane
proof
  set S=OASpace(V);
  assume
A1: ex u,v st (for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0) &
  for w ex a,b being Real st w = a*u + b*v;
  then
  for a,b,c,d being Element of S st not a,b // c,d & not a,b // d,c holds
ex p being Element of S st (a,b // a,p or a,b // p,a) & (c,d // c,p or c,d // p
  ,c) by Th24;
  hence thesis by A1,Def6,Th26;
end;