:: Construction of a bilinear antisymmetric form in symplectic vector space
::  by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: Copyright (c) 1990-2012 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, ORDERS_2, STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1,
      FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_0, XXREAL_0, CARD_1, TARSKI, RLVECT_1,
      SUPINF_2, ARYTM_1, ARYTM_3, GROUP_1, MESFUNC1, SYMSP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, DOMAIN_1, NUMBERS,
      STRUCT_0, ORDERS_2, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1,
      RELSET_1;
 constructors BINOP_1, DOMAIN_1, RLVECT_1, VECTSP_1, ORDERS_2;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, STRUCT_0, RLVECT_1, ALGSTR_0;
 theorems VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, GROUP_1, ORDERS_2, XTUPLE_0;
 schemes BINOP_1, XBOOLE_0;

begin :: 1. SYMPLECTIC VECTOR SPACE STRUCTURE

reserve F for Field;

definition
  let F;
  struct (RelStr,VectSpStr over F) SymStr over F (# carrier -> set, addF ->
BinOp of the carrier, ZeroF -> Element of the carrier, lmult -> Function of [:
the carrier of F, the carrier:], the carrier, InternalRel -> Relation of the
    carrier #);
end;

registration
  let F;
  cluster non empty for SymStr over F;
  existence
  proof

set X = the non empty set,a = the BinOp of X,Z = the Element of X,l =the
Function of [:the carrier of F, X:], X,r = the Relation of X;
    take SymStr(#X,a,Z,l,r#);
    thus the carrier of SymStr(#X,a,Z,l,r#) is non empty;
  end;
end;

notation
  let F;
  let S be SymStr over F;
  let a,b be Element of S;
  synonym a _|_ b for a <= b;
end;

set X = {0};
reconsider o = 0 as Element of {0} by TARSKI:def 1;
deffunc F(Element of {0},Element of {0}) = o;
consider md being BinOp of {0} such that
Lm1: for x,y being Element of {0} holds md.(x,y) = F(x,y) from BINOP_1:sch
4;

Lm2: now
  defpred P[set] means ex a,b being Element of X st $1 = [a,b] & b = o;
  set CV = [:X,X:];
  let F;
  consider mo being set such that
A1: for x being set holds x in mo iff x in CV & P[x] from XBOOLE_0:sch 1;
  mo c= CV
  proof
    let x be set;
    thus thesis by A1;
  end;
  then reconsider mo as Relation of X;
  take mo;
  thus for x being set holds x in mo iff x in CV & ex a,b being Element of X
  st x = [a,b] & b = o by A1;
end;

registration
  let F;
  let X be non empty set, md be BinOp of X, o be Element of X, mF be Function
  of [:the carrier of F, X:], X, mo be Relation of X;
  cluster SymStr (# X,md,o,mF,mo #) -> non empty;
  coherence;
end;

Lm3: for mF being Function of [:the carrier of F,X:],X, mo being Relation of X
holds SymStr (# X,md,o,mF,mo #) is Abelian add-associative right_zeroed
right_complementable
proof
  let mF be Function of [:the carrier of F,X:],X;
  let mo be Relation of X;
  set H = SymStr (# X,md,o,mF,mo #);
  thus H is Abelian
  proof
    let x,y be Element of H;
    reconsider x,y as Element of X;
    md.(x,y) = o by Lm1;
    hence thesis by Lm1;
  end;
  thus H is add-associative
  proof
    let x,y,z be Element of H;
    reconsider x,y,z as Element of X;
    md.(x,md.(y,z)) = o by Lm1;
    hence thesis by Lm1;
  end;
  thus H is right_zeroed
  proof
    let x be Element of H;
    reconsider x as Element of X;
    md.(x,0.H) = o by Lm1;
    hence thesis by TARSKI:def 1;
  end;
  let x be Element of H;
  take -x;
  thus thesis by Lm1;
end;

registration
  let F;
  cluster Abelian add-associative right_zeroed right_complementable for
non empty
    SymStr over F;
  existence
  proof
    set mo = the Relation of X;
    set mF = the Function of [:the carrier of F,X:],X;
    SymStr (# X,md,o,mF,mo #) is Abelian add-associative right_zeroed
    right_complementable by Lm3;
    hence thesis;
  end;
end;

Lm4: now
  let F;
  let mF be Function of [:the carrier of F,X:],X such that
A1: for a being Element of F for x being Element of X holds mF.(a,x) = o;
  let mo be Relation of X;
  let MPS be Abelian add-associative right_zeroed right_complementable non
  empty SymStr over F such that
A2: MPS = SymStr (# X,md,o,mF,mo #);
  for x,y being Element of F for v,w being Element of MPS holds x*(v+w) =
  x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1_F)*v = v
  proof
    let x,y be Element of F;
    let v,w be Element of MPS;
A3: (x*y)*v = x*(y*v)
    proof
      set z = x*y;
A4:   z*v = mF.(z,v) by A2,VECTSP_1:def 12;
      reconsider v as Element of MPS;
      reconsider v as Element of MPS;
A5:   (x*y)*v = o by A1,A2,A4;
      reconsider v as Element of MPS;
A6:   mF.(y,v) = o by A1,A2;
      reconsider v as Element of MPS;
      y*v = o by A2,A6,VECTSP_1:def 12;
      then x*(y*v) = mF.(x,o) by A2,VECTSP_1:def 12;
      hence thesis by A1,A5;
    end;
A7: x*(v+w) = x*v+x*w
    proof
      reconsider v,w as Element of X by A2;
A8:   md.(v,w) = o by Lm1;
      reconsider v,w as Element of MPS;
      x*(v+w) = mF.(x,o) by A2,A8,VECTSP_1:def 12;
      then
A9:   x*(v+w) = o by A1;
      mF.(x,v) = o by A1;
      then
A10:  x*v = o by A2,VECTSP_1:def 12;
      mF.(x,w) = o by A1;
      then
A11:  x*w = o by A2,VECTSP_1:def 12;
      o = 0.MPS by A2;
      hence thesis by A9,A10,A11,RLVECT_1:4;
    end;
A12: (x+y)*v = x*v+y*v
    proof
      set z = x+y;
A13:  z*v = mF.(z,v) by A2,VECTSP_1:def 12;
      reconsider v as Element of MPS;
      reconsider v as Element of MPS;
A14:  (x+y)*v = o by A1,A2,A13;
      reconsider v as Element of MPS;
A15:  mF.(x,v) = o by A1,A2;
      reconsider v as Element of MPS;
A16:  x*v = o by A2,A15,VECTSP_1:def 12;
      reconsider v as Element of MPS;
A17:  mF.(y,v) = o by A1,A2;
A18:  o = 0.MPS by A2;
      reconsider v as Element of MPS;
      y*v = o by A2,A17,VECTSP_1:def 12;
      hence thesis by A14,A16,A18,RLVECT_1:4;
    end;
    (1_F)*v = v
    proof
      set one1 = 1_F;
A19:  one1*v = mF.(one1,v) by A2,VECTSP_1:def 12;
      reconsider v as Element of MPS;
      mF.(one1,v) = o by A1,A2;
      hence thesis by A2,A19,TARSKI:def 1;
    end;
    hence thesis by A7,A12,A3;
  end;
  hence MPS is vector-distributive scalar-distributive scalar-associative
  scalar-unital by VECTSP_1:def 14,def 15,def 16,def 17;
end;

Lm5: now
  set CV = [:X,X:];
  let F;
  let mF be Function of [:the carrier of F,X:],X;
  let mo be Relation of X such that
A1: for x being set holds x in mo iff x in CV & ex a,b being Element of
  X st x = [a,b] & b = o;
  let MPS be Abelian add-associative right_zeroed right_complementable non
  empty SymStr over F such that
A2: MPS = SymStr (# X,md,o,mF,mo #);
  thus for a being Element of MPS holds (a <> 0.MPS implies ex p being Element
  of MPS st not p _|_ a ) by A2,TARSKI:def 1;
A3: for a,b being Element of MPS holds a _|_ b iff [a,b] in CV & ex c,d
  being Element of X st [a,b] = [c,d] & d = o
  proof
    let a,b be Element of MPS;
    a _|_ b iff [a,b] in mo by A2,ORDERS_2:def 5;
    hence thesis by A1;
  end;
A4: for a,b being Element of MPS holds a _|_ b iff b = o
  proof
    let a,b be Element of MPS;
A5: b = o implies a _|_ b
    proof
      consider c,d being Element of MPS such that
A6:   c = a & d = b;
      assume
A7:   b = o;
      [a,b] = [c,d] by A6;
      hence thesis by A2,A3,A7;
    end;
    a _|_ b implies b = o
    proof
      assume a _|_ b;
      then ex c,d being Element of X st [a,b] = [c,d] & d = o by A3;
      hence thesis by XTUPLE_0:1;
    end;
    hence thesis by A5;
  end;
  thus for a,b being Element of MPS for l being Element of F holds (a _|_ b
  implies l*a _|_ b)
  proof
    let a,b be Element of MPS;
    let l be Element of F;
    assume a _|_ b;
    then b = o by A4;
    hence thesis by A4;
  end;
  thus for a,b,c being Element of MPS holds (b _|_ a & c _|_ a implies b+c _|_
  a)
  proof
    let a,b,c be Element of MPS;
    assume that
A8: b _|_ a and
    c _|_ a;
    a = o by A4,A8;
    hence thesis by A4;
  end;
  thus for a,b,x being Element of MPS holds ( not b _|_ a implies ex k being
  Element of F st x-k*b _|_ a)
  proof
    let a,b,x be Element of MPS;
    assume
A9: not b _|_ a;
    assume not thesis;
    a <> o by A4,A9;
    hence contradiction by A2,TARSKI:def 1;
  end;
  let a,b,c be Element of MPS;
  assume that
  a _|_ b+c and
  b _|_ c+a;
  assume not c _|_ a+b;
  then a+b <> o by A4;
  hence contradiction by A2,TARSKI:def 1;
end;

:: 2. SYMPLECTIC VECTOR SPACE

definition
  let F;
  let IT be Abelian add-associative right_zeroed right_complementable non
  empty SymStr over F;
  attr IT is SymSp-like means
  :Def1:
  for a,b,c,x being Element of IT for l
  being Element of F holds (a<>(0.IT) implies ex y being Element of IT st not y
_|_ a ) & (a _|_ b implies l*a _|_ b) & ( b _|_ a & c _|_ a implies b+c _|_ a )
& (not b _|_ a implies ex k being Element of F st x-k*b _|_ a ) & (a _|_ b+c &
  b _|_ c+a implies c _|_ a+b );
end;

registration
  let F;
  cluster SymSp-like vector-distributive scalar-distributive
  scalar-associative scalar-unital strict for
Abelian add-associative right_zeroed
    right_complementable non empty SymStr over F;
  existence
  proof
    deffunc F(Element of F, Element of X) = o;
    consider mF being Function of [:the carrier of F,X:],X such that
A1: for a being Element of F for x being Element of X holds mF.(a,x) =
    F(a,x) from BINOP_1:sch 4;
    consider mo being Relation of X such that
A2: for x being set holds x in mo iff x in [:X,X:] & ex a,b being
    Element of X st x = [a,b] & b = o by Lm2;
    reconsider MPS = SymStr (# X,md,o,mF,mo #) as Abelian add-associative
    right_zeroed right_complementable non empty SymStr over F by Lm3;
    take MPS;
    thus for a,b,c,x being Element of MPS for l being Element of F holds (a<>(
0.MPS) implies ex y being Element of MPS st not y _|_ a ) & (a _|_ b implies l*
a _|_ b) & ( b _|_ a & c _|_ a implies b+c _|_ a ) & (not b _|_ a implies ex k
being Element of F st x-k*b _|_ a ) & (a _|_ b+c & b _|_ c+a implies c _|_ a+b
    ) by A2,Lm5;
    thus MPS is vector-distributive scalar-distributive scalar-associative
    scalar-unital by A1,Lm4;
    thus thesis;
  end;
end;

definition
  let F;
  mode SymSp of F is SymSp-like vector-distributive scalar-distributive
  scalar-associative scalar-unital Abelian add-associative
    right_zeroed right_complementable non empty SymStr over F;
end;

reserve S for SymSp of F;
reserve a,b,c,d,a9,b9,p,q,r,s,x,y,z for Element of S;
reserve k,l for Element of F;

theorem Th1:
  0.S _|_ a
proof
  set 0V = 0.S, 0F = 0.F;
A1: now
    assume not a _|_ a;
    then consider m being Element of F such that
A2: (0V-m*a) _|_ a by Def1;
    0F*(0V-m*a) _|_ a by A2,Def1;
    hence thesis by VECTSP_1:14;
  end;
  now
    assume a _|_ a;
    then 0F*a _|_ a by Def1;
    hence thesis by VECTSP_1:14;
  end;
  hence thesis by A1;
end;

theorem Th2:
  a _|_ b implies b _|_ a
proof
  set 0V = 0.S;
  assume a _|_ b;
  then
A1: a _|_ 0V+b by RLVECT_1:4;
  0V _|_ b+a by Th1;
  then b _|_ a+0V by A1,Def1;
  hence thesis by RLVECT_1:4;
end;

theorem Th3:
  not a _|_ b & c+a _|_ b implies not c _|_ b
proof
  assume that
A1: not a _|_ b and
A2: c+a _|_ b;
  assume not thesis;
  then (-1_F)*c _|_ b by Def1;
  then -c _|_ b by VECTSP_1:14;
  then -c+(c+a) _|_ b by A2,Def1;
  then (c+(-c))+a _|_ b by RLVECT_1:def 3;
  then 0.S+a _|_ b by RLVECT_1:5;
  hence contradiction by A1,RLVECT_1:4;
end;

theorem Th4:
  not b _|_ a & c _|_ a implies not b+c _|_ a
proof
  assume that
A1: not b _|_ a and
A2: c _|_ a;
  (-1_F)*c _|_ a by A2,Def1;
  then
A3: -c _|_ a by VECTSP_1:14;
  assume not thesis;
  then (b+c)+(-c) _|_ a by A3,Def1;
  then b+(c+(-c)) _|_ a by RLVECT_1:def 3;
  then b+0.S _|_ a by RLVECT_1:5;
  hence contradiction by A1,RLVECT_1:4;
end;

theorem Th5:
  not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a
proof
  set 1F = 1.F;
  assume that
A1: not b _|_ a and
A2: not l=0.F;
A3: now
    consider k such that
A4: k*l=1F by A2,VECTSP_1:def 9;
    assume b _|_ l*a;
    then l*a _|_ b by Th2;
    then k*(l*a) _|_ b by Def1;
    then 1F*a _|_ b by A4,VECTSP_1:def 16;
    then a _|_ b by VECTSP_1:def 17;
    hence contradiction by A1,Th2;
  end;
  now
    consider k such that
A5: k*l=1F by A2,VECTSP_1:def 9;
    assume l*b _|_ a;
    then k*(l*b) _|_ a by Def1;
    then 1F*b _|_ a by A5,VECTSP_1:def 16;
    hence contradiction by A1,VECTSP_1:def 17;
  end;
  hence thesis by A3;
end;

theorem Th6:
  a _|_ b implies -a _|_ b
proof
  assume a _|_ b;
  then (-1_F)*a _|_ b by Def1;
  hence thesis by VECTSP_1:14;
end;

theorem Th7:
  not a _|_ c implies not a+b _|_ c or not (1_F+1_F)*a+b _|_ c
proof
  set 1F = 1_F;
  assume
A1: not a _|_ c;
  assume
A2: not thesis;
  then (1F*a+1_F*a)+b _|_ c by VECTSP_1:def 15;
  then (a+1F*a)+b _|_ c by VECTSP_1:def 17;
  then (a+a)+b _|_ c by VECTSP_1:def 17;
  then a+(a+b) _|_ c by RLVECT_1:def 3;
  hence contradiction by A1,A2,Th4;
end;

theorem Th8:
  not a9 _|_ a & a9 _|_ b & not b9 _|_ b & b9 _|_ a implies not a9
  +b9 _|_ a & not a9+b9 _|_ b
proof
  set 0V = 0.S;
  assume that
A1: not a9 _|_ a and
A2: a9 _|_ b and
A3: not b9 _|_ b and
A4: b9 _|_ a;
  assume not thesis;
  then
  a9+b9 _|_ a & (-(1_F))*b9 _|_ a or a9+b9 _|_ b & (-(1_F))*a9 _|_ b by A2,A4
,Def1;
  then a9+b9 _|_ a & -b9 _|_ a or a9+b9 _|_ b & -a9 _|_ b by VECTSP_1:14;
  then (a9+b9)+(-b9) _|_ a or -a9+(a9+b9) _|_ b by Def1;
  then a9+(b9+(-b9)) _|_ a or (-a9+a9)+b9 _|_ b by RLVECT_1:def 3;
  then a9+0V _|_ a or 0V+b9 _|_ b by RLVECT_1:5;
  hence contradiction by A1,A3,RLVECT_1:4;
end;

theorem Th9:
  a<>0.S & b<>0.S implies ex p st not p _|_ a & not p _|_ b
proof
  assume that
A1: a<>0.S and
A2: b<>0.S;
  consider a9 such that
A3: not a9 _|_ a by A1,Def1;
  now
    consider b9 such that
A4: not b9 _|_ b by A2,Def1;
    assume
A5: a9 _|_ b;
    now
      assume b9 _|_ a;
      then ( not a9+b9 _|_ a)& not a9+b9 _|_ b by A3,A5,A4,Th8;
      hence thesis;
    end;
    hence thesis by A4;
  end;
  hence thesis by A3;
end;

theorem Th10:
  1_F+1_F<>0.F & a<>0.S & b<>0.S & c <>0.S implies ex p st not p
  _|_ a & not p _|_ b & not p _|_ c
proof
  assume that
A1: 1_F+1_F<>0.F and
A2: a<>0.S and
A3: b<>0.S and
A4: c <>0.S;
  consider r such that
A5: not r _|_ a and
A6: not r _|_ b by A2,A3,Th9;
  consider s such that
A7: not s _|_ a and
A8: not s _|_ c by A2,A4,Th9;
  now
    assume that
A9: r _|_ c and
A10: s _|_ b;
A11: now
      (1_F+1_F)*r _|_ c by A9,Def1;
      then
A12:  not (1_F+1_F)*r+s _|_ c by A8,Th4;
      not (1_F+1_F)*r _|_ b by A1,A6,Th5;
      then
A13:  not (1_F+1_F)*r+s _|_ b by A10,Th4;
      assume not (1_F+1_F)*r+s _|_ a;
      hence thesis by A13,A12;
    end;
    now
      assume
A14:  not r+s _|_ a;
      ( not r+s _|_ b)& not r+s _|_ c by A6,A8,A9,A10,Th4;
      hence thesis by A14;
    end;
    hence thesis by A5,A11,Th7;
  end;
  hence thesis by A5,A6,A7,A8;
end;

theorem Th11:
  a-b _|_ d & a-c _|_ d implies b-c _|_ d
proof
  assume that
A1: a-b _|_ d and
A2: a-c _|_ d;
  -(a-b) _|_ d by A1,Th6;
  then -a+b _|_ d by VECTSP_1:17;
  then b+(-a)+(a-c) _|_ d by A2,Def1;
  then b+((-a)+(a-c)) _|_ d by RLVECT_1:def 3;
  then b+((-a+a)+(-c)) _|_ d by RLVECT_1:def 3;
  then b+((0.S)+(-c)) _|_ d by RLVECT_1:5;
  hence thesis by RLVECT_1:4;
end;

theorem Th12:
  not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
proof
  assume that
A1: not b _|_ a and
A2: x-k*b _|_ a & x-l*b _|_ a;
  set 1F=1_F;
  k*b-l*b _|_ a by A2,Th11;
  then k*b+((-1F)*(l*b)) _|_ a by VECTSP_1:14;
  then k*b+(((-1F)*l)*b) _|_ a by VECTSP_1:def 16;
  then k*b+(-(l*(1F)))*b _|_ a by VECTSP_1:9;
  then k*b+(-l)*b _|_ a by VECTSP_1:def 8;
  then (k+(-l))*b _|_ a by VECTSP_1:def 15;
  then (k+(-l))"*((k+(-l))*b) _|_ a by Def1;
  then
A3: ((k+(-l))"*(k+(-l)))*b _|_ a by VECTSP_1:def 16;
  assume not thesis;
  then k-l<>0.F by RLVECT_1:21;
  then (1F)*b _|_ a by A3,VECTSP_1:def 10;
  hence contradiction by A1,VECTSP_1:def 17;
end;

theorem Th13:
  1_F+1_F<>0.F implies a _|_ a
proof
  set 1F = 1_F;
  assume
A1: 1_F+1_F<>0.F;
  now
    assume a <> 0.S;
    then consider c such that
A2: not c _|_ a by Def1;
    consider k such that
A3: a-k*c _|_ a by A2,Def1;
    a _|_ a+(-k*c) by A3,Th2;
    then -k*c _|_ a+a by Def1;
    then -k*c _|_ a+(1F)*a by VECTSP_1:def 17;
    then -k*c _|_ (1F)*a+(1F)*a by VECTSP_1:def 17;
    then (-1F)*(k*c) _|_ (1F)*a+(1F)*a by VECTSP_1:14;
    then (-1F)*(k*c) _|_ ((1F)+(1F))*a by VECTSP_1:def 15;
    then ((-1F)*k)*c _|_ ((1F)+(1F))*a by VECTSP_1:def 16;
    then (-(k*(1F)))*c _|_ ((1F)+(1F))*a by VECTSP_1:9;
    then (-k)*c _|_ ((1_F)+(1F))*a by VECTSP_1:def 8;
    then ((1_F)+(1_F))*a _|_ (-k)*c by Th2;
    then ((1_F)+(1_F))"*(((1_F)+(1_F))*a) _|_ (-k)*c by Def1;
    then a _|_ (-k)*c by A1,VECTSP_1:20;
    then
A4: (-k)*c _|_ a by Th2;
    a+(-k)*c _|_ a by A3,VECTSP_1:21;
    hence thesis by A4,Th4;
  end;
  hence thesis by Th1;
end;

::                      5. ORTHOGONAL PROJECTION

definition
  let F;
  let S,a,b,x;
  assume
A1: not b _|_ a;

  func ProJ(a,b,x) -> Element of F means
  :Def2:
  for l being Element of F st x-l*b _|_ a holds it = l;
  existence
  proof
    consider k being Element of F such that
A2: x-k*b _|_ a by A1,Def1;
    take k;
    let l be Element of F;
    assume x-l*b _|_ a;
    hence thesis by A1,A2,Th12;
  end;
  uniqueness
  proof
    let l1,l2 be Element of F such that
A3: for l being Element of F st x-l*b _|_ a holds l1 = l and
A4: for l being Element of F st x-l*b _|_ a holds l2 = l;
    consider k being Element of F such that
A5: x-k*b _|_ a by A1,Def1;
    l1 = k by A3,A5;
    hence thesis by A4,A5;
  end;
end;

theorem Th14:
  not b _|_ a implies x-ProJ(a,b,x)*b _|_ a
proof
  assume
A1: not b _|_ a;
  then ex l being Element of F st x-l*b _|_ a by Def1;
  hence thesis by A1,Def2;
end;

theorem Th15:
  not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x)
proof
  set L = x-ProJ(a,b,x)*b;
A1: l*L = l*x-l*(ProJ(a,b,x)*b) by VECTSP_1:23
    .= l*x-(l*ProJ(a,b,x))*b by VECTSP_1:def 16;
  assume
A2: not b _|_ a;
  then
A3: l*x - ProJ(a,b,l*x)*b _|_ a by Th14;
  L _|_ a by A2,Th14;
  then l*x-(l*ProJ(a,b,x))*b _|_ a by A1,Def1;
  hence thesis by A2,A3,Th12;
end;

theorem Th16:
  not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y)
proof
  set 1F = 1_F;
  set L = (x-ProJ(a,b,x)*b)+(y-ProJ(a,b,y)*b);
A1: L = (((-ProJ(a,b,x)*b)+x)+y)+(-ProJ(a,b,y)*b) by RLVECT_1:def 3
    .= ((x+y)+(-ProJ(a,b,x)*b))+(-ProJ(a,b,y)*b) by RLVECT_1:def 3
    .= (x+y)+((-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by RLVECT_1:def 3
    .= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by VECTSP_1:def 17
    .= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(1F)*(-ProJ (a,b,y)*b)) by VECTSP_1:def 17
    .= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*(-ProJ(a,b,y)*b)) by VECTSP_1:21
    .= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*((-ProJ (a,b,y))*b)) by VECTSP_1:21
    .= (x+y)+(((1F)*(-ProJ(a,b,x)))*b+(1F)*((-ProJ (a,b,y))*b)) by
VECTSP_1:def 16
    .= (x+y)+(((-ProJ(a,b,x))*(1F))*b+((1F)*(-ProJ(a,b,y)))*b) by
VECTSP_1:def 16
    .= (x+y)+((-ProJ(a,b,x))*b+((-ProJ(a,b,y))*(1F))*b) by VECTSP_1:def 8
    .= (x+y)+((-ProJ(a,b,x))*b+(-ProJ(a,b,y))*b) by VECTSP_1:def 8
    .= (x+y)+((-ProJ(a,b,x))+(-ProJ(a,b,y)))*b by VECTSP_1:def 15
    .= (x+y)+(-(ProJ(a,b,x)+ProJ(a,b,y)))*b by RLVECT_1:31
    .= (x+y)-(ProJ(a,b,x)+ProJ(a,b,y))*b by VECTSP_1:21;
  assume
A2: not b _|_ a;
  then x-ProJ(a,b,x)*b _|_ a & y-ProJ(a,b,y)*b _|_ a by Th14;
  then
A3: L _|_ a by Def1;
  (x+y)-ProJ(a,b,x+y)*b _|_ a by A2,Th14;
  hence thesis by A2,A3,A1,Th12;
end;

theorem
  not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x)
proof
  assume that
A1: not b _|_ a and
A2: l <> 0.F;
  set L = x-ProJ(a,l*b,x)*(l*b);
  not l*b _|_ a by A1,A2,Th5;
  then
A3: L _|_ a by Th14;
A4: L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 16;
  x-ProJ(a,b,x)*b _|_ a by A1,Th14;
  then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A3,A4,Th12;
  then ProJ(a,b,x)*l" = ProJ(a,l*b,x)*(l*l") by GROUP_1:def 3;
  then l"*ProJ(a,b,x) = ProJ(a,l*b,x)*(1_F) by A2,VECTSP_1:def 10;
  hence thesis by VECTSP_1:def 8;
end;

theorem Th18:
  not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x)
proof
  assume that
A1: not b _|_ a and
A2: l <> 0.F;
  not b _|_ l*a by A1,A2,Th5;
  then x-ProJ(l*a,b,x)*b _|_ l*a by Th14;
  then l*a _|_ x-ProJ(l*a,b,x)*b by Th2;
  then l"*(l*a) _|_ x-ProJ(l*a,b,x)*b by Def1;
  then (l"*l)*a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 16;
  then 1_F*a _|_ x-ProJ(l*a,b,x)*b by A2,VECTSP_1:def 10;
  then a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 17;
  then
A3: x-ProJ(l*a,b,x)*b _|_ a by Th2;
  x-ProJ(a,b,x)*b _|_ a by A1,Th14;
  hence thesis by A1,A3,Th12;
end;

theorem Th19:
  not b _|_ a & p _|_ a implies ProJ(a,b+p,c) = ProJ(a,b,c) & ProJ
  (a,b,c+p) = ProJ(a,b,c)
proof
  set 0V = 0.S;
  assume that
A1: not b _|_ a and
A2: p _|_ a;
  not b+p _|_ a by A1,A2,Th4;
  then c-ProJ(a,b+p,c)*(b+p) _|_ a by Th14;
  then c-(ProJ(a,b+p,c)*b+ProJ(a,b+p,c)*p) _|_ a by VECTSP_1:def 14;
  then
A3: c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p _|_ a by VECTSP_1:17;
  c+p-ProJ(a,b,c+p)*b _|_ a & -p _|_ a by A1,A2,Th6,Th14;
  then -p+(p+c-ProJ(a,b,c+p)*b) _|_ a by Def1;
  then -p+(p+(c+(-ProJ(a,b,c+p)*b))) _|_ a by RLVECT_1:def 3;
  then (-p+p)+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 3;
  then 0V+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:5;
  then
A4: c-ProJ(a,b,c+p)*b _|_ a by RLVECT_1:4;
  ProJ(a,b+p,c)*p _|_ a by A2,Def1;
  then c+(-ProJ(a,b+p,c)*b)-ProJ(a,b+p,c)*p+ProJ(a,b+p,c)*p _|_ a by A3,Def1;
  then c+(-ProJ(a,b+p,c)*b)+((-ProJ(a,b+p,c)*p)+ProJ(a,b+p,c)*p) _|_ a by
RLVECT_1:def 3;
  then c+(-ProJ(a,b+p,c)*b)+0V _|_ a by RLVECT_1:5;
  then
A5: c-ProJ(a,b+p,c)*b _|_ a by RLVECT_1:4;
  c-ProJ(a,b,c)*b _|_ a by A1,Th14;
  hence thesis by A1,A5,A4,Th12;
end;

theorem Th20:
  not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b ,c)
proof
  assume that
A1: not b _|_ a and
A2: p _|_ b and
A3: p _|_ c;
  b _|_ p by A2,Th2;
  then ProJ(a,b,c)*b _|_ p by Def1;
  then
A4: -(ProJ(a,b,c)*b) _|_ p by Th6;
  c _|_ p by A3,Th2;
  then c+(-(ProJ(a,b,c)*b)) _|_ p by A4,Def1;
  then
A5: p _|_ c-ProJ(a,b,c)*b by Th2;
  c-ProJ(a,b,c)*b _|_ a by A1,Th14;
  then a _|_ c-ProJ(a,b,c)*b by Th2;
  then a+p _|_ c-ProJ(a,b,c)*b by A5,Def1;
  then
A6: c-ProJ(a,b,c)*b _|_ a+p by Th2;
  not a _|_ b by A1,Th2;
  then not a+p _|_ b by A2,Th4;
  then
A7: not b _|_ a+p by Th2;
  then c-ProJ(a+p,b,c)*b _|_ a+p by Th14;
  hence thesis by A7,A6,Th12;
end;

theorem Th21:
  not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_F
proof
  assume that
A1: not b _|_ a and
A2: c-b _|_ a;
  c-(1_F)*b _|_ a & c-ProJ(a,b,c)*b _|_ a by A1,A2,Th14,VECTSP_1:def 17;
  hence thesis by A1,Th12;
end;

theorem Th22:
  not b _|_ a implies ProJ(a,b,b) = 1_F
proof
A1: b-b = 0.S by RLVECT_1:5;
  assume not b _|_ a;
  hence thesis by A1,Th1,Th21;
end;

theorem Th23:
  not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F )
proof
  set 0F = 0.F, 0V = 0.S;
A1: now
    assume that
A2: not b _|_ a and
A3: x _|_ a;
    x+0V _|_ a by A3,RLVECT_1:4;
    then x+(-0V) _|_ a by RLVECT_1:12;
    then
A4: x-0F*b _|_ a by VECTSP_1:14;
    x-ProJ(a,b,x)*b _|_ a by A2,Th14;
    hence ProJ(a,b,x) = 0.F by A2,A4,Th12;
  end;
  now
    assume ( not b _|_ a)& ProJ(a,b,x) = 0.F;
    then x-0F*b _|_ a by Th14;
    then x-0V _|_ a by VECTSP_1:14;
    then x+0V _|_ a by RLVECT_1:12;
    hence x _|_ a by RLVECT_1:4;
  end;
  hence thesis by A1;
end;

theorem Th24:
  not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p)
proof
  assume that
A1: not b _|_ a and
A2: not q _|_ a;
  ProJ(a,q,p)*q- ProJ(a,b,ProJ(a,q,p)*q)*b _|_ a & p-ProJ(a,q,p)*q _|_ a
  by A1,A2,Th14;
  then (p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q-(ProJ(a,b,ProJ(a,q,p)*q)*b)) _|_ a
  by Def1;
  then ((p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q))+(-(ProJ(a,b,ProJ(a,q,p)*q))*b)
  _|_ a by RLVECT_1:def 3;
  then (p+((-ProJ(a,q,p)*q)+(ProJ(a,q,p)*q))+(-(ProJ(a,b,ProJ(a,q,p)*q))*b))
  _|_ a by RLVECT_1:def 3;
  then p+0.S+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:5;
  then p+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:4;
  then
A3: p-(ProJ(a,q,p)*ProJ(a,b,q))*b _|_ a by A1,Th15;
  p-ProJ(a,b,p)*b _|_ a by A1,Th14;
  then ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A3,Th12;
  then
A4: ProJ(a,q,p)*(ProJ(a,b,q)*ProJ(a,b,q)") = ProJ(a,b,p)*ProJ (a,b,q)" by
GROUP_1:def 3;
  ProJ(a,b,q) <> 0.F by A1,A2,Th23;
  then ProJ(a,q,p)*1_F = ProJ(a,b,p)*ProJ(a,b,q)" by A4,VECTSP_1:def 10;
  hence thesis by VECTSP_1:def 8;
end;

theorem Th25:
  not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"
proof
  set 1F = 1_F, 0F = 0.F;
  assume that
A1: not b _|_ a and
A2: not c _|_ a;
A3: ProJ(a,c,b) <> 0F by A1,A2,Th23;
  ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by A1,A2,Th24;
  then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th22;
  then
A4: ProJ(a,b,c)" = ProJ(a,c,b) by VECTSP_1:def 8;
  ProJ(a,b,c) <> 0F by A1,A2,Th23;
  then 1F = ProJ(a,c,b)*ProJ(a,b,c) by A4,VECTSP_1:def 10;
  then ProJ(a,c,b)" = ProJ(a,c,b)"*(ProJ(a,c,b)*ProJ(a,b,c)) by VECTSP_1:def 8
    .= (ProJ(a,c,b)"*ProJ(a,c,b))*ProJ(a,b,c) by GROUP_1:def 3
    .= ProJ(a,b,c)*1F by A3,VECTSP_1:def 10;
  hence thesis by VECTSP_1:def 8;
end;

theorem Th26:
  not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = ProJ(c,b,a)
proof
  assume that
A1: not b _|_ a and
A2: b _|_ c+a;
  ProJ(a,b,c)*b _|_ c+a by A2,Def1;
  then
A3: -ProJ(a,b,c)*b _|_ c+a by Th6;
  c-ProJ(a,b,c)*b _|_ a by A1,Th14;
  then a _|_ -ProJ(a,b,c)*b+c by Th2;
  then c _|_ a+(-ProJ(a,b,c)*b) by A3,Def1;
  then
A4: a-ProJ(a,b,c)*b _|_ c by Th2;
  ( not a _|_ b)& c+a _|_ b by A1,A2,Th2;
  then not c _|_ b by Th3;
  then
A5: not b _|_ c by Th2;
  then a-ProJ(c,b,a)*b _|_ c by Th14;
  hence thesis by A5,A4,Th12;
end;

theorem Th27:
  not a _|_ b & not c _|_ b implies ProJ(c,b,a) = (-ProJ(b,a,c)")* ProJ(a,b,c)
proof
  set 1F = 1_F;
  assume that
A1: not a _|_ b and
A2: not c _|_ b;
A3: ProJ(b,a,c) <> 0.F by A1,A2,Th23;
  then
A4: -ProJ(b,a,c)" <> 0.F by VECTSP_1:25;
  (-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by A3,VECTSP_1:def 10;
  then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F)*(1F) by GROUP_1:def 3;
  then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F) by VECTSP_1:def 8;
  then (-(ProJ(b,a,c)"*(1F)))*ProJ(b,a,c) = -1F by VECTSP_1:9;
  then (-ProJ(b,a,c)")*ProJ(b,a,c) = -1F by VECTSP_1:def 8;
  then ProJ(b,a,(-ProJ(b,a,c)")*c) = -1F by A1,Th15;
  then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th14;
  then (-ProJ(b,a,c)")*c-(-a) _|_ b by VECTSP_1:14;
  then (-ProJ(b,a,c)")*c+a _|_ b by RLVECT_1:17;
  then
A5: b _|_ (-ProJ(b,a,c)")*c+a by Th2;
  not b _|_ a by A1,Th2;
  then ProJ(a,b,(-ProJ(b,a,c)")*c) = ProJ((-ProJ (b,a,c)")*c,b,a) by A5,Th26;
  then ProJ(a,b,(-ProJ(b,a,c)")*c) = ProJ(c,b,a) by A2,A4,Th2,Th18;
  hence thesis by A1,Th2,Th15;
end;

theorem Th28:
  1_F+1_F<>0.F & not a _|_ p & not a _|_ q & not b _|_ q implies
  ProJ(a,p,q)*ProJ(b,q,p) = ProJ(p,a,b)*ProJ(q,b,a)
proof
  assume that
A1: 1_F+1_F<>0.F and
A2: not a _|_ p and
A3: not a _|_ q and
A4: not b _|_ q;
A5: now
    assume that
A6: p _|_ q and
A7: a _|_ b;
    not q _|_ b by A4,Th2;
    then
A8: ProJ(b,q,p) = ProJ (b,q,p+a) by A7,Th19;
A9: not p+a _|_ q by A3,A6,Th4;
    then
A10: ProJ(b,q,p+a) = (-ProJ(q,p+a,b)")*ProJ(p+a,q,b) by A4,Th27;
A11: a _|_ a by A1,Th13;
A12: not p _|_ a by A2,Th2;
    then
A13: ProJ(a,p,q) = ProJ(a,p+a,q) by A11,Th19;
    not p+a _|_ a by A12,A11,Th4;
    then
A14: not a _|_ p+a by Th2;
A15: not q _|_ p+a by A9,Th2;
    then ProJ(a,p+a,q) = (-ProJ(p+a,q,a)")*ProJ(q,p+a,a) by A14,Th27;
    then
    ProJ(a,p,q)*ProJ(b,q,p) = ((ProJ(q,p+a,a)*(-ProJ(p+a,q,a)"))*(-ProJ(q
    ,p+a,b)"))*ProJ (p+a,q,b) by A13,A8,A10,GROUP_1:def 3
      .= (ProJ(q,p+a,a)*((-ProJ(p+a,q,a)")*(-ProJ(q,p+a,b)")))*ProJ (p+a,q,b
    ) by GROUP_1:def 3
      .= (ProJ(q,p+a,a)*(ProJ(q,p+a,b)"*ProJ(p+a,q,a)"))*ProJ(p+a,q,b) by
VECTSP_1:10
      .= ((ProJ(q,p+a,a)*ProJ(q,p+a,b)")*ProJ(p+a,q,a)")*ProJ (p+a,q,b) by
GROUP_1:def 3
      .= (ProJ(q,b,a)*ProJ(p+a,q,a)")*ProJ(p+a,q,b) by A4,A9,Th24
      .= ProJ(q,b,a)*(ProJ(p+a,q,b)*ProJ(p+a,q,a)") by GROUP_1:def 3
      .= ProJ(q,b,a)*ProJ(p+a,a,b) by A14,A15,Th24
      .= ProJ(q,b,a)*ProJ(p,a,b) by A2,A7,A11,Th20;
    hence thesis;
  end;
A16: now
    assume
A17: not a _|_ b;
A18: not q _|_ b by A4,Th2;
    then
A19: ProJ(q,b,a) = (-ProJ(b,a,q)")*ProJ(a,b,q) by A17,Th27;
A20: not p _|_ a by A2,Th2;
A21: not b _|_ a by A17,Th2;
    then ProJ(p,a,b) = (-ProJ(a,b,p)")*ProJ(b,a,p) by A20,Th27;
    then
    ProJ(p,a,b)*ProJ(q,b,a) = ((ProJ(b,a,p)*(-ProJ(a,b,p)"))*(-ProJ(b,a,q
    )"))*ProJ (a,b,q) by A19,GROUP_1:def 3
      .= (ProJ(b,a,p)*((-ProJ(a,b,p)")*(-ProJ(b,a,q)")))*ProJ (a,b,q) by
GROUP_1:def 3
      .= (ProJ(b,a,p)*(ProJ(b,a,q)"*ProJ(a,b,p)"))*ProJ(a,b,q) by VECTSP_1:10
      .= ((ProJ(b,a,p)*ProJ(b,a,q)")*ProJ(a,b,p)")*ProJ(a,b,q) by GROUP_1:def 3
      .= (ProJ(b,q,p)*ProJ(a,b,p)")*ProJ(a,b,q) by A17,A18,Th24
      .= ProJ(b,q,p)*(ProJ(a,b,q)*ProJ(a,b,p)") by GROUP_1:def 3
      .= ProJ(b,q,p)*ProJ(a,p,q) by A21,A20,Th24;
    hence thesis;
  end;
  now
    assume
A22: not p _|_ q;
    then
A23: ProJ(b,q,p) = (-(ProJ(q,p,b)"))*ProJ(p,q,b) by A4,Th27;
A24: not q _|_ p by A22,Th2;
    then ProJ(a,p,q) = (-ProJ(p,q,a)")*ProJ(q,p,a) by A2,Th27;
    then
    ProJ(a,p,q)*ProJ(b,q,p) = ((ProJ(q,p,a)*(-ProJ(p,q,a)"))*(-ProJ(q,p,b
    )"))*ProJ(p,q,b) by A23,GROUP_1:def 3
      .= (ProJ(q,p,a)*((-ProJ(p,q,a)")*(-ProJ(q,p,b)")))*ProJ (p,q,b) by
GROUP_1:def 3
      .= (ProJ(q,p,a)*(ProJ(q,p,b)"*ProJ(p,q,a)"))*ProJ(p,q,b) by VECTSP_1:10
      .= ((ProJ(q,p,a)*ProJ(q,p,b)")*ProJ(p,q,a)")*ProJ(p,q,b) by GROUP_1:def 3
      .= (ProJ(q,b,a)*ProJ(p,q,a)")*ProJ(p,q,b) by A4,A22,Th24
      .= ProJ(q,b,a)*(ProJ(p,q,b)*ProJ(p,q,a)") by GROUP_1:def 3
      .= ProJ(q,b,a)*ProJ(p,a,b) by A2,A24,Th24;
    hence thesis;
  end;
  hence thesis by A16,A5;
end;

theorem Th29:
  1_F+1_F<>0.F & not p _|_ a & not p _|_ x & not q _|_ a & not q
  _|_ x implies ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x)
proof
  set 0F = 0.F, 1F = 1_F;
  assume that
A1: 1_F+1_F<>0.F and
A2: not p _|_ a and
A3: not p _|_ x and
A4: not q _|_ a and
A5: not q _|_ x;
A6: ( not a _|_ q)& not x _|_ q by A4,A5,Th2;
  ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,p,q)*ProJ(x,q,p) by A1,A2,A3,A5,Th28;
  then ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,q,p)"*ProJ(x,q,p) by A2,A4,Th25;
  then
A7: ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = (ProJ(a,q,p)*ProJ(a,q,p)")*ProJ
  (x,q,p) by GROUP_1:def 3;
  ProJ(a,q,p) <> 0F by A2,A4,Th23;
  then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ (x,q,p)*(1F) by A7,
VECTSP_1:def 10;
  then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ(x,q,p) by VECTSP_1:def 8;
  then (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,x,a) = ProJ(x,q,p) by GROUP_1:def 3;
  then (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,a,x)" = ProJ(x,q,p) by A6,Th25;
  then
A8: (ProJ(a,q,p)*ProJ(p,a,x))*(ProJ(q,a,x)"*ProJ(q,a,x)) = ProJ(x,q,p)*ProJ
  (q,a,x) by GROUP_1:def 3;
  ProJ(q,a,x) <> 0F by A6,Th23;
  then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(x,q,p)*ProJ (q,a,x) by A8,
VECTSP_1:def 10;
  hence thesis by VECTSP_1:def 8;
end;

theorem Th30:
  1_F+1_F<>0.F & not p _|_ a & not p _|_ x & not q _|_ a & not q
_|_ x & not b _|_ a implies ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(a,b,q)*
  ProJ(q,a,x)*ProJ(x,q,y)
proof
  set 0F = 0.F, 1F = 1_F;
  assume that
A1: 1_F+1_F<>0.F & not p _|_ a and
A2: not p _|_ x and
A3: not q _|_ a and
A4: not q _|_ x and
A5: not b _|_ a;
A6: now
A7: ProJ(a,b,q) <> 0F by A3,A5,Th23;
    assume
A8: not y _|_ x;
    ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x) by A1,A2,A3,A4,Th29;
    then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ (q,a,x) by
A3,A5,Th24;
    then (ProJ(a,b,q)"*ProJ(a,b,p))*ProJ(p,a,x) = (ProJ(x,y,p)*ProJ(x,y,q)")*
    ProJ (q,a,x) by A4,A8,Th24;
    then
    ProJ(a,b,q)*(ProJ(a,b,q)"*(ProJ(a,b,p)*ProJ(p,a,x))) = ProJ(a,b,q)*((
    ProJ(x,y,p)*ProJ(x,y,q)")*ProJ (q,a,x)) by GROUP_1:def 3;
    then
    (ProJ(a,b,q)*ProJ(a,b,q)")*(ProJ(a,b,p)*ProJ(p,a,x)) = ProJ(a,b,q)*((
    ProJ(x,y,p)*ProJ(x,y,q)")*ProJ (q,a,x)) by GROUP_1:def 3;
    then
    (ProJ(a,b,p)*ProJ(p,a,x))*(1F) = ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q
    )")*ProJ (q,a,x)) by A7,VECTSP_1:def 10;
    then ProJ(a,b,p)*ProJ(p,a,x) = ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q)")*
    ProJ (q,a,x)) by VECTSP_1:def 8;
    then ProJ(a,b,p)*ProJ(p,a,x) = ProJ(a,b,q)*((ProJ(x,y,q)"*ProJ(x,p,y)")*
    ProJ (q,a,x)) by A2,A8,Th25;
    then ProJ(a,b,p)*ProJ(p,a,x) = (ProJ(a,b,q)*(ProJ(x,y,q)"*ProJ(x,p,y)"))*
    ProJ (q,a,x) by GROUP_1:def 3;
    then ProJ(a,b,p)*ProJ(p,a,x) = ProJ(q,a,x)*((ProJ(a,b,q)*ProJ(x,y,q)")*
    ProJ (x,p,y)") by GROUP_1:def 3;
    then
    ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ((ProJ(q,a,x)*(ProJ(a,b,q)*ProJ
    (x,y,q)"))*ProJ(x,p,y)")*ProJ (x,p,y) by GROUP_1:def 3;
    then
A9: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = (ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(
    x,y,q)"))*(ProJ(x,p,y)"*ProJ (x,p,y)) by GROUP_1:def 3;
    ProJ(x,p,y) <> 0F by A2,A8,Th23;
    then
    ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = (ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(
    x,y,q)"))*(1F) by A9,VECTSP_1:def 10;
    then
    ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x
    ,y,q)") by VECTSP_1:def 8;
    then
    ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x
    ,q,y)) by A4,A8,Th25;
    hence thesis by GROUP_1:def 3;
  end;
  now
    assume
A10: y _|_ x;
    then ProJ(x,p,y) = 0F by A2,Th23;
    then
A11: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by VECTSP_1:7;
    ProJ(x,q,y) = 0F by A4,A10,Th23;
    hence thesis by A11,VECTSP_1:7;
  end;
  hence thesis by A6;
end;

theorem Th31:
  not a _|_ p & not x _|_ p & not y _|_ p implies ProJ(p,a,x)*ProJ
  (x,p,y) = (-ProJ(p,a,y))*ProJ(y,p,x)
proof
  set 0F = 0.F, 1F = 1_F;
  assume that
A1: not a _|_ p and
A2: not x _|_ p and
A3: not y _|_ p;
A4: not p _|_ y by A3,Th2;
A5: not p _|_ x by A2,Th2;
A6: now
A7: ProJ(p,a,x) <> 0F by A1,A2,Th23;
    assume
A8: not y _|_ x;
    then
A9: not x _|_ y by Th2;
    ProJ(p,a,y)*ProJ(p,a,x)" = ProJ(p,x,y) by A1,A2,Th24;
    then
    (ProJ(p,a,y)*ProJ(p,a,x)")*ProJ(p,a,x) = ((-ProJ(x,y,p)")*ProJ(y,x,p)
    )*ProJ(p,a,x) by A5,A8,Th27;
    then
    ProJ(p,a,y)*(ProJ(p,a,x)"*ProJ(p,a,x)) = ((-ProJ(x,y,p)")*ProJ(y,x,p)
    )*ProJ(p,a,x) by GROUP_1:def 3;
    then ProJ(p,a,y)*(1F) = ((-ProJ(x,y,p)")*ProJ(y,x,p))*ProJ(p,a,x) by A7,
VECTSP_1:def 10;
    then ProJ(p,a,y) = (ProJ(y,x,p)*(-ProJ(x,y,p)"))*ProJ (p,a,x) by
VECTSP_1:def 8;
    then ProJ(p,a,y) = ProJ(y,x,p)*((-ProJ(x,y,p)")*ProJ (p,a,x)) by
GROUP_1:def 3;
    then
    ProJ(y,p,x)*ProJ(p,a,y) = ProJ(y,p,x)*(ProJ(y,p,x)"*((-ProJ(x,y,p)")*
    ProJ(p,a,x))) by A4,A9,Th25;
    then
A10: ProJ(y,p,x)*ProJ(p,a,y) = (ProJ(y,p,x)*ProJ(y,p,x)")*((-ProJ(x,y,p )"
    )*ProJ (p,a,x)) by GROUP_1:def 3;
    ProJ(y,p,x) <> 0F by A4,A9,Th23;
    then ProJ(y,p,x)*ProJ(p,a,y) = ((-ProJ(x,y,p)")*ProJ(p,a,x))*(1F) by A10,
VECTSP_1:def 10;
    then ProJ(p,a,y)*ProJ(y,p,x) = (-ProJ(x,y,p)")*ProJ(p,a,x) by
VECTSP_1:def 8;
    then -(ProJ(p,a,y)*ProJ(y,p,x)) = -(-ProJ(x,y,p)"*ProJ (p,a,x)) by
VECTSP_1:9;
    then -(ProJ(p,a,y)*ProJ(y,p,x)) = ProJ(x,y,p)"*ProJ(p,a,x) by RLVECT_1:17;
    then (-ProJ(p,a,y))*ProJ(y,p,x) = ProJ(x,y,p)"*ProJ(p,a,x) by VECTSP_1:9;
    hence thesis by A5,A8,Th25;
  end;
  now
    assume
A11: y _|_ x;
    then ProJ(x,p,y) = 0F by A5,Th23;
    then
A12: ProJ(p,a,x)*ProJ(x,p,y) = 0F by VECTSP_1:7;
    x _|_ y by A11,Th2;
    then ProJ(y,p,x) = 0F by A4,Th23;
    hence thesis by A12,VECTSP_1:7;
  end;
  hence thesis by A6;
end;

::                   6. BILINEAR ANTISYMMETRIC FORM

definition
  let F,S,x,y,a,b;
  assume
A1: ( not b _|_ a)& 1_F+1_F<>0.F;
  func PProJ(a,b,x,y) -> Element of F means
  :Def3:
  for q st not q _|_ a & not q _|_ x holds
  it = ProJ(a,b,q)* ProJ(q,a,x)*ProJ(x,q,y)
  if ex p st not p _|_ a & not p _|_ x
  otherwise it = 0.F;
  existence
  proof
    thus (ex p st not p _|_ a & not p _|_ x) implies ex IT being Element of F
st for q st not q _|_ a & not q _|_ x holds IT = ProJ(a,b,q)*ProJ(q,a,x)*ProJ (
    x,q,y)
    proof
      given p such that
A2:   ( not p _|_ a)& not p _|_ x;
      take ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y);
      let q;
      assume ( not q _|_ a)& not q _|_ x;
      hence thesis by A1,A2,Th30;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be Element of F;
    thus (ex p st not p _|_ a & not p _|_ x) & (for q st not q _|_ a & not q
_|_ x holds IT1 = ProJ(a,b,q)* ProJ(q,a,x)*ProJ(x,q,y)) & (for q st not q _|_ a
& not q _|_ x holds IT2 = ProJ(a,b,q)*ProJ(q,a,x)*ProJ (x,q,y)) implies IT1 =
    IT2
    proof
      given p such that
A3:   ( not p _|_ a)& not p _|_ x;
      consider r such that
A4:   ( not r _|_ a)& not r _|_ x by A3;
      assume that
A5:   for q st not q _|_ a & not q _|_ x holds IT1 = ProJ(a,b,q)*ProJ(
      q,a,x)*ProJ(x,q,y) and
A6:   for q st not q _|_ a & not q _|_ x holds IT2 = ProJ(a,b,q)*ProJ
      (q,a,x)*ProJ(x,q,y);
      IT1 = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A5,A4;
      hence thesis by A6,A4;
    end;
    thus thesis;
  end;
  consistency;
end;

theorem Th32:
  1_F+1_F<>0.F & not b _|_ a & x=0.S implies PProJ(a,b,x,y) = 0.F
proof
  assume that
A1: 1_F+1_F<>0.F & not b _|_ a and
A2: x=0.S;
  for p holds p _|_ a or p _|_ x by A2,Th1,Th2;
  hence thesis by A1,Def3;
end;

theorem Th33:
  1_F+1_F<>0.F & not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x)
proof
  set 0F = 0.F;
  assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: a<>0.S by A2,Th1,Th2;
A4: PProJ(a,b,x,y) = 0.F implies y _|_ x
  proof
    assume
A5: PProJ(a,b,x,y) = 0.F;
A6: now
      given p such that
A7:   not p _|_ a and
A8:   not p _|_ x;
A9:   now
        assume
A10:    ProJ(p,a,x) = 0.F;
        not a _|_ p by A7,Th2;
        then x _|_ p by A10,Th23;
        hence contradiction by A8,Th2;
      end;
      ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A2,A5,A7,A8,Def3;
      then ProJ(a,b,p)*ProJ(p,a,x) = 0F or ProJ(x,p,y) = 0F by VECTSP_1:12;
      then ProJ(a,b,p) = 0.F or ProJ(p,a,x) = 0.F or ProJ(x,p,y) = 0.F by
VECTSP_1:12;
      hence thesis by A2,A7,A8,A9,Th23;
    end;
    now
      assume for p holds p _|_ a or p _|_ x;
      then x = 0.S by A3,Th9;
      hence thesis by Th1,Th2;
    end;
    hence thesis by A6;
  end;
  y _|_ x implies PProJ(a,b,x,y) = 0.F
  proof
    assume
A11: y _|_ x;
A12: now
      assume x<>0.S;
      then consider p such that
A13:  not p _|_ a and
A14:  not p _|_ x by A3,Th9;
      ProJ(x,p,y) = 0F by A11,A14,Th23;
      then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F by VECTSP_1:7;
      hence thesis by A1,A2,A13,A14,Def3;
    end;
    now
      assume x = 0.S;
      then for p holds p _|_ a or p _|_ x by Th1,Th2;
      hence thesis by A1,A2,Def3;
    end;
    hence thesis by A12;
  end;
  hence thesis by A4;
end;

theorem
  1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,y) = -PProJ(a,b,y,x)
proof
  set 0F = 0.F, 1F = 1_F;
  assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
    assume not x _|_ y;
    then
A4: x <> 0.S & y <> 0.S by Th1,Th2;
    a <> 0.S by A2,Th1,Th2;
    then consider r such that
A5: not r _|_ a and
A6: not r _|_ x and
A7: not r _|_ y by A1,A4,Th10;
A8: not y _|_ r by A7,Th2;
    PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A2,A5,A7,Def3;
    then
A9: PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,y)*ProJ (y,r,x)) by GROUP_1:def 3;
    ( not a _|_ r)& not x _|_ r by A5,A6,Th2;
    then PProJ(a,b,y,x) = ProJ(a,b,r)*((-(ProJ(r,a,x)))*ProJ (x,r,y)) by A8,A9
,Th31;
    then PProJ(a,b,y,x) = ((-(ProJ(r,a,x)))*ProJ(a,b,r))*ProJ (x,r,y) by
GROUP_1:def 3;
    then PProJ(a,b,y,x) = (-ProJ(r,a,x)*ProJ(a,b,r))*ProJ (x,r,y) by VECTSP_1:9
;
    then (-1F)*PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y))
    by VECTSP_1:9;
    then
    -(PProJ(a,b,y,x)*(1F)) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y)
    ) by VECTSP_1:9;
    then -PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y)) by
VECTSP_1:def 8;
    then
A10: -PProJ(a,b,y,x) = (ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y))*(1F) by
VECTSP_1:10;
    PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A2,A5,A6,Def3;
    hence thesis by A10,VECTSP_1:def 8;
  end;
  now
    assume
A11: x _|_ y;
    then (-1F)*PProJ(a,b,y,x) = (-1F)*0F by A1,A2,Th33;
    then -(PProJ (a,b,y,x)*(1F)) = (-1F)*0F by VECTSP_1:9;
    then
A12: -PProJ(a,b,y,x) = (-1F)*0F by VECTSP_1:def 8;
    y _|_ x by A11,Th2;
    then PProJ(a,b,x,y) = 0F by A1,A2,Th33;
    hence thesis by A12,VECTSP_1:7;
  end;
  hence thesis by A3;
end;

theorem
  1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y)
proof
  set 0F = 0.F;
  assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
    assume not x _|_ y;
    then
A4: x <> 0.S by Th1;
    a <> 0.S by A2,Th1,Th2;
    then consider p such that
A5: not p _|_ a and
A6: not p _|_ x by A4,Th9;
    PProJ(a,b,x,l*y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ (x,p,l*y) by A1,A2,A5,A6
,Def3;
    then
A7: PProJ(a,b,x,l*y) = (l*ProJ(x,p,y))*(ProJ(a,b,p)*ProJ(p,a,x)) by A6,Th15;
    PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A2,A5,A6,Def3;
    hence thesis by A7,GROUP_1:def 3;
  end;
  now
    assume
A8: x _|_ y;
    then y _|_ x by Th2;
    then l*y _|_ x by Def1;
    then
A9: PProJ(a,b,x,l*y) = 0F by A1,A2,Th33;
    y _|_ x by A8,Th2;
    then l*PProJ(a,b,x,y) = l*0F by A1,A2,Th33;
    hence thesis by A9,VECTSP_1:7;
  end;
  hence thesis by A3;
end;

theorem
  1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) +
  PProJ (a,b,x,z)
proof
  assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
    assume
A4: x <> 0.S;
    a <> 0.S by A2,Th1,Th2;
    then consider p such that
A5: ( not p _|_ a)& not p _|_ x by A4,Th9;
A6: PProJ(a,b,x,y+z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ (x,p,y+z) & PProJ(a,b
    ,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A2,A5,Def3;
    PProJ(a,b,x,z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,z) & ProJ(x,p,y+z)
    = ProJ( x,p,y) + ProJ(x,p,z) by A1,A2,A5,Def3,Th16;
    hence thesis by A6,VECTSP_1:def 7;
  end;
  set 0F = 0.F;
  now
    assume
A7: x = 0.S;
    then
A8: PProJ (a,b,x,z) = 0F by A1,A2,Th32;
    PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F by A1,A2,A7,Th32;
    hence thesis by A8,RLVECT_1:4;
  end;
  hence thesis by A3;
end;