:: Parallelity Spaces
::  by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: Copyright (c) 1990-2019 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 VECTSP_1, SUBSET_1, RLVECT_1, ALGSTR_0, XBOOLE_0, ARYTM_1,
      ARYTM_3, RELAT_1, SUPINF_2, ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, TARSKI,
      PARSP_1, RECDEF_2, ANALOAF;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, FUNCT_2,
      BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RELSET_1;
 constructors BINOP_1, DOMAIN_1, VECTSP_1, RLVECT_1, RELSET_1, ZFMISC_1,
      GROUP_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, VECTSP_1, XTUPLE_0, MCART_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, STRUCT_0;
 equalities XTUPLE_0, MCART_1;
 theorems MCART_1, VECTSP_1, BINOP_1, FUNCT_2, TARSKI, RLVECT_1, GROUP_1;
 schemes BINOP_1, FUNCT_2, XBOOLE_0;

begin

reserve F for Field,
  a,b,c,d,e,f,g,h for Element of F;

Lm1: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a, b being Element of F holds -(a-b) = b-a
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, a, b be Element of F;
  thus -(a-b) = b+-a by RLVECT_1:33
    .= b-a by RLVECT_1:def 11;
end;

Lm2: (a-b)*(c-d) - (b-a)*(d-c) = 0.F
proof
  -(a-b) = b-a & -(c-d) = d-c by Lm1;
  then (a-b)*(c-d)-(b-a)*(d-c)=(a-b)*(c-d)-((a-b)*(c-d)) by VECTSP_1:10;
  hence thesis by RLVECT_1:15;
end;

Lm3: a*(b-b) - (c-c)*d = 0.F
proof
  c-c = 0.F by RLVECT_1:15;
  then
A1: (c-c)*d = 0.F;
  b-b = 0.F by RLVECT_1:15;
  then a*(b-b) = 0.F;
  hence thesis by A1,RLVECT_1:15;
end;

Lm4: a <> 0.F & a*e - d*b = 0.F & a*c - h*b = 0.F implies d*c - h*e = 0.F
proof
  assume that
