AFVECT01

:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
::  by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and
::     Krzysztof Pra\.zmowski
::
:: Received October 4, 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 AFVECT0, SUBSET_1, XBOOLE_0, RELAT_1, ZFMISC_1, ANALOAF, PARSP_1,
      DIRAF, STRUCT_0, AFVECT01;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ANALOAF, DIRAF,
      AFVECT0, RELSET_1;
 constructors DOMAIN_1, DIRAF, AFVECT0;
 registrations XBOOLE_0, STRUCT_0, AFVECT0;
 requirements SUBSET, BOOLE;
 theorems ZFMISC_1, AFVECT0, STRUCT_0, ANALOAF, DIRAF, XTUPLE_0;
 schemes RELSET_1;

begin

reserve AFV for WeakAffVect;
reserve a,a9,b,b9,c,d,p,p9,q,q9,r,r9 for Element of AFV;

registration
  let A be non empty set, C be Relation of [:A,A:];
  cluster AffinStruct(#A,C#) -> non empty;
  coherence;
end;

Lm1: a,b '||' b,c & a<>c implies a,b // b,c
proof
  assume that
A1: a,b '||' b,c and
A2: a<>c;
  not a,b // c,b by A2,AFVECT0:4,7;
  hence thesis by A1,DIRAF:def 4;
end;

Lm2: a,b // b,a iff ex p,q st a,b '||' p,q & a,p '||' p,b & a,q '||' q,b
proof
A1: now
    given p,q such that
A2: a,b '||' p,q and
A3: a,p '||' p,b and
A4: a,q '||' q,b;
    now
A5:   now
        assume
A6:     MDist p,q;
        a,b // p,q or a,b // q,p by A2,DIRAF:def 4;
        then MDist a,b by A6,AFVECT0:3,15;
        hence a,b // b,a by AFVECT0:def 2;
      end;
      assume
A7:   a<>b;
      then a,q // q,b by A4,Lm1;
      then
A8:   Mid a,q,b by AFVECT0:def 3;
A9:   now
        assume p=q;
        then a,b // p,p by A2,DIRAF:def 4;
        hence contradiction by A7,AFVECT0:def 1;
      end;
      a,p // p,b by A3,A7,Lm1;
      then Mid a,p,b by AFVECT0:def 3;
      hence a,b // b,a by A8,A9,A5,AFVECT0:20;
    end;
    hence a,b // b,a by AFVECT0:2;
  end;
  now
    assume
A10: a,b // b,a;
A11: now
      assume a<>b;
      then
A12:  MDist a,b by A10,AFVECT0:def 2;
      consider p such that
A13:  Mid a,p,b by AFVECT0:19;
A14:  a,p // p,b by A13,AFVECT0:def 3;
      consider q such that
A15:  a,b // p,q by AFVECT0:def 1;
      take p,q;
      Mid a,q,b by A13,A15,A12,AFVECT0:15,23;
      then a,q // q,b by AFVECT0:def 3;
      hence a,b '||' p,q & a,p '||' p,b & a,q '||' q,b by A15,A14,DIRAF:def 4;
    end;
    now
      assume
A16:  a=b;
      take p=a,q=a;
      a,b // p,q by A16,AFVECT0:2;
      hence a,b '||' p,q & a,p '||' p,b & a,q '||' q,b by A16,DIRAF:def 4;
    end;
    hence ex p,q st a,b '||' p,q & a,p '||' p,b & a,q '||' q,b by A11;
  end;
  hence thesis by A1;
end;

Lm3: a,b '||' c,d implies b,a '||' c,d
proof
  assume a,b '||' c,d;
  then a,b // c,d or a,b // d,c by DIRAF:def 4;
  then b,a // d,c or b,a // c,d by AFVECT0:7;
  hence thesis by DIRAF:def 4;
end;

Lm4: a,b '||' b,a
proof
  a,b // a,b by AFVECT0:1;
  hence thesis by DIRAF:def 4;
end;

Lm5: a,b '||' p,p implies a=b
proof
  assume a,b '||' p,p;
  then a,b // p,p by DIRAF:def 4;
  hence thesis by AFVECT0:def 1;
end;

Lm6: for a,b,c,d,p,q holds a,b '||' p,q & c,d '||' p,q implies a,b '||' c,d
proof
  let a,b,c,d,p,q;
  assume a,b '||' p,q & c,d '||' p,q;
  then a,b // p,q & c,d // p,q or a,b // p,q & c,d // q,p or a,b // q,p & c,d
  // p,q or a,b // q,p & c,d // q,p by DIRAF:def 4;
  then a,b // c,d or a,b // p,q & d,c // p,q or a,b // q,p & d,c // q,p by
AFVECT0:7,def 1;
  then a,b // c,d or a,b // d,c by AFVECT0:def 1;
  hence thesis by DIRAF:def 4;
end;

Lm7: ex b st a,b '||' b,c
proof
  consider b such that
A1: a,b // b,c by AFVECT0:def 1;
  take b;
  thus thesis by A1,DIRAF:def 4;
end;

Lm8: for a,a9,b,b9,p st a<>a9 & b<>b9 & p,a '||' p,a9 & p,b '||' p,b9 holds a,
b '||' a9,b9
proof
  let a,a9,b,b9,p;
  assume that
A1: a<>a9 and
A2: b<>b9 and
A3: p,a '||' p,a9 and
A4: p,b '||' p,b9;
  b,p // p,b9 by A2,A4,Lm1,Lm3;
  then
A5: Mid b,p,b9 by AFVECT0:def 3;
  a,p // p,a9 by A1,A3,Lm1,Lm3;
  then Mid a,p,a9 by AFVECT0:def 3;
  then a,b // b9,a9 by A5,AFVECT0:25;
  hence thesis by DIRAF:def 4;
end;

Lm9: a=b or ex c st a<>c & a,b '||' b,c or ex p,p9 st p<>p9 & a,b '||' p,p9 &
a,p '||' p,b & a,p9 '||' p9,b
proof
  consider c such that
A1: a,b // b,c by AFVECT0:def 1;
A2: now
    assume a=c;
    then consider p,p9 such that
A3: a,b '||' p,p9 and
A4: a,p '||' p,b & a,p9 '||' p9,b by A1,Lm2;
    p=p9 implies a=b by A3,Lm5;
    hence
    a=b or ex p,p9 st p<>p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9
    ,b by A3,A4;
  end;
  now
    assume
A5: a<>c;
    a,b '||' b,c by A1,DIRAF:def 4;
    hence ex c st a<>c & a,b '||' b,c by A5;
  end;
  hence thesis by A2;
end;

Lm10: for a,b,b9,p,p9,c st a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,
p9 '||' p9,b9 holds a,b9 '||' b9,c
proof
  let a,b,b9,p,p9,c;
  assume that
A1: a,b '||' b,c and
A2: b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9;
A3: b,b9 // b9,b by A2,Lm2;
A4: now
    assume
A5: a,b // b,c;
    then
A6: Mid a,b,c by AFVECT0:def 3;
A7: now
      assume MDist b,b9;
      then Mid a,b9,c by A6,AFVECT0:23;
      then a,b9 // b9,c by AFVECT0:def 3;
      hence thesis by DIRAF:def 4;
    end;
    b=b9 implies thesis by A5,DIRAF:def 4;
    hence thesis by A3,A7,AFVECT0:def 2;
  end;
  now
    assume a,b // c,b;
    then a=c by AFVECT0:4,7;
    then a,b9 // c,b9 by AFVECT0:1;
    hence thesis by DIRAF:def 4;
  end;
  hence thesis by A1,A4,DIRAF:def 4;
end;

Lm11: for a,b,b9,c st a<>c & b<>b9 & a,b '||' b,c & a,b9 '||' b9,c holds ex p,
p9 st p<>p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9
proof
  let a,b,b9,c;
  assume that
A1: a<>c and
A2: b<>b9 and
A3: a,b '||' b,c and
A4: a,b9 '||' b9,c;
  a,b9 // b9,c by A1,A4,Lm1;
  then
A5: Mid a,b9,c by AFVECT0:def 3;
  a,b // b,c by A1,A3,Lm1;
  then Mid a,b,c by AFVECT0:def 3;
  then MDist b, b9 by A2,A5,AFVECT0:20;
  then b,b9 // b9,b by AFVECT0:def 2;
  then consider p,p9 such that
A6: b,b9 '||' p,p9 and
A7: b,p '||' p,b9 & b,p9 '||' p9,b9 by Lm2;
  p<>p9 implies thesis by A6,A7;
  hence thesis by A2,A6,Lm5;
end;

Lm12: for a,b,c,p,p9,q,q9 st a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,
q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c holds ex r,r9 st b,c '||' r,r9 & b
,r '||' r,c & b,r9 '||' r9,c
proof
  let a,b,c,p,p9,q,q9;
  assume a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9
  '||' p9,b & a,q9 '||' q9,c;
  then a,b // b,a & a,c // c,a by Lm2;
  then b,c // c,b by AFVECT0:12;
  hence thesis by Lm2;
end;

set AFV0 = the WeakAffVect;
set X = the carrier of AFV0;
set XX = [:X,X:];
defpred P[object,object] means
ex a,b,c,d being Element of X st $1=[a,b] & $2=[c,d]
& a,b '||' c,d;
consider P being Relation of XX,XX such that
Lm13: for x,y being object holds [x,y] in P iff x in XX & y in XX & P[x,y]
from RELSET_1:sch 1;

Lm14: for a,b,c,d being Element of X holds [[a,b],[c,d]] in P iff a,b '||' c,d
proof
  let a,b,c,d be Element of X;
A1: [[a,b],[c,d]] in P implies a,b '||' c,d
  proof
    assume [[a,b],[c,d]] in P;
    then consider a9,b9,c9,d9 being Element of X such that
A2: [a,b]=[a9,b9] and
A3: [c,d]=[c9,d9] and
A4: a9,b9 '||' c9,d9 by Lm13;
A5: c = c9 by A3,XTUPLE_0:1;
    a=a9 & b=b9 by A2,XTUPLE_0:1;
    hence thesis by A3,A4,A5,XTUPLE_0:1;
  end;
  [a,b] in XX & [c,d] in XX by ZFMISC_1:def 2;
  hence thesis by A1,Lm13;
end;

set WAS = AffinStruct(#the carrier of AFV0,P#);

Lm15: for a,b,c,d being Element of AFV0, a9,b9,c9,d9 being Element
 of WAS st a=a9 & b=b9 & c =c9 & d=d9 holds a,b '||' c,d iff a9,b9 // c9
,d9
proof
  let a,b,c,d be Element of AFV0, a9,b9,c9,d9 be Element of WAS
  such that
A1: a=a9 & b=b9 & c =c9 & d=d9;
A2: now
    assume a9,b9 // c9,d9;
    then [[a9,b9],[c9,d9]] in P by ANALOAF:def 2;
    hence a,b '||' c,d by A1,Lm14;
  end;
  now
    assume a,b '||' c,d;
    then [[a,b],[c,d]] in the CONGR of WAS by Lm14;
    hence a9,b9 // c9,d9 by A1,ANALOAF:def 2;
  end;
  hence thesis by A2;
end;

Lm16: now
  thus ex a9,b9 being Element of WAS st a9<>b9 by STRUCT_0:def 10;
  thus for a9,b9 being Element of WAS holds a9,b9 // b9,a9
  proof
    let a9,b9 be Element of WAS;
    reconsider a=a9,b=b9 as Element of AFV0;
    a,b '||' b,a by Lm4;
    hence thesis by Lm15;
  end;
  thus for a9,b9 being Element of WAS st a9,b9 // a9,a9 holds a9=b9
  proof
    let a9,b9 be Element of WAS such that
A1: a9,b9 // a9,a9;
    reconsider a=a9,b=b9 as Element of AFV0;
    a,b '||' a,a by A1,Lm15;
    hence thesis by Lm5;
  end;
  thus for a,b,c,d,p,q being Element of WAS st a,b // p,q & c,d // p,q holds a
  ,b // c,d
  proof
    let a,b,c,d,p,q be Element of WAS such that
A2: a,b // p,q & c,d // p,q;
    reconsider a1=a,b1=b,c1=c, d1=d,p1=p,q1=q as Element of AFV0;
    a1,b1 '||' p1,q1 & c1,d1 '||' p1,q1 by A2,Lm15;
    then a1,b1 '||' c1,d1 by Lm6;
    hence thesis by Lm15;
  end;
  thus for a,c being Element of WAS ex b being Element of WAS st a,b // b,c
  proof
    let a,c be Element of WAS;
    reconsider a1=a,c1=c as Element of AFV0;
    consider b1 being Element of AFV0 such that
A3: a1,b1 '||' b1,c1 by Lm7;
    reconsider b=b1 as Element of WAS;
    a,b // b,c by A3,Lm15;
    hence thesis;
  end;
  thus for a,a9,b,b9,p being Element of WAS st a<>a9 & b<>b9& p,a // p,a9 & p,
  b // p,b9 holds a,b // a9,b9
  proof
    let a,a9,b,b9,p be Element of WAS such that
A4: a<>a9 & b<>b9 and
A5: p,a // p,a9 & p,b // p,b9;
    reconsider a1=a,a19=a9,b1=b,b19=b9,p1=p as Element of AFV0;
    p1,a1 '||' p1,a19 & p1,b1 '||' p1,b19 by A5,Lm15;
    then a1,b1 '||' a19,b19 by A4,Lm8;
    hence thesis by Lm15;
  end;
  thus for a,b being Element of WAS holds a=b or ex c being Element of WAS st
  a<>c & a,b // b,c or ex p,p9 being Element of WAS st p<>p9 & a,b // p,p9& a,p
  // p,b & a,p9 // p9,b
  proof
    let a,b be Element of WAS such that
A6: not a=b;
    reconsider a1=a,b1=b as Element of AFV0;
A7: now
      given p1,p19 being Element of AFV0 such that
A8:   p1<>p19 and
A9:   a1,b1 '||' p1,p19 & a1,p1 '||' p1,b1 and
A10:  a1,p19 '||' p19,b1;
      reconsider p=p1,p9=p19 as Element of WAS;
A11:  a,p9 // p9,b by A10,Lm15;
      a,b // p,p9 & a,p // p,b by A9,Lm15;
      hence
      ex p,p9 being Element of WAS st p<>p9 & a,b // p,p9& a,p // p,b & a
      ,p9 // p9,b by A8,A11;
    end;
    now
      given c1 being Element of AFV0 such that
A12:  a1<>c1 and
A13:  a1,b1 '||' b1,c1;
      reconsider c =c1 as Element of WAS;
      a,b // b,c by A13,Lm15;
      hence ex c being Element of WAS st a<>c & a,b // b,c by A12;
    end;
    hence thesis by A6,A7,Lm9;
  end;
  thus for a,b,b9,p,p9,c being Element of WAS st a,b // b,c & b,b9 // p,p9 & b
  ,p // p,b9& b,p9 // p9,b9 holds a,b9 // b9,c
  proof
    let a,b,b9,p,p9,c be Element of WAS such that
A14: a,b // b,c & b,b9 // p,p9 and
A15: b,p // p,b9 & b,p9 // p9,b9;
    reconsider a1=a,b1=b,b19=b9,p1=p, p19=p9,c1=c as Element of AFV0;
A16: b1,p1 '||' p1,b19 & b1,p19 '||' p19,b19 by A15,Lm15;
    a1,b1 '||' b1,c1 & b1,b19 '||' p1,p19 by A14,Lm15;
    then a1,b19 '||' b19,c1 by A16,Lm10;
    hence thesis by Lm15;
  end;
  thus for a,b,b9,c being Element of WAS st a<>c & b<>b9 & a,b // b,c & a,b9
// b9,c holds ex p,p9 being Element of WAS st p<>p9 & b,b9 // p,p9& b,p // p,b9
  & b,p9 // p9,b9
  proof
    let a,b,b9,c be Element of WAS such that
A17: a<>c & b<>b9 and
A18: a,b // b,c & a,b9 // b9,c;
    reconsider a1=a,b1=b,b19=b9,c1=c as Element of AFV0;
    a1,b1 '||' b1,c1 & a1,b19 '||' b19,c1 by A18,Lm15;
    then consider p1,p19 being Element of AFV0 such that
A19: p1<>p19 and
A20: b1,b19 '||' p1,p19 & b1,p1 '||' p1,b19 and
A21: b1,p19 '||' p19,b19 by A17,Lm11;
    reconsider p=p1,p9=p19 as Element of WAS;
A22: b,p9 // p9,b9 by A21,Lm15;
    b,b9 // p,p9 & b,p // p,b9 by A20,Lm15;
    hence thesis by A19,A22;
  end;
  thus for a,b,c,p,p9,q,q9 being Element of WAS st a,b // p,p9 & a,c // q,q9 &
  a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r,r9 being
  Element of WAS st b,c // r,r9 & b,r // r,c & b,r9 // r9,c
  proof
    let a,b,c,p,p9,q,q9 be Element of WAS such that
A23: a,b // p,p9 & a,c // q,q9 and
A24: a,p // p,b & a,q // q,c and
A25: a,p9 // p9,b & a,q9 // q9,c;
    reconsider a1=a,b1=b,c1=c,p1=p,p19=p9,q1=q,q19=q9 as Element of AFV0;
A26: a1,p1 '||' p1,b1 & a1,q1 '||' q1,c1 by A24,Lm15;
A27: a1,p19 '||' p19,b1 & a1,q19 '||' q19,c1 by A25,Lm15;
    a1,b1 '||' p1,p19 & a1,c1 '||' q1,q19 by A23,Lm15;
    then consider r1,r19 being Element of AFV0 such that
A28: b1,c1 '||' r1,r19 & b1,r1 '||' r1,c1 and
A29: b1,r19 '||' r19,c1 by A26,A27,Lm12;
    reconsider r=r1,r9=r19 as Element of WAS;
A30: b,r9 // r9,c by A29,Lm15;
    b,c // r,r9 & b,r // r,c by A28,Lm15;
    hence thesis by A30;
  end;
end;

definition
  let IT be non empty AffinStruct;

  attr IT is WeakAffSegm-like means
  :Def1:
  (for a,b being Element of IT holds
a,b // b,a) & (for a,b being Element of IT st a,b // a,a holds a=b) & (for a,b,
c,d,p,q being Element of IT st a,b // p,q & c,d // p,q holds a,b // c,d) & (for
a,c being Element of IT ex b being Element of IT st a,b // b,c) & (for a,a9,b,
b9,p being Element of IT st a<>a9 & b<>b9& p,a // p,a9 & p,b // p,b9 holds a,b
// a9,b9) & (for a,b being Element of IT holds a=b or ex c being Element of IT
st ( a<>c & a,b // b,c) or ex p,p9 being Element of IT st (p<>p9 & a,b // p,p9
  & a,p // p,b & a,p9 // p9,b)) & (for a,b,b9,p,p9,c being Element of IT st a,b
// b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c) & (for
a,b,b9,c being Element of IT st a<>c & b<>b9 & a,b // b,c & a,b9 // b9,c holds
ex p,p9 being Element of IT st p<>p9 & b,b9 // p,p9& b,p // p,b9 & b,p9 // p9,
b9) & for a,b,c,p,p9,q,q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a,
p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r,r9 being Element
  of IT st b,c // r,r9 & b,r // r,c & b,r9 // r9,c;
end;

registration
  cluster strict WeakAffSegm-like for non trivial AffinStruct;
  existence
  proof
    WAS is WeakAffSegm-like non trivial by Lm16;
    hence thesis;
  end;
end;

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

::
::         PROPERTIES OF RELATION OF CONGRUENCE OF THE CARRIER
::

reserve AFV for WeakAffSegm;
reserve a,b,b9,b99,c,d,p,p9 for Element of AFV;

theorem Th1:
  a,b // a,b
proof
  a,b // b,a by Def1;
  hence thesis by Def1;
end;

theorem Th2:
  a,b // c,d implies c,d // a,b
proof
  assume
A1: a,b // c,d;
  c,d // c,d by Th1;
  hence thesis by A1,Def1;
end;

theorem Th3:
  a,b // c,d implies a,b // d,c
proof
  assume
A1: a,b // c,d;
  d,c // c,d by Def1;
  hence thesis by A1,Def1;
end;

theorem Th4:
  a,b // c,d implies b,a // c,d
proof
  assume a,b // c,d;
  then c,d // a,b by Th2;
  then c,d // b,a by Th3;
  hence thesis by Th2;
end;

theorem Th5:
  for a,b holds a,a // b,b
proof
  let a,b;
  now
    consider c such that
A1: a,c // c,b by Def1;
    assume
A2: a<>b;
    c,a // c,b by A1,Th4;
    hence thesis by A2,Def1;
  end;
  hence thesis by Def1;
end;

theorem Th6:
  a,b // c,c implies a=b
proof
  assume
A1: a,b // c,c;
  a,a // c,c by Th5;
  then a,b // a,a by A1,Def1;
  hence thesis by Def1;
end;

theorem Th7:
  a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b implies a=c
proof
  assume that
A1: a,b // p,p9 and
A2: a,b // b,c and
A3: a,p // p,b and
A4: a,p9 // p9,b;
  p,b // a,p by A3,Th2;
  then p,b // p,a by Th3;
  then
A5: b,p // p,a by Th4;
  p9,b // a,p9 by A4,Th2;
  then p9,b // p9,a by Th3;
  then
A6: b,p9 // p9,a by Th4;
  b,a // p,p9 by A1,Th4;
  then a,a // a,c by A2,A5,A6,Def1;
  then a,c // a,a by Th2;
  hence thesis by Def1;
end;

theorem
  a,b9 // a,b99 & a,b // a,b99 implies b=b9 or b=b99 or b9=b99
proof
  assume
A1: a,b9 // a,b99 & a,b // a,b99;
  now
    assume b9<>b99 & b<>b99;
    then b9,b // b99,b99 by A1,Def1;
    hence thesis by Th6;
  end;
  hence thesis;
end;

::
::          RELATION OF MAXIMAL DISTANCE AND MIDPOINT RELATION
::

definition
  let AFV;
  let a,b;

  pred MDist a,b means

  ex p,p9 st p<>p9 & a,b // p,p9 & a,p // p,b & a, p9 // p9,b;
end;

definition
  let AFV;
  let a,b,c;
  pred Mid a,b,c means
  a=b & b=c & a=c or a=c & MDist a,b or a<>c & a,b // b,c;
end;

theorem
  a<>b & not MDist a,b implies ex c st a<>c & a,b // b,c
by Def1;

theorem
  MDist a,b & a,b // b,c implies a=c
by Th7;

theorem
  MDist a,b implies a<>b
by Th2,Th6;