:: Construction of a bilinear symmetric form in orthogonal vector space
::  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, CARD_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_1, ZFMISC_1,
      TARSKI, RELAT_1, STRUCT_0, SYMSP_1, RLVECT_1, ALGSTR_0, ARYTM_3,
      SUPINF_2, ARYTM_1, GROUP_1, FUNCOP_1, ORTSP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      ORDINAL1, NUMBERS, DOMAIN_1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1,
      GROUP_1, VECTSP_1, RELSET_1, SYMSP_1;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, SYMSP_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, SYMSP_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, ALGSTR_0;
 equalities BINOP_1, ALGSTR_0;
 expansions TARSKI;
 theorems VECTSP_1, TARSKI, RLVECT_1, GROUP_1, FUNCOP_1, STRUCT_0, ORDERS_2,
      XTUPLE_0;
 schemes BINOP_1, XBOOLE_0;

begin

::                 1. ORTHOGONAL VECTOR SPACE STRUCTURE

reserve F for Field;

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

Lm2: now
  defpred P[object] 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 object holds x in mo iff x in CV & P[x] from XBOOLE_0:sch 1;
  mo c= CV
  by A1;
  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;

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 #);
A1: for x being Element of H holds x+0.H = x
  proof
    let x be Element of H;
    md.(x,0.H) = o by Lm1;
    hence thesis by TARSKI:def 1;
  end;
A2: H is right_complementable
  proof
    let x be Element of H;
    take -x;
    0.H = o by STRUCT_0:def 6;
    hence thesis by Lm1;
  end;
A3: for x,y,z being Element of H holds (x+y)+z = x+(y+z)
  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;
  for x,y being Element of H holds x+y = y+x
  proof
    let x,y be Element of H;
    md.(x,y) = o by Lm1;
    hence thesis by Lm1;
  end;
  hence thesis by A3,A1,A2,RLVECT_1:def 2,def 3,def 4;
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 qua
  set] = 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 qua set) = 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 MPS;
A8:   o = 0.MPS by A2,STRUCT_0:def 6;
      reconsider v,w as Element of X by A2;
A9:   md.(v,w) = o by Lm1;
      reconsider v,w as Element of MPS;
      x*(v+w) = mF.(x,o) by A2,A9,VECTSP_1:def 12;
      then
A10:  x*(v+w) = o by A1;
      reconsider w as Element of MPS;
      reconsider v as Element of MPS;
A11:  mF.(x,v qua set) = o by A1;
      reconsider v as Element of MPS;
A12:  mF.(x,w qua set) = o by A1;
      reconsider w as Element of MPS;
A13:  x*w = o by A2,A12,VECTSP_1:def 12;
      x*v = o by A2,A11,VECTSP_1:def 12;
      hence thesis by A10,A13,A8,RLVECT_1:4;
    end;
A14: (x+y)*v = x*v+y*v
    proof
      set z = x+y;
A15:  z*v = mF.(z,v) by A2,VECTSP_1:def 12;
      reconsider v as Element of MPS;
      reconsider v as Element of MPS;
A16:  (x+y)*v = o by A1,A2,A15;
      reconsider v as Element of MPS;
A17:  mF.(x,v qua set) = o by A1,A2;
      reconsider v as Element of MPS;
A18:  x*v = o by A2,A17,VECTSP_1:def 12;
      reconsider v as Element of MPS;
A19:  mF.(y,v qua set) = o by A1,A2;
A20:  o = 0.MPS by A2,STRUCT_0:def 6;
      reconsider v as Element of MPS;
      y*v = o by A2,A19,VECTSP_1:def 12;
      hence thesis by A16,A18,A20,RLVECT_1:4;
    end;
    (1_F)*v = v
    proof
      set one1 = 1_F;
A21:  one1*v = mF.(one1,v) by A2,VECTSP_1:def 12;
      reconsider v as Element of MPS;
      mF.(one1,v qua set) = o by A1,A2;
      hence thesis by A2,A21,TARSKI:def 1;
    end;
    hence thesis by A7,A14,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 #);
  0.MPS = o by A2,TARSKI:def 1;
  hence for a,b,c,d being Element of MPS holds (a <> 0.MPS & b <> 0.MPS & c <>
0.MPS & d <> 0.MPS implies ex p being Element of MPS st not p _|_ a & not p _|_
  b & not p _|_ c & not p _|_ d ) 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;
  thus for a,b,c being Element of MPS holds (a _|_ b-c & b _|_ c-a implies c
  _|_ a-b)
  proof
    let a,b,c be Element of MPS;
    assume that
    a _|_ b-c and
    b _|_ c-a;
    assume not thesis;
    then a-b <> o by A4;
    hence contradiction by A2,TARSKI:def 1;
  end;