A1: a <> 0.F and
A2: a*e - d*b = 0.F and
A3: a*c - h*b = 0.F;
  c = h*b*a" by A1,A3,VECTSP_1:30;
  then c = h*(b*a") by GROUP_1:def 3;
  then
A4: d*c = (d*h)*(b*a") by GROUP_1:def 3;
  e = d*b*a" by A1,A2,VECTSP_1:30;
  then e = d*(b*a") by GROUP_1:def 3;
  then h*e = (h*d)*(b*a") by GROUP_1:def 3;
  hence thesis by A4,RLVECT_1:15;
end;

Lm5: a*b - c*d = 0.F implies d*c - b*a = 0.F
proof
  assume a*b - c*d = 0.F;
  then
A1: -(a*b - c*d) = 0.F by RLVECT_1:12;
  thus d*c - b*a = d*c + -(b*a) by RLVECT_1:def 11
    .= 0.F by A1,RLVECT_1:33;
end;

Lm6: b <> 0.F & a*e - d*b = 0.F & a*c - h*b = 0.F implies d*c - h*e = 0.F
proof
  assume b <> 0.F;
  then b*d - e*a = 0.F & b*h - c*a = 0.F implies e*h - c*d = 0.F by Lm4;
  hence thesis by Lm5;
end;

Lm7: (c*d)*(a*b) = ((a*c)*d)*b
proof
  thus (c*d)*(a*b) = (a*(c*d))*b by GROUP_1:def 3
    .= ((a*c)*d)*b by GROUP_1:def 3;
end;

Lm8: a*b - c*d = 0.F implies (a*f*g*b) - (c*f*g*d) = 0.F
proof
  assume
A1: a*b - c*d = 0.F;
  (a*f*g*b) = (f*g)*(a*b) & (c*f*g*d) = (f*g)*(c*d) by Lm7;
  hence (a*f*g*b) - (c*f*g*d) = (f*g)*(a*b - c*d) by VECTSP_1:11
    .= 0.F by A1;
end;

Lm9: (a-b)*(c-d) = a*c + (-a*d +-(b*(c-d)))
proof
  thus (a-b)*(c-d) = (a+-b)*(c-d) by RLVECT_1:def 11
    .= a*(c-d)+(-b)*(c-d) by VECTSP_1:def 7
    .= a*(c-d)+-b*(c-d) by VECTSP_1:9
    .= (a*c-a*d)+-b*(c-d) by VECTSP_1:11
    .= (a*c+-a*d)+-b*(c-d) by RLVECT_1:def 11
    .= a*c + (-a*d +-(b*(c-d))) by RLVECT_1:def 3;
end;

Lm10: (a+b)+(c+d) = a+(b+c)+d
proof
  thus (a+b)+(c+d) = (a+b)+c+d by RLVECT_1:def 3
    .= a+(b+c)+d by RLVECT_1:def 3;
end;

Lm11: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a, b, c being Element of F holds (b+a)-(c+a) = b-c
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, a,b,c be Element of F;
  thus (b+a)-(c+a) = (b+a)+-(c+a) by RLVECT_1:def 11
    .= (b+a)+(-a+-c) by RLVECT_1:31
    .= ((b+a)+-a)+-c by RLVECT_1:def 3
    .= (b+(a+-a))+-c by RLVECT_1:def 3
    .= (b+0.F)+-c by RLVECT_1:def 10
    .= b+-c by RLVECT_1:4
    .= b-c by RLVECT_1:def 11;
end;

Lm12: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a, b being Element of F holds a + b = -(-b + -a)
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, a,b be Element of F;
  thus a + b = --(a + b) by RLVECT_1:17
    .= -(-b + -a) by RLVECT_1:31;
end;

Lm13: (a-b)*(c-d)-(a-e)*(c-f) = 0.F implies (b-a)*(f-d)-(b-e)*(f-c) = 0.F
proof
  assume
A1: (a-b)*(c-d)-(a-e)*(c-f) = 0.F;
A2: (a-b)*(c-d) = a*c+(-a*d+-(b*(c-d))) & (a-e)*(c-f) = a*c+(-a*f+-(e*(c-f))
  ) by Lm9;
  (b-a)*(f-d) = b*f+(-b*d+-(a*(f-d))) & (b-e)*(f-c) = b*f +(-b*c+-(e*(f-c)
  ) ) by Lm9;
  hence (b-a)*(f-d)-(b-e)*(f-c) = (-b*d+-(a*(f-d)))-(-b*c+-(e*(f-c))) by Lm11
    .= (-b*d+-(a*f-a*d))-(-b*c+-(e*(f-c))) by VECTSP_1:11
    .= (-b*d+(-a*f+a*d))-(-b*c+-(e*(f-c))) by RLVECT_1:33
    .= ((-b*d+a*d)+-a*f)-(-b*c+-(e*(f-c))) by RLVECT_1:def 3
    .= ((a*d+-b*d)+-a*f)+-(-b*c+-(e*(f-c))) by RLVECT_1:def 11
    .= ((a*d+-b*d)+-a*f)+(--b*c+--(e*(f-c))) by RLVECT_1:31
    .= ((a*d+-b*d)+-a*f)+(b*c+--(e*(f-c))) by RLVECT_1:17
    .= ((a*d+-b*d)+-a*f)+(b*c+(e*(f-c))) by RLVECT_1:17
    .= ((a*d+-b*d)+(-a*f+b*c))+(e*(f-c)) by Lm10
    .= ((a*d+-b*d)+b*c)+(-a*f+(e*(f-c))) by Lm10
    .= (a*d+(-b*d+b*c))+(-a*f+(e*(f-c))) by RLVECT_1:def 3
    .= (a*d+(b*c-b*d))+(-a*f+(e*(f-c))) by RLVECT_1:def 11
    .= (a*d+b*(c-d))+(-a*f+(e*(f-c))) by VECTSP_1:11
    .= -(-a*d+-b*(c-d))+(-a*f+(e*(f-c))) by Lm12
    .= -(-a*d+-b*(c-d))+-(--a*f+-(e*(f-c))) by Lm12
    .= -(-a*d+-b*(c-d))+-(a*f+-(e*(f-c))) by RLVECT_1:17
    .= -((-a*d+-b*(c-d))+(a*f+-(e*(f-c)))) by RLVECT_1:31
    .= -((-a*d+-b*(c-d))+-(-a*f+--(e*(f-c)))) by Lm12
    .= -((-a*d+-b*(c-d))-(-a*f+--(e*(f-c)))) by RLVECT_1:def 11
    .= -((-a*d+-b*(c-d))-(-a*f+-((-(f-c))*e))) by VECTSP_1:9
    .= -((-a*d+-b*(c-d))-(-a*f+-(e*(c-f)))) by Lm1
    .= - 0.F by A1,A2,Lm11
    .= 0.F by RLVECT_1:12;
end;

Lm14: a-(a+b+-c) = c-b
proof
  thus a-(a+b+-c) = a-(a+(b+-c)) by RLVECT_1:def 3
    .= a-(a+(b-c)) by RLVECT_1:def 11
    .= a+-(a+(b-c)) by RLVECT_1:def 11
    .= a+(-a+-(b-c)) by RLVECT_1:31
    .= (a+-a)+-(b-c) by RLVECT_1:def 3
    .= 0.F + -(b-c) by RLVECT_1:def 10
    .= -(b-c) by RLVECT_1:4
    .= c-b by Lm1;
end;

Lm15: (a-b)*(c-(c+h+-g))-(e-(e+b+-a))*(g-h) = 0.F
proof
  c-(c+h+-g) = g-h & e-(e+b+-a) = a-b by Lm14;
  hence thesis by RLVECT_1:15;
end;

::
::               1. A THREE-DIMENSION CARTESIAN GROUP
::

reserve x,y for Element of [:the carrier of F,the carrier of F,the carrier of
  F:];

deffunc 3F(Field) = [:the carrier of $1,the carrier of $1,the carrier of $1:];

definition
  let F;
  func c3add(F) -> BinOp of [:the carrier of F,the carrier of F,the carrier of
  F:] means
  :Def1:
  it.(x,y) = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3];
  existence
  proof
    deffunc O(Element of 3F(F),Element of 3F(F))
     = [$1`1_3+$2`1_3,$1`2_3+$2`2_3,$1`3_3+
    $2`3_3];
    consider f be BinOp of 3F(F) such that
A1: f.(x,y) = O(x,y) from BINOP_1:sch 4;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be BinOp of 3F(F) such that
A2: f.(x,y) = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3] and
A3: g.(x,y) = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3];
    f.(x,y) = g.(x,y)
    proof
      thus f.(x,y)=[x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3] by A2
        .= g.(x,y) by A3;
    end;
    hence f = g by BINOP_1:2;
  end;
end;

definition
  let F,x,y;
  func x+y -> Element of [:the carrier of F,the carrier of F,the carrier of F
  :] equals
  (c3add(F)).(x,y);
  coherence;
end;

theorem
  x+y = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3] by Def1;

theorem Th2:
  [a,b,c]+[f,g,h]=[a+f,b+g,c+h]
proof
  set abc = [a,b,c] ,fgh = [f,g,h];
A1: abc`3_3=c & fgh`1_3=f;
A2: fgh`2_3=g & fgh`3_3=h;
  abc`1_3=a & abc`2_3=b;
  hence thesis by A1,A2,Def1;
end;

definition
  let F;
  func c3compl(F) -> UnOp of [:the carrier of F,the carrier of F,the carrier
  of F:] means
  :Def3:
  it.(x) = [-x`1_3,-x`2_3,-x`3_3];
  existence
  proof
    deffunc O(Element of 3F(F)) = [-$1`1_3,-$1`2_3,-$1`3_3];
    consider f be UnOp of 3F(F) such that
A1: f.(x) = O(x) from FUNCT_2:sch 4;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be UnOp of 3F(F) such that
A2: f.(x) = [-x`1_3,-x`2_3,-x`3_3] and
A3: g.(x) = [-x`1_3,-x`2_3,-x`3_3];
    f.(x) = g.(x)
    proof
      thus f.(x) = [-x`1_3,-x`2_3,-x`3_3] by A2
        .= g.(x) by A3;
    end;
    hence f = g by FUNCT_2:63;
  end;
end;

definition
  let F,x;
  func -x -> Element of [:the carrier of F,the carrier of F,the carrier of F:]
  equals
  (c3compl(F)).(x);
  coherence;
end;

theorem
  -x = [-x`1_3,-x`2_3,-x`3_3] by Def3;

::
::                      2. PARALLELITY STRUCTURE
::

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