end;

::                    2. ORTHOGONAL VECTOR SPACE

definition
  let F;
  let IT be Abelian add-associative right_zeroed right_complementable non
  empty SymStr over F;

  attr IT is OrtSp-like means
  :Def1:
  for a,b,c,d,x being Element of IT for l
  being Element of F holds (a<>0.IT & b<>0.IT & c <>0.IT & d<>0.IT implies ex p
being Element of IT st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d )
& (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 OrtSp-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
    reconsider mF = [:the carrier of F,X:] --> o as Function of [:the carrier
    of F,X:],X;
    consider mo being Relation of X such that
A1: 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,d,x being Element of MPS for l being Element of F holds (a
<>0.MPS & b<>0.MPS & c <>0.MPS & d<>0.MPS implies ex p being Element of MPS st
not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d ) & (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 A1,Lm5;
    for a being Element of F for x being Element of X holds mF.[a,x] = o
    by FUNCOP_1:7;
    hence MPS is vector-distributive scalar-distributive scalar-associative
    scalar-unital by Lm4;
    thus thesis;
  end;
end;

definition
  let F;
  mode OrtSp of F is OrtSp-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 OrtSp of F;
reserve a,b,c,d,p,q,r,x,y,z for Element of S;
reserve k,l for Element of F;

theorem Th1:
  0.S _|_ a
proof
  set 0F = 0.F,0V = 0.S;
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 a _|_ (-(-b)) by RLVECT_1:17;
  then
A1: a _|_ 0V-(-b) by RLVECT_1:4;
  0V _|_ -b-a by Th1;
  then -b _|_ a-0V by A1,Def1;
  then -b _|_ a by VECTSP_1:18;
  then (-1_F)*(-b) _|_ a by Def1;
  then -(-b) _|_ a by VECTSP_1:14;
  hence thesis by RLVECT_1:17;
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:
  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 Th8:
  not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
proof
  set 1F = 1_F;
  assume that
A1: not b _|_ a and
A2: x-k*b _|_ a & x-l*b _|_ a;
  k*b-l*b _|_ a by A2,Th7;
  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;
  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 Th9:
  a _|_ a & b _|_ b implies a+b _|_ a-b
proof
  set 0V = 0.S;
  assume that
A1: a _|_ a and
A2: b _|_ b;
  (-1_F)*a _|_ a by A1,Def1;
  then -a _|_ a by VECTSP_1:14;
  then a _|_ -a by Th2;
  then a _|_ 0V+(-a) by RLVECT_1:4;
  then a _|_ (b+(-b))+(-a) by RLVECT_1:5;
  then a _|_ b+(-b-a) by RLVECT_1:def 3;
  then
A3: a _|_ b-(a+b) by VECTSP_1:17;
  b _|_ b+0V by A2,RLVECT_1:4;
  then b _|_ b+(a+(-a)) by RLVECT_1:5;
  then b _|_ (a+b)-a by RLVECT_1:def 3;
  hence thesis by A3,Def1;
end;

theorem
  1_F+1_F <> 0.F & (ex a st a<>0.S) implies ex b st not b _|_ b
proof
  set 1F = 1_F,0V = 0.S;
  assume that
A1: 1_F+1_F<>0.F and
A2: ex a st a<>0.S;
  consider a such that
A3: a<>0.S by A2;
  assume
A4: not thesis;
A5: for c,d holds c _|_ d
  proof
    let c,d;
    d _|_ d & c _|_ c by A4;
    then d+c _|_ d-c by Th9;
    then
A6: d-c _|_ d+c by Th2;
    d+c _|_ d+c by A4;
    then (d+c)+((-c)+d) _|_ d+c by A6,Def1;
    then ((d+c)+(-c))+d _|_ d+c by RLVECT_1:def 3;
    then (d+(c+(-c)))+d _|_ d+c by RLVECT_1:def 3;
    then (d+0V)+d _|_ d+c by RLVECT_1:5;
    then d+d _|_ d+c by RLVECT_1:4;
    then (1F)*d+d _|_ d+c by VECTSP_1:def 17;
    then (1F)*d+(1F)*d _|_ d+c by VECTSP_1:def 17;
    then (1F+1F)*d _|_ d+c by VECTSP_1:def 15;
    then (1F+1F)"*((1F+1F)*d) _|_ d+c by Def1;
    then ((1F+1F)"*(1F+1F))*d _|_ d+c by VECTSP_1:def 16;
    then (1F)*d _|_ d+c by A1,VECTSP_1:def 10;
    then d _|_ d+c by VECTSP_1:def 17;
    then
A7: d+c _|_ d by Th2;
    -d _|_ d by A4,Th6;
    then -d+(d+c) _|_ d by A7,Def1;
    then (-d+d)+c _|_ d by RLVECT_1:def 3;
    then 0V+c _|_ d by RLVECT_1:5;
    hence thesis by RLVECT_1:4;
  end;
  ex c st not c _|_ a & not c _|_ a & not c _|_ a & not c _|_ a by A3,Def1;
  hence contradiction by A5;
end;

::                     5. ORTHOGONAL PROJECTION

definition
  let F,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,Th8;
  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 Th11:
  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 Th12:
  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 Th11;
  L _|_ a by A2,Th11;
  then l*x-(l*ProJ(a,b,x))*b _|_ a by A1,Def1;
  hence thesis by A2,A3,Th8;
end;

theorem Th13:
  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 = (x+(-ProJ(a,b,x)*b))+(y-ProJ(a,b,y)*b)
    .= (x+(-ProJ(a,b,x)*b))+(y+(-ProJ(a,b,y)*b))
    .= (((-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)
    .= (x+y)+((-ProJ(a,b,x))*b+(-ProJ(a,b,y))*b)
    .= (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 Th11;
  then
A3: L _|_ a by Def1;
  (x+y)-ProJ(a,b,x+y)*b _|_ a by A2,Th11;
  hence thesis by A2,A1,A3,Th8;
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 Th11;
A4: L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 16;
  x-ProJ(a,b,x)*b _|_ a by A1,Th11;
  then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A3,A4,Th8;
  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;
end;

theorem Th15:
  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 Th11;
  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,Th11;
  hence thesis by A1,A3,Th8;
end;

theorem
  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 Th11;
  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,Th11;
  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,Th11;
  hence thesis by A1,A5,A4,Th8;
end;

theorem
  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,Th11;
  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 Th11;
  hence thesis by A7,A6,Th8;
end;

theorem Th18:
  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,Th11,VECTSP_1:def 17;
  hence thesis by A1,Th8;
end;

theorem Th19:
  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,Th18;
end;

theorem Th20:
  not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F )
proof
  set 0F = 0.F;
  set 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,Th11;
    hence ProJ(a,b,x) = 0.F by A2,A4,Th8;
  end;
  now
    assume ( not b _|_ a)& ProJ(a,b,x) = 0.F;
    then x-0F*b _|_ a by Th11;
    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 Th21:
  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,Th11;
  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,Th12;
  p-ProJ(a,b,p)*b _|_ a by A1,Th11;
  then ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A3,Th8;
  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,Th20;
  then ProJ(a,q,p)*1_F = ProJ(a,b,p)*ProJ(a,b,q)" by A4,VECTSP_1:def 10;
  hence thesis;
end;

theorem Th22:
  not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"
proof
  set 1F = 1_F;
  set 0F = 0.F;
  assume that
A1: not b _|_ a and
A2: not c _|_ a;
A3: ProJ(a,c,b) <> 0F by A1,A2,Th20;
  ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by A1,A2,Th21;
  then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th19;
  then
A4: ProJ(a,b,c)" = ProJ(a,c,b);
  ProJ(a,b,c) <> 0F by A1,A2,Th20;
  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))
    .= (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;
end;

theorem Th23:
  not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = -ProJ(c,b,a)
proof
  set 1F = 1_F;
  assume that
A1: not b _|_ a and
A2: b _|_ c+a;
  c-ProJ(a,b,c)*b _|_ a by A1,Th11;
  then (-ProJ(a,b,c))*b+c _|_ a by VECTSP_1:21;
  then (-1F)*((-ProJ(a,b,c))*b+c) _|_ a by Def1;
  then (-1F)*((-ProJ(a,b,c))*b)+(-1F)*c _|_ a by VECTSP_1:def 14;
  then ((-1F)*(-ProJ(a,b,c)))*b+(-1F)*c _|_ a by VECTSP_1:def 16;
  then (ProJ(a,b,c)*(1F))*b+(-1F)*c _|_ a by VECTSP_1:10;
  then ProJ(a,b,c)*b+(-1F)*c _|_ a;
  then ProJ(a,b,c)*b-c _|_ a by VECTSP_1:14;
  then a _|_ ProJ(a,b,c)*b-c by Th2;
  then
A3: -a _|_ ProJ(a,b,c)*b-c by Th6;
  ProJ(a,b,c)*b _|_ c+a by A2,Def1;
  then ProJ(a,b,c)*b _|_ c-(-a) by RLVECT_1:17;
  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
A5: not c _|_ b by Th3;
  then
A6: not b _|_ c by Th2;
  then -a-ProJ(c,b,-a)*b _|_ c by Th11;
  then ProJ(a,b,c) = ProJ(c,b,-a) by A6,A4,Th8
    .= ProJ(c,b,(-1F)*a) by VECTSP_1:14
    .= (-1F)*ProJ(c,b,a) by A5,Th2,Th12
    .= -(ProJ(c,b,a)*(1F)) by VECTSP_1:9;
  hence thesis;
end;

theorem Th24:
  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;
  ProJ(b,a,c) <> 0.F by A1,A2,Th20;
  then
A3: -ProJ(b,a,c)" <> 0.F by VECTSP_1:25;
  ProJ(b,a,c) <> 0.F by A1,A2,Th20;
  then (-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by 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);
  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;
  then ProJ(b,a,(-ProJ(b,a,c)")*c) = -1F by A1,Th12;
  then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th11;
  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
A4: 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 A4,Th23;
  then ProJ(a,b,(-ProJ(b,a,c)")*c) = -ProJ(c,b,a) by A2,A3,Th2,Th15;
  then (-ProJ(b,a,c)")*ProJ(a,b,c) = -ProJ(c,b,a) by A1,Th2,Th12;
  then (-(ProJ(b,a,c)"*ProJ(a,b,c)))*(-1F) = (-ProJ (c,b,a))*(-1F) by
VECTSP_1:9;
  then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = (-ProJ(c,b,a))*(-1F) by VECTSP_1:10;
  then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = ProJ(c,b,a)*(1F) by VECTSP_1:10;
  then ProJ(b,a,c)"*ProJ(a,b,c) = ProJ(c,b,a)*(1F);
  hence thesis;
end;

theorem Th25:
  not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x implies
  ProJ(a,q,p)*ProJ(p,a,x) = ProJ(q,a,x)*ProJ(x,q,p)
proof
  set 0F = 0.F;
  set 1F = 1_F;
  assume that
A1: not p _|_ a and
A2: not p _|_ x and
A3: not q _|_ a and
A4: not q _|_ x;
A5: p <> 0.S & q <> 0.S by A1,A3,Th1;
A6: not a _|_ p by A1,Th2;
  a <> 0.S & x <> 0.S by A1,A2,Th1,Th2;
  then consider r such that
A7: not r _|_ p and
A8: not r _|_ q and
A9: not r _|_ a and
A10: not r _|_ x by A5,Def1;
A11: not q _|_ r by A8,Th2;
A12: not x _|_ r by A10,Th2;
A13: not p _|_ r by A7,Th2;
  then
A14: ProJ(r,q,p) <> 0F by A11,Th20;
A15: not a _|_ r by A9,Th2;
A16: not x _|_ q by A4,Th2;
A17: not x _|_ p by A2,Th2;
A18: not a _|_ q by A3,Th2;
  ProJ(a,q,p)*ProJ(p,a,x)*ProJ(q,a,x)" = (ProJ(a,r,p)*ProJ(a,r,q)")*ProJ(
  p,a,x)*ProJ(q,a,x)" by A3,A9,Th21
    .= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ (q,a,x)"
  by A6,A7,Th21
    .= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ (q,x,a) by
A18,A16,Th22
    .= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*(ProJ(q,r,a)*
  ProJ (q,r,x)") by A16,A8,Th21
    .= (ProJ(a,p,r)"*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*(ProJ(q,r,a)*
  ProJ (q,r,x)") by A1,A9,Th22
    .= (ProJ(a,p,r)"*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,r,a)*
  ProJ (q,r,x)") by A6,A7,Th22
    .= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,r,a)*
  ProJ (q,r,x)") by A3,A9,Th22
    .= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,a,r)"*
  ProJ (q,r,x)") by A18,A8,Th22
    .= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,x,r)"*ProJ(p,a,r))*(ProJ(q,a,r)"*
  ProJ (q,r,x)") by A17,A7,Th22
    .= (ProJ(p,x,r)"*ProJ(p,a,r))*(ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(q,a,r)"*
  ProJ (q,x,r)) by A16,A8,Th22
    .= ProJ(p,x,r)"*((ProJ(a,p,r)"*ProJ(a,q,r))*ProJ(p,a,r))*(ProJ(q,a,r)"*
  ProJ (q,x,r)) by GROUP_1:def 3
    .= ProJ(p,x,r)"*((ProJ(a,p,r)"*ProJ(p,a,r))*ProJ(a,q,r))*(ProJ(q,a,r)"*
  ProJ (q,x,r)) by GROUP_1:def 3
    .= ProJ(p,x,r)"*(ProJ(r,a,p)*ProJ(a,q,r))*(ProJ(q,a,r)"*ProJ (q,x,r)) by A1
,A9,Th24
    .= (ProJ(p,x,r)"*ProJ(r,a,p))*ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ (q,x,r)) by
GROUP_1:def 3
    .= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ (q,x,r)))
  by GROUP_1:def 3
    .= (ProJ(p,x,r)"*ProJ(r,a,p))*((ProJ(q,a,r)"*ProJ(a,q,r))*ProJ(q,x,r))
  by GROUP_1:def 3
    .= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(r,q,a)*ProJ(q,x,r)) by A18,A8,Th24
    .= ProJ(p,x,r)"*(ProJ(r,a,p)*(ProJ(r,q,a)*ProJ(q,x,r))) by GROUP_1:def 3
    .= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,q,a))*ProJ(q,x,r)) by GROUP_1:def 3
    .= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,a,q)")*ProJ(q,x,r)) by A11,A15,Th22
    .= ProJ(p,x,r)"*(ProJ(r,q,p)*ProJ(q,x,r)) by A11,A15,Th21
    .= ProJ(p,r,x)*(ProJ(r,q,p)*ProJ(q,x,r)) by A17,A7,Th22
    .= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*ProJ(q,x,r)) by A13,A12,Th24
    .= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*(ProJ(x,r,q)"*ProJ (r,x,q)))
  by A4,A10,Th24
    .= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,x,q)*(ProJ(r,q,p)*ProJ(x,r,q)"))
  by GROUP_1:def 3
    .= ((ProJ(x,r,p)*ProJ(r,x,p)")*ProJ(r,x,q))*(ProJ(r,q,p)*ProJ(x,r,q)")
  by GROUP_1:def 3
    .= (ProJ(x,r,p)*(ProJ(r,x,q)*ProJ(r,x,p)"))*(ProJ(r,q,p)*ProJ(x,r,q)")
  by GROUP_1:def 3
    .= (ProJ(x,r,p)*ProJ(r,p,q))*(ProJ(r,q,p)*ProJ(x,r,q)") by A13,A12,Th21
    .= ProJ(x,r,p)*(ProJ(r,p,q)*(ProJ(r,q,p)*ProJ(x,r,q)")) by GROUP_1:def 3
    .= ProJ(x,r,p)*((ProJ(r,p,q)*ProJ(r,q,p))*ProJ(x,r,q)") by GROUP_1:def 3
    .= ProJ(x,r,p)*((ProJ(r,q,p)"*ProJ(r,q,p))*ProJ(x,r,q)") by A13,A11,Th22
    .= ProJ(x,r,p)*(ProJ(x,r,q)"*(1F)) by A14,VECTSP_1:def 10
    .= ProJ(x,r,p)*ProJ(x,r,q)"
    .= ProJ(x,q,p) by A4,A10,Th21;
  then
A19: (ProJ(q,a,x)*ProJ(q,a,x)")*(ProJ(a,q,p)*ProJ(p,a,x)) = ProJ(q,a,x)*
  ProJ (x,q,p) by GROUP_1:def 3;
  ProJ(q,a,x) <> 0F by A18,A16,Th20;
  then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(q,a,x)*ProJ (x,q,p) by A19,
VECTSP_1:def 10;
  hence thesis;
end;

theorem Th26:
  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;
  set 1F = 1_F;
  assume that
A1: 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,Th20;
    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,Th25;
    then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ (q,a,x) by
A3,A5,Th21;
    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,Th21;
    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));
    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,Th22;
    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,Th20;
    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)");
    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,Th22;
    hence thesis by GROUP_1:def 3;
  end;
  now
    assume
A10: y _|_ x;
    then ProJ(x,p,y) = 0F by A2,Th20;
    then
A11: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F;
    ProJ(x,q,y) = 0F by A4,A10,Th20;
    hence thesis by A11;
  end;
  hence thesis by A6;
end;

theorem Th27:
  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;
  set 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,Th20;
    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,Th21;
    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,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 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);
    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,Th22;
    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,Th20;
    then ProJ(y,p,x)*ProJ(p,a,y) = (ProJ(x,y,p)"*ProJ(p,a,x))*(1F) by A10,
VECTSP_1:def 10
      .= ProJ(x,y,p)"*ProJ(p,a,x);
    hence thesis by A5,A8,Th22;
  end;
  now
    assume
A11: y _|_ x;
    then ProJ(x,p,y) = 0F by A5,Th20;
    then
A12: ProJ(p,a,x)*ProJ(x,p,y) = 0F;
    x _|_ y by A11,Th2;
    then ProJ(y,p,x) = 0F by A4,Th20;
    hence thesis by A12;
  end;
  hence thesis by A6;
end;

::                   6. BILINEAR SYMMETRIC FORM

definition
  let F,S,x,y,a,b;
  assume
A1: not b _|_ a;
  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,Th26;
    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 Th28:
  not b _|_ a & x = 0.S implies PProJ(a,b,x,y) = 0.F
proof
  assume that
A1: 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 Th29:
  not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x)
proof
  set 0F = 0.F;
  assume
A1: not b _|_ a;
  then
A2: a <> 0.S by Th1,Th2;
A3: PProJ(a,b,x,y) = 0.F implies y _|_ x
  proof
    assume
A4: PProJ(a,b,x,y) = 0.F;
A5: now
      given p such that
A6:   not p _|_ a and
A7:   not p _|_ x;
A8:   now
        assume
A9:     ProJ(p,a,x) = 0.F;
        not a _|_ p by A6,Th2;
        then x _|_ p by A9,Th20;
        hence contradiction by A7,Th2;
      end;
      ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A4,A6,A7,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 A1,A6,A7,A8,Th20;
    end;
    now
      assume
A10:  for p holds p _|_ a or p _|_ x;
      x = 0.S
      proof
        assume not thesis;
        then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by
A2,Def1;
        hence contradiction by A10;
      end;
      hence thesis by Th1,Th2;
    end;
    hence thesis by A5;
  end;
  y _|_ x implies PProJ(a,b,x,y) = 0.F
  proof
    assume
A11: y _|_ x;
A12: now
      assume x <> 0.S;
      then
      ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A2,Def1;
      then consider p such that
A13:  not p _|_ a and
A14:  not p _|_ x;
      ProJ(x,p,y) = 0F by A11,A14,Th20;
      then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F;
      hence thesis by A1,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,Def3;
    end;
    hence thesis by A12;
  end;
  hence thesis by A3;
end;

theorem
  not b _|_ a implies PProJ(a,b,x,y) = PProJ(a,b,y,x)
proof
  assume
A1: not b _|_ a;
A2: now
    assume not x _|_ y;
    then
A3: x <> 0.S & y <> 0.S by Th1,Th2;
    a <> 0.S by A1,Th1,Th2;
    then
    ex r st not r _|_ a & not r _|_ x & not r _|_ y & not r _|_ a by A3,Def1;
    then consider r such that
A4: not r _|_ a and
A5: not r _|_ x and
A6: not r _|_ y;
A7: not y _|_ r by A6,Th2;
    PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A4,A6,Def3;
    then
A8: 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 A4,A5,Th2;
    then
A9: PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,x)*ProJ(x,r,y)) by A7,A8,Th27;
    PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A4,A5,Def3;
    hence thesis by A9,GROUP_1:def 3;
  end;
  now
    assume x _|_ y;
    then y _|_ x & PProJ(a,b,y,x) = 0.F by A1,Th2,Th29;
    hence thesis by A1,Th29;
  end;
  hence thesis by A2;
end;

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

theorem
  not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) + PProJ(a,b,x,z)
proof
  set 0F = 0.F;
  assume
A1: not b _|_ a;
A2: now
    assume
A3: x <> 0.S;
    a <> 0.S by A1,Th1,Th2;
    then
    ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A3,Def1;
    then consider p such that
A4: ( not p _|_ a)& not p _|_ x;
A5: 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,A4,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,A4,Def3,Th13;
    hence thesis by A5,VECTSP_1:def 7;
  end;
  now
    assume
A6: x = 0.S;
    then
A7: PProJ (a,b,x,z) = 0F by A1,Th28;
    PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F by A1,A6,Th28;
    hence thesis by A7,RLVECT_1:4;
  end;
  hence thesis by A2;
end;