registration
  cluster non empty for ParStr;
  existence
  proof
    set A = the non empty set,R = the Relation of [:A,A:];
    take ParStr(#A,R#);
    thus the carrier of ParStr(#A,R#) is non empty;
  end;
end;

reserve F for Field;
reserve PS for non empty ParStr;

definition
  let PS;
  let a,b,c,d be Element of PS;
  pred a,b '||' c,d means

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

definition
  let F;
  func C_3(F) -> set equals
  [:the carrier of F,the carrier of F,the carrier of F:];
  coherence;
end;

registration
  let F;
  cluster C_3(F) -> non empty;
  coherence;
end;

definition
  let F;
  func 4C_3(F) -> set equals
  [:[:C_3(F),C_3(F):],[:C_3(F),C_3(F):]:];
  coherence;
end;

registration
  let F;
  cluster 4C_3(F) -> non empty;
  coherence;
end;

reserve x for set,
  a,b,c,d,e,f,g,h,i,j,k,l for Element of [:the carrier of F,
  the carrier of F,the carrier of F:];

definition
  let F;
  func PRs(F) -> set means
  :Def8:
  for x being object holds x in it iff
  x in 4C_3(F) & ex a,b,c,d st x =[[a,b],[c,d]] &
  (a`1_3-b`1_3)*(c`2_3-d`2_3) - (c`1_3-d`1_3)*(a`2_3-b`2_3) = 0.F &
  (a`1_3-b`1_3)*(c`3_3-d`3_3) - (c`1_3-d`1_3)*(a`3_3-b`3_3) = 0.F &
  (a`2_3-b`2_3)*(c`3_3-d`3_3) - (c`2_3-d`2_3)*(a`3_3-b`3_3) = 0.F;
  existence
  proof
    defpred P[object] means ex a,b,c,d st $1 = [[a,b],[c,d]] &
     (a`1_3-b`1_3)*(c`2_3-d`2_3) -
     (c`1_3-d`1_3)*(a`2_3-b`2_3) = 0.F &
     (a`1_3-b`1_3)*(c`3_3-d`3_3) - (c`1_3-d`1_3)*(a`3_3-b`3_3) = 0.F &
     (a`2_3-b`2_3)*(c`3_3-d`3_3) - (c`2_3-d`2_3)*(a`3_3-b`3_3) = 0.F;
    thus ex X be set st for x be object holds x in X iff x in 4C_3(F) & P[x]
      from XBOOLE_0:sch 1;
  end;
  uniqueness
  proof
    defpred CB[object] means $1 in 4C_3(F) &
  ex a,b,c,d st $1 = [[a,b],[c,d]] &
   (a`1_3-b`1_3)*(c`2_3-d`2_3) - (c`1_3-d`1_3)*(a`2_3-b`2_3) = 0.F &
   (a`1_3-b`1_3)*(c`3_3-d`3_3) - (c`1_3-d`1_3)*(a`3_3-b`3_3) = 0.F &
   (a`2_3-b`2_3)*(c`3_3-d`3_3) - (c`2_3-d`2_3)*(a`3_3-b`3_3) = 0.F;
    let H1,H2 be set such that
A1: for x being object holds x in H1 iff CB[x] and
A2: for x being object holds x in H2 iff CB[x];
    for x being object holds x in H1 iff x in H2
    proof let x be object;
      x in H1 iff CB[x] by A1;
      hence thesis by A2;
    end;
    hence thesis by TARSKI:2;
  end;
end;

theorem Th4:
  PRs(F) c= [:[:C_3(F),C_3(F):],[:C_3(F),C_3(F):]:]
proof
  let x be object;
  4C_3(F) = [:[:C_3(F),C_3(F):],[:C_3(F),C_3(F):]:];
  hence thesis by Def8;
end;

definition
  let F;
  func PR(F) -> Relation of [:C_3 F,C_3 F:] equals
  PRs(F);
  coherence by Th4;
end;

definition
  let F;
  func MPS(F) -> ParStr equals
  ParStr (# C_3(F),PR(F) #);
  correctness;
end;

registration
  let F;
  cluster MPS(F) -> strict non empty;
  coherence;
end;

theorem
  the carrier of MPS(F) = C_3(F);

theorem
  the CONGR of MPS(F) = PR(F);

reserve a,b,c,d,p,q,r,s for Element of MPS(F);

theorem
  a,b '||' c,d iff [[a,b],[c,d]] in PR(F);

theorem
  [[a,b],[c,d]] in PR(F) iff ([[a,b],[c,d]] in 4C_3(F) &
   ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] &
    (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
    (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
    (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F) by Def8;

theorem Th9:
  a,b '||' c,d iff ([[a,b],[c,d]] in 4C_3(F) &
  ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] &
  (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
  (e`1_3-f`1_3)*(g`3_3-
h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
   (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) =
  0.F)
by Def8;

theorem
  the carrier of MPS(F) = [:the carrier of F,the carrier of F,the
  carrier of F:];

theorem
  [[a,b],[c,d]] in 4C_3(F);

theorem Th12:
  a,b '||' c,d iff
 ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] & (e`1_3-f`1_3)
*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
   (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f
  `3_3) = 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F
proof
  [[a,b],[c,d]] in 4C_3(F);
  hence thesis by Th9;
end;

theorem Th13:
  a,b '||' b,a
proof
  consider e,f such that
A1: [[e,f],[f,e]] = [[a,b],[b,a]];
A2: (e`2_3-f`2_3)*(f`3_3-e`3_3) - (f`2_3-e`2_3)*(e`3_3-f`3_3) = 0.F by Lm2;
  (e`1_3-f`1_3)*(f`2_3-e`2_3) - (f`1_3-e`1_3)*(e`2_3-f`2_3) = 0.F &
   (e`1_3-f`1_3)*(f`3_3-e`3_3) -
  (f`1_3 -e`1_3)*(e`3_3-f`3_3) = 0.F by Lm2;
  hence thesis by A1,A2,Th12;
end;

theorem Th14:
  a,b '||' c,c
proof
  consider e,f,g such that
A1: [[e,f],[g,g]] = [[a,b],[c,c]];
A2: (e`2_3-f`2_3)*(g`3_3-g`3_3) - (g`2_3-g`2_3)*(e`3_3-f`3_3) = 0.F by Lm3;
  (e`1_3-f`1_3)*(g`2_3-g`2_3) - (g`1_3-g`1_3)*(e`2_3-f`2_3) = 0.F &
  (e`1_3-f`1_3)*(g`3_3-g`3_3) -
  (g`1_3 -g`1_3)*(e`3_3-f`3_3) = 0.F by Lm3;
  hence thesis by A1,A2,Th12;
end;

theorem Th15:
  a,b '||' p,q & a,b '||' r,s implies p,q '||' r,s or a=b
proof
  defpred CB[(Element of 3F(F)),(Element of 3F(F)), (Element of 3F(F)),Element
of 3F(F)] means ($1`1_3-$2`1_3)*($3`2_3-$4`2_3) -
  ($3`1_3-$4`1_3)*($1`2_3-$2`2_3) = 0.F & ($1`1_3
-$2`1_3)*($3`3_3-$4`3_3) - ($3`1_3-$4`1_3)*($1`3_3-$2`3_3) = 0.F &
   ($1`2_3-$2`2_3)*($3`3_3-$4`3_3) -
  ($3`2_3-$4`2_3)*($1`3_3-$2`3_3) = 0.F;
  assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s;
  consider e,f,g,h such that
A3: [[e,f],[g,h]] = [[a,b],[p,q]] and
A4: CB[e,f,g,h] by A1,Th12;
  consider i,j,k,l such that
A5: [[i,j],[k,l]] = [[a,b],[r,s]] and
A6: CB[i,j,k,l] by A2,Th12;
A7: i = a & j = b by A5,MCART_1:93;
A8: k = r & l = s by A5,MCART_1:93;
  set A = e`1_3-f`1_3, B = e`2_3-f`2_3, C = e`3_3-f`3_3, D = g`1_3-h`1_3,
   E = g`2_3-h`2_3, K = g`3_3
  -h`3_3, G = k`1_3-l`1_3, H = k`2_3-l`2_3, I = k`3_3-l`3_3;
A9: e = a & f = b by A3,MCART_1:93;
A10: g = p & h = q by A3,MCART_1:93;
  now
    assume
A11: a <> b;
    now
AA: for X1,X2,X3 being non empty set
  for x being Element of [:X1,X2,
  X3:] holds x = [x`1_3,x`2_3,x`3_3];
      e = [e`1_3,e`2_3,e`3_3];
      then
A12:  e`1_3 <> f`1_3 or e`2_3 <> f`2_3 or e`3_3 <> f`3_3 by A9,A11,AA;
      per cases by A12,RLVECT_1:21;
      case
A13:    A <> 0.F;
        hence D*H-G*E = 0.F by A4,A6,A9,A7,Lm4;
        thus
A14:    D*I-G*K = 0.F by A4,A6,A9,A7,A13,Lm4;
        E*I = ((D*B)*A")*I & H*K = ((G*B)*A")*K by A4,A6,A9,A7,A13,VECTSP_1:30;
        hence E*I-H*K = 0.F by A14,Lm8;
      end;
      case
A15:    B <> 0.F;
        hence D*H-G*E = 0.F by A4,A6,A9,A7,Lm6;
        thus
A16:    E*I-H*K = 0.F by A4,A6,A9,A7,A15,Lm4;
        D*I = ((E*A)*B")*I & G*K = ((H*A)*B")*K by A4,A6,A9,A7,A15,VECTSP_1:30;
        hence D*I-G*K = 0.F by A16,Lm8;
      end;
      case
A17:    C <> 0.F;
        hence E*I-H*K = 0.F by A4,A6,A9,A7,Lm6;
A18:    D*H = ((K*A)*C")*H & G*E = ((I*A)*C")*E by A4,A6,A9,A7,A17,VECTSP_1:30;
        K*H - I*E = 0.F by A4,A6,A9,A7,A17,Lm6;
        hence D*H-G*E = 0.F by A18,Lm8;
        thus D*I-G*K = 0.F by A4,A6,A9,A7,A17,Lm6;
      end;
    end;
    hence ex g,h,k,l st [[g,h],[k,l]] = [[p,q],[r,s]] & CB[g,h,k,l] by A10,A8;
  end;
  hence thesis by Th12;
end;

theorem Th16:
  a,b '||' a,c implies b,a '||' b,c
proof
  assume a,b '||' a,c;
  then consider e,f,g,h such that
A1: [[e,f],[g,h]] = [[a,b],[a,c]] and
A2: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
  (e`1_3-f`1_3)*(g`3_3-h`3_3
  ) - (g`1_3 -h`1_3)*(e`3_3-f`3_3) = 0.F and
A3: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F by Th12;
A4: e = a by A1,MCART_1:93;
A5: g = a by A1,MCART_1:93;
  then
A6: (f`2_3-e`2_3)*(f`3_3-h`3_3) - (f`2_3-h`2_3)*(f`3_3-e`3_3) = 0.F
   by A3,A4,Lm13;
  f = b by A1,MCART_1:93;
  then
A7: [[f,e],[f,h]] = [[b,a],[b,c]] by A1,A4,MCART_1:93;
  (f`1_3-e`1_3)*(f`2_3-h`2_3) - (f`1_3-h`1_3)*(f`2_3-e`2_3) = 0.F &
   (f`1_3-e`1_3)*(f`3_3-h`3_3) -
  (f`1_3 -h`1_3)*(f`3_3-e`3_3) = 0.F by A2,A4,A5,Lm13;
  hence thesis by A7,A6,Th12;
end;

theorem Th17:
  ex d st a,b '||' c,d & a,c '||' b,d
proof
  consider e,f,g such that
A1: e = a & f = b & g = c;
  set h = g+f+-e;
  reconsider d = h as Element of MPS(F);
A2: [[e,f],[g,h]] = [[a,b],[c,d]] by A1;
  take d;
  g+f = [g`1_3+f`1_3,g`2_3+f`2_3,g`3_3+f`3_3] & -e = [-e`1_3,-e`2_3,-e`3_3]
    by Def1,Def3;
  then
A3: h = [g`1_3+f`1_3+-e`1_3,g`2_3+f`2_3+-e`2_3,g`3_3+f`3_3+-e`3_3] by Th2;
  then
A4: h`1_3 = g`1_3+f`1_3+-e`1_3;
A5: h`3_3 = g`3_3+f`3_3+(-e`3_3) by A3;
  then
A6: (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F by A4,Lm15;
A7: (e`1_3-g`1_3)*(f`3_3-h`3_3) - (f`1_3-h`1_3)*(e`3_3-g`3_3) = 0.F
     by A4,A5,Lm15;
A8: h`2_3 = g`2_3+f`2_3+-e`2_3 by A3;
  then
A9: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F by A5,Lm15;
  (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F
     by A4,A8,Lm15;
  hence a,b '||' c,d by A2,A6,A9,Th12;
A10: [[e,g],[f,h]] = [[a,c],[b,d]] by A1;
A11: (e`2_3-g`2_3)*(f`3_3-h`3_3) - (f`2_3-h`2_3)*(e`3_3-g`3_3) = 0.F
    by A8,A5,Lm15;
  (e`1_3-g`1_3)*(f`2_3-h`2_3) - (f`1_3-h`1_3)*(e`2_3-g`2_3) = 0.F
     by A4,A8,Lm15;
  hence thesis by A10,A7,A11,Th12;
end;

::
::                  3. DEFINITION OF PARALLELITY SPACE
::

definition
  let IT be non empty ParStr;
  attr IT is ParSp-like means
  :Def11:
  for a,b,c,d,p,q,r,s being Element of IT
  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
  IT st a,b '||' c,x & a,c '||' b,x;
end;

registration
  cluster strict ParSp-like for non empty ParStr;
  existence
  proof
    set F = the Field;
    for a,b,c,d,p,q,r,s being Element of MPS(F) 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 MPS(F) st a,b '||' c,x &
    a,c '||' b,x by Th13,Th14,Th15,Th16,Th17;
    then MPS(F) is ParSp-like;
    hence thesis;
  end;
end;

definition
  mode ParSp is ParSp-like non empty ParStr;
end;

reserve PS for ParSp,
  a,b,c,d,p,q,r,s for Element of PS;

theorem Th18:
  a,b '||' a,b
proof
  b,a '||' b,b by Def11;
  hence thesis by Def11;
end;

theorem Th19:
  a,b '||' c,d implies c,d '||' a,b
proof
  assume
A1: a,b '||' c,d;
  a,b '||' a,b by Th18;
  then a<>b implies c,d '||' a,b by A1,Def11;
  hence thesis by Def11;
end;

theorem Th20:
  a,a '||' b,c
proof
  b,c '||' a,a by Def11;
  hence thesis by Th19;
end;

theorem Th21:
  a,b '||' c,d implies b,a '||' c,d
proof
  assume
A1: a,b '||' c,d;
  a,b '||' b,a by Def11;
  then a<>b implies b,a '||' c,d by A1,Def11;
  hence thesis by A1;
end;

theorem Th22:
  a,b '||' c,d implies a,b '||' d,c
proof
  assume a,b '||' c,d;
  then c,d '||' a,b by Th19;
  then d,c '||' a,b by Th21;
  hence thesis by Th19;
end;

theorem Th23:
  a,b '||' c,d implies b,a '||' c,d & a,b '||' d,c & b,a '||' d,c
  & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a
proof
  assume a,b '||' c,d;
  then c,d '||' a,b by Th19;
  then
A1: d,c '||' a,b by Th21;
  then
A2: d,c '||' b,a by Th22;
  then c,d '||' b,a by Th21;
  hence thesis by A1,A2,Th19,Th21;
end;

theorem Th24:
  a,b '||' a,c implies a,c '||' a,b & b,a '||' a,c & a,b '||' c,a
& a,c '||' b,a & b,a '||' c,a & c,a '||' a,b & c,a '||' b,a & b,a '||' b,c & a,
  b '||' b,c & b,a '||' c,b & b,c '||' b,a & a,b '||' c,b & c,b '||' b,a & b,c
'||' a,b & c,b '||' a,b & c,a '||' c,b & a,c '||' c,b & c,a '||' b,c & a,c '||'
  b,c & c,b '||' c,a & b,c '||' c,a & c,b '||' a,c & b,c '||' a,c
proof
  assume
A1: a,b '||' a,c;
  then a,c '||' a,b by Th19;
  then
A2: c,a '||' c,b by Def11;
  b,a '||' b,c by A1,Def11;
  hence thesis by A1,A2,Th23;
end;

theorem
  a=b or c = d or a=c & b=d or a=d & b=c implies a,b '||' c,d by Def11,Th18
,Th20;

theorem Th26:
  a<>b & p,q '||' a,b & a,b '||' r,s implies p,q '||' r,s
proof
  assume that
A1: a<>b and
A2: p,q '||' a,b and
A3: a,b '||' r,s;
  a,b '||' p,q by A2,Th23;
  hence thesis by A1,A3,Def11;
end;

theorem
  not a,b '||' a,c implies a<>b & b<>c & c <>a by Def11,Th18,Th20;

theorem
  not a,b '||' c,d implies a<>b & c <>d by Def11,Th20;

theorem Th29:
  not a,b '||' a,c implies not a,c '||' a,b & not b,a '||' a,c &
not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not
c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c
  '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b
  '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c
  '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c
  '||' a,c
proof
  assume
A1: not a,b '||' a,c;
  assume not thesis;
  then
  a,c '||' a,b or a,b '||' a,c or a,b '||' a,c or a,c '||' a,b or a,b '||'
a,c or a,c '||' a,b or a,c '||' a,b or b,a '||' b,c or b,a '||' b,c or b,a '||'
b,c or b,c '||' b,a or b,a '||' b,c or b,c '||' b,a or b,c '||' b,a or b,c '||'
b,a or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,b '||'
  c,a or c,b '||' c,a or c,b '||' c,a or c,b '||' c,a by Th23;
  hence contradiction by A1,Th24;
end;

theorem Th30:
  not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p<>q & r<>s
  implies not p,q '||' r,s
proof
  assume that
A1: not a,b '||' c,d and
A2: a,b '||' p,q and
A3: c,d '||' r,s and
A4: p<>q and
A5: r<>s;
  assume p,q '||' r,s;
  then a,b '||' r,s by A2,A4,Th26;
  then
A6: r,s '||' a,b by Th23;
  r,s '||' c,d by A3,Th23;
  hence contradiction by A1,A5,A6,Def11;
end;

theorem Th31:
  not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r &
  p<>q implies not p,q '||' p,r
proof
  assume that
A1: not a,b '||' a,c and
A2: a,b '||' p,q and
A3: a,c '||' p,r and
A4: b,c '||' q,r and
A5: p<>q;
  now
    assume p=r;
    then
A6: p,q '||' b,c by A4,Th23;
    p,q '||' b,a by A2,Th23;
    then b,a '||' b,c by A5,A6,Def11;
    hence contradiction by A1,Th24;
  end;
  hence thesis by A1,A2,A3,A5,Th30;
end;

theorem Th32:
  not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r implies p=r
proof
  assume that
A1: ( not a,b '||' a,c)& a,c '||' p,r and
A2: b,c '||' p,r;
A3: p,r '||' b,c by A2,Th23;
  ( not a,c '||' b,c)& p,r '||' a,c by A1,Th23,Th29;
  hence thesis by A3,Def11;
end;

theorem Th33:
  not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s implies r=s
proof
  assume that
A1: ( not p,q '||' p,r)& p,r '||' p,s and
A2: q,r '||' q,s;
A3: r,s '||' r,q by A2,Th29;
  ( not r,p '||' r,q)& r,s '||' r,p by A1,Th29;
  hence thesis by A3,Def11;
end;

theorem
  not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c
  '||' q,r & b,c '||' q,s implies r=s
proof
  assume that
A1: not a,b '||' a,c and
A2: a,b '||' p,q and
A3: a,c '||' p,r and
A4: a,c '||' p,s and
A5: b,c '||' q,r and
A6: b,c '||' q,s;
A7: now
    b<>c by A1,Th18;
    then
A8: q,r '||' q,s by A5,A6,Def11;
    a<>c by A1,Def11;
    then
A9: p,r '||' p,s by A3,A4,Def11;
    assume p<>q;
    then not p,q '||' p,r by A1,A2,A3,A5,Th31;
    hence thesis by A9,A8,Th33;
  end;
  p=q implies p=r & p=s by A1,A3,A4,A5,A6,Th32;
  hence thesis by A7;
end;

theorem Th35:
  a,b '||' a,c & a,b '||' a,d implies a,b '||' c,d
proof
  assume that
A1: a,b '||' a,c and
A2: a,b '||' a,d;
  now
    assume that
A3: a<>b and
A4: a<>c;
    a,c '||' a,d by A1,A2,A3,Def11;
    then a,c '||' c,d by Th24;
    hence thesis by A1,A4,Th26;
  end;
  hence thesis by A2,Th20;
end;

theorem
  (for a,b holds a=b) implies for p,q,r,s holds p,q '||' r,s
proof
  assume
A1: for a,b holds a=b;
  let p,q,r,s;
  r=s by A1;
  hence thesis by Def11;
end;

theorem
  (ex a,b st a<>b & for c holds a,b '||' a,c) implies for p,q,r,s holds
  p,q '||' r,s
proof
  assume ex a,b st a<>b & for c holds a,b '||' a,c;
  then consider a,b such that
A1: a<>b and
A2: for c holds a,b '||' a,c;
  let p,q,r,s;
  a,b '||' a,r & a,b '||' a,s by A2;
  then
A3: a,b '||' r,s by Th35;
  a,b '||' a,p & a,b '||' a,q by A2;
  then a,b '||' p,q by Th35;
  hence thesis by A1,A3,Def11;
end;

theorem
  not a,b '||' a,c & p<>q implies not p,q '||' p,a or not p,q '||' p,b
  or not p,q '||' p,c
proof
  assume that
A1: not a,b '||' a,c and
A2: p<>q;
  assume
A3: not thesis;
  then p,a '||' p,b by A2,Def11;
  then
A4: a,p '||' a,b by Th24;
  p,a '||' p,c by A2,A3,Def11;
  then
A5: a,p '||' a,c by Th24;
  a<>p by A1,A2,A3,Def11;
  hence contradiction by A1,A4,A5,Def11;
end;