The Mizar article:

Construction of a bilinear antisymmetric form in symplectic vector space

by
Eugeniusz Kusak,
Wojciech Leonczuk, and
Michal Muzalewski

Received November 23, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: SYMSP_1
[ MML identifier index ]


environ

 vocabulary VECTSP_1, RLVECT_1, BINOP_1, FUNCT_1, RELAT_1, ARYTM_1, SYMSP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, DOMAIN_1,
      STRUCT_0, RLVECT_1, BINOP_1, VECTSP_1, RELSET_1;
 constructors DOMAIN_1, BINOP_1, VECTSP_1, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, SUBSET_1, VECTSP_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, STRUCT_0;
 theorems BINOP_1, VECTSP_1, TARSKI, RELSET_1, ZFMISC_1, RLVECT_1;
 schemes BINOP_1, FUNCT_2, XBOOLE_0;

begin :: 1. SYMPLECTIC VECTOR SPACE STRUCTURE

 reserve F for Field;

definition let F;
 struct (VectSpStr over F) SymStr over F
              (# carrier -> set,
                add -> BinOp of the carrier,
                Zero -> Element of the carrier,
                lmult -> Function of [:the carrier of F, the carrier:],
                                   the carrier,
                2_arg_relation -> Relation of the carrier #);
end;

definition let F;
 cluster non empty SymStr over F;
 existence
  proof
    consider X being non empty set,
             a being BinOp of X,
             Z being Element of X,
             l being Function of [:the carrier of F, X:], X,
             r being 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;

definition let F; let S be SymStr over F;
  let a,b be Element of S;
  pred a _|_ b means
  :Def1: [a,b] in the 2_arg_relation of S;
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 BinOpLambda;

Lm2:
now let F;
set CV = [:X,X:];
defpred P[set] means ex a,b being Element of X st $1 = [a,b] & b = o;
consider mo being set such that A1:
 for x being set holds x in mo iff x in CV & P[x] from Separation;
   mo c= CV
 proof
  let x be set;
  thus thesis by A1;
 end;
then reconsider mo as Relation of X by RELSET_1:def 1;
 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;

definition 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
 proof
   thus the carrier of SymStr (# X,md,o,mF,mo #) is non empty;
 end;
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,y being Element of H holds x+y = y+x
   proof
    let x,y be Element of H;
    A2: y+x = md.(y,x) by RLVECT_1:5;
    reconsider x,y as Element of X;
      md.(x,y) = o & md.(y,x) = o by Lm1;
    hence thesis by A2,RLVECT_1:5;
   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;
    A4: (x+y)+z = md.((x+y),z) by RLVECT_1:5;
       x+(y+z) = md.(x,(y+z)) by RLVECT_1:5;
    then A5: x+(y+z) = md.(x,md.(y,z)) by RLVECT_1:5;
    reconsider x,y,z as Element of X;
       md.(x,md.(y,z)) = o by Lm1;
    hence thesis by A4,A5,Lm1;
   end;
  A6: for x being Element of H holds x+0.H = x
   proof
    let x be Element of H;
    A7: x+0.H = md.(x,0.H) by RLVECT_1:5;
    reconsider x as Element of X;
       md.(x,0.H) = o by Lm1;
    hence thesis by A7,TARSKI:def 1;
   end;
    for x being Element of H
   ex y being Element of H st x+y = 0.H
   proof
    let x be Element of H;
A8: x+(-x) = md.(x,(-x)) by RLVECT_1:5;
A9:  0.H = o by RLVECT_1:def 2;
    take -x;
    thus thesis by A8,A9,Lm1;
   end;
  hence thesis by A1,A3,A6,VECTSP_1:7;
 end;

definition let F;
 cluster Abelian add-associative right_zeroed right_complementable
                   (non empty SymStr over F);
 existence
  proof consider mF being
    Function of [:the carrier of F,X:],X;
    consider mo being Relation of 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 #);
 thus MPS is VectSp-like
 proof
    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*(v+w) = x*v+x*w
    proof
     A4: v+w = md.(v,w) by A2,RLVECT_1:5;
     reconsider v,w as Element of X by A2;
     A5: md.(v,w) = o by Lm1;
     reconsider v,w as Element of MPS;
     A6: x*(v+w) = mF.(x,o) by A2,A4,A5,VECTSP_1:def 24;
        mF.(x,o) = mF.[x,o] by BINOP_1:def 1;
     then A7: x*(v+w) = o by A1,A6;
        mF.(x,v) = mF.[x,v] by BINOP_1:def 1;
     then mF.(x,v) = o by A1;
     then A8: x*v = o by A2,VECTSP_1:def 24;
        mF.(x,w) = mF.[x,w] by BINOP_1:def 1;
     then mF.(x,w) = o by A1;
     then A9: x*w = o by A2,VECTSP_1:def 24;
        o = 0.MPS by A2,RLVECT_1:def 2;
     hence thesis by A7,A8,A9,RLVECT_1:10;
    end;
   A10: (x+y)*v = x*v+y*v
    proof
     set z = x+y;
     A11: z*v = mF.(z,v) by A2,VECTSP_1:def 24;
     reconsider v as Element of MPS;
A12:      mF.(z,v) = mF.[z,v] by BINOP_1:def 1;
     reconsider v as Element of MPS;
     A13: (x+y)*v = o by A1,A2,A11,A12;
     reconsider v as Element of MPS;
        mF.(x,v) = mF.[x,v] by BINOP_1:def 1;
     then A14: mF.(x,v) = o by A1,A2;
     reconsider v as Element of MPS;
     A15: x*v = o by A2,A14,VECTSP_1:def 24;
     reconsider v as Element of MPS;
        mF.(y,v) = mF.[y,v] by BINOP_1:def 1;
     then A16: mF.(y,v) = o by A1,A2;
     reconsider v as Element of MPS;
     A17: y*v = o by A2,A16,VECTSP_1:def 24;
        o = 0.MPS by A2,RLVECT_1:def 2;
     hence thesis by A13,A15,A17,RLVECT_1:10;
    end;
   A18: (x*y)*v = x*(y*v)
    proof
     set z = x*y;
     A19: z*v = mF.(z,v) by A2,VECTSP_1:def 24;
     reconsider v as Element of MPS;
A20:      mF.(z,v) = mF.[z,v] by BINOP_1:def 1;
     reconsider v as Element of MPS;
     A21: (x*y)*v = o by A1,A2,A19,A20;
     reconsider v as Element of MPS;
        mF.(y,v) = mF.[y,v] by BINOP_1:def 1;
     then A22: mF.(y,v) = o by A1,A2;
     reconsider v as Element of MPS;
        y*v = o by A2,A22,VECTSP_1:def 24;
     then A23: x*(y*v) = mF.(x,o) by A2,VECTSP_1:def 24;
        mF.(x,o) = mF.[x,o] by BINOP_1:def 1;
     hence thesis by A1,A21,A23;
    end;
      (1_ F)*v = v
    proof
     set one = 1_ F;
     A24: one*v = mF.(one,v) by A2,VECTSP_1:def 24;
     A25: mF.(one,v) = mF.[one,v] by BINOP_1:def 1;
     reconsider v as Element of MPS;
        mF.(one,v) = o by A1,A2,A25;
     hence thesis by A2,A24,TARSKI:def 1;
    end;
   hence thesis by A3,A10,A18;
  end;
  hence thesis by VECTSP_1:def 26;
 end;
end;

Lm5:
now let F;
 let mF be Function of [:the carrier of F,X:],X such that
   for a being Element of F
      for x being Element of X holds
      mF.[a,x] = o;
set CV = [: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 #);
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,Def1;
  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: 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 ZFMISC_1:33;
    end;
     b = o implies a _|_ b
    proof
     assume A6: b = o;
     consider c,d being Element of MPS such that A7: c = a &
     d = b;
        [a,b] = [c,d] by A7;
     hence thesis by A2,A3,A6;
    end;
  hence thesis by A5;
 end;

   0.MPS = o by A2,TARSKI:def 1;

 hence 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;

 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 b _|_ a & c _|_ a;
  then a = o by A4;
  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 A8: not b _|_ a;
  assume not thesis;
     a <> o by A4,A8;
  hence contradiction by A2,TARSKI:def 1;
 end;
  let a,b,c be Element of MPS;
  assume a _|_ b+c & 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
 :Def2: 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 the carrier
            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;

definition let F;
 cluster SymSp-like VectSp-like strict
  (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 Lambda2D;
     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 the carrier
       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 A1,A2,Lm5;
    thus MPS is VectSp-like by A1,Lm4;
    thus thesis;
   end;
end;

definition let F;
 mode SymSp of F is SymSp-like VectSp-like
   (Abelian add-associative right_zeroed right_complementable
      (non empty SymStr over F));
end;


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

canceled 10;

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

theorem
Th12: a _|_ b implies b _|_ a
 proof
  set 0V = 0.S;
  assume a _|_ b;
  then a _|_ 0V+b & 0V _|_ b+a by Th11,RLVECT_1:10;
  then b _|_ a+0V by Def2;
  hence thesis by RLVECT_1:10;
 end;

theorem
Th13: not a _|_ b & c+a _|_ b implies not c _|_ b
 proof
  assume A1:not a _|_ b & c+a _|_ b;
  assume not thesis;
  then (-1_ F)*c _|_ b by Def2;
  then -c _|_ b by VECTSP_1:59;
  then -c+(c+a) _|_ b by A1,Def2;
  then (c+(-c))+a _|_ b by RLVECT_1:def 6;
  then 0.S+a _|_ b by RLVECT_1:16;
  hence contradiction by A1,RLVECT_1:10;
 end;

theorem
Th14: not b _|_ a & c _|_ a implies not b+c _|_ a
 proof
  assume A1:not b _|_ a & c _|_ a;
  assume A2:not thesis;
    (-1_ F)*c _|_ a by A1,Def2;
  then -c _|_ a by VECTSP_1:59;
  then (b+c)+(-c) _|_ a by A2,Def2;
  then b+(c+(-c)) _|_ a by RLVECT_1:def 6;
  then b+0.S _|_ a by RLVECT_1:16;
  hence contradiction by A1,RLVECT_1:10;
 end;

theorem
Th15: not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a
 proof
  set 1F = 1_ F;
  assume A1: not b _|_ a & not l=0.F;
  A2:now assume A3:l*b _|_ a;
   consider k such that A4:l*k=1F by A1,VECTSP_1:def 20;
     k*(l*b) _|_ a by A3,Def2;
   then 1F*b _|_ a by A4,VECTSP_1:def 26;
   hence contradiction by A1,VECTSP_1:def 26;
  end;
    now assume b _|_ l*a;
   then A5:l*a _|_ b by Th12;
   consider k such that A6:l*k=1F by A1,VECTSP_1:def 20;
     k*(l*a) _|_ b by A5,Def2;
   then 1F*a _|_ b by A6,VECTSP_1:def 26;
   then a _|_ b by VECTSP_1:def 26;
   hence contradiction by A1,Th12;
  end;
  hence thesis by A2;
 end;

theorem
Th16: a _|_ b implies -a _|_ b
 proof
  assume a _|_ b;
  then (-1_ F)*a _|_ b by Def2;
  hence thesis by VECTSP_1:59;
 end;

canceled 2;

theorem
Th19: 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 not thesis;
    then a+b _|_ c & (1F*a+1_ F*a)+b _|_ c by VECTSP_1:def 26;
    then a+b _|_ c & (a+1F*a)+b _|_ c by VECTSP_1:def 26;
    then a+b _|_ c & (a+a)+b _|_ c by VECTSP_1:def 26;
    then a+(a+b) _|_ c & (a+b) _|_ c by RLVECT_1:def 6;
  hence contradiction by A1,Th14;
 end;

theorem
Th20: not a' _|_ a & a' _|_ b & not b' _|_ b & b' _|_ a implies not a'+b' _|_
a & not a'+b' _|_ b
 proof
 set 0V = 0.S;
 assume A1: not a' _|_ a & a' _|_ b & not b' _|_ b & b' _|_ a;
 assume not thesis;
       then (a'+b' _|_ a & (-(1_ F))*b' _|_ a) or (a'+b' _|_ b &
            (-(1_ F))*a' _|_ b) by A1,Def2;
       then (a'+b' _|_ a & -b' _|_ a) or (a'+b' _|_ b & -a' _|_ b)
       by VECTSP_1:59;
       then (a'+b')+(-b') _|_ a or -a'+(a'+b') _|_ b by Def2;
       then a'+(b'+(-b')) _|_ a or (-a'+a')+b' _|_ b by RLVECT_1:def 6;
       then a'+0V _|_ a or 0V+b' _|_ b by RLVECT_1:16;
       hence contradiction by A1,RLVECT_1:10;
       end;

theorem
Th21: a<>0.S & b<>0.S implies ex p st not p _|_ a & not p _|_ b
  proof
  assume A1: a<>0.S & b<>0.S;
  then consider a' such that A2: not a' _|_ a by Def2;
     now assume A3: a' _|_ b;
  consider b' such that A4: not b' _|_ b by A1,Def2;
     now assume b' _|_ a;
   then not a'+b' _|_ a & not a'+b' _|_ b by A2,A3,A4,Th20; hence thesis;
end;
   hence thesis by A4; end;
   hence thesis by A2; end;

theorem
Th22: 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 A1: 1_ F+1_ F<>0.F & a<>0.S & b<>0.S & c <>0.S;
 then consider r such that A2: not r _|_ a & not r _|_ b by Th21;
 consider s such that A3: not s _|_ a & not s _|_ c by A1,Th21;
    now assume that A4: r _|_ c and A5: s _|_ b;
    A6: now assume A7: not r+s _|_ a;
      not r+s _|_ b & not r+s _|_ c by A2,A3,A4,A5,Th14;
    hence thesis by A7; end;
       now assume A8: not (1_ F+1_ F)*r+s _|_ a;
      not (1_ F+1_ F)*r+s _|_ b & not (1_ F+1_ F)*r+s _|_ c
     proof
         not (1_ F+1_ F)*r _|_ b & (1_ F+1_ F)*r _|_ c by A1,A2,A4,Def2,Th15;
       hence thesis by A3,A5,Th14;
     end;
    hence thesis by A8; end;
 hence thesis by A2,A6,Th19; end;
 hence thesis by A2,A3;
end;

theorem
Th23: a-b _|_ d & a-c _|_ d implies b-c _|_ d
 proof
  assume a-b _|_ d & a-c _|_ d;
  then -(a-b) _|_ d & a-c _|_ d by Th16;
  then -a+b _|_ d & a-c _|_ d by VECTSP_1:64;
  then b+(-a)+(a-c) _|_ d by Def2;
  then b+((-a)+(a-c)) _|_ d by RLVECT_1:def 6;
  then b+(-a+(a+(-c))) _|_ d by RLVECT_1:def 11;
  then b+((-a+a)+(-c)) _|_ d by RLVECT_1:def 6;
  then b+((0.S)+(-c)) _|_ d by RLVECT_1:16;
  then b+(-c) _|_ d by RLVECT_1:10;
  hence thesis by RLVECT_1:def 11;
 end;

theorem
Th24: not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
 proof
  assume A1:not b _|_ a & x-k*b _|_ a & x-l*b _|_ a;
  assume A2:not thesis;
  set 1F=1_ F;
    k*b-l*b _|_ a by A1,Th23;
  then k*b+(-l*b) _|_ a by RLVECT_1:def 11;
  then k*b+((-1F)*(l*b)) _|_ a by VECTSP_1:59;
  then k*b+(((-1F)*l)*b) _|_ a by VECTSP_1:def 26;
  then k*b+(-(l*(1F)))*b _|_ a by VECTSP_1:41;
  then k*b+(-l)*b _|_ a by VECTSP_1:def 19;
  then (k+(-l))*b _|_ a by VECTSP_1:def 26;
  then (k+(-l))"*((k+(-l))*b) _|_ a by Def2;
  then A3: ((k+(-l))"*(k+(-l)))*b _|_ a by VECTSP_1:def 26;
    k-l<>0.F by A2,RLVECT_1:35;
  then k+(-l)<>0.F by RLVECT_1:def 11;
  then (1F)*b _|_ a by A3,VECTSP_1:def 22;
  hence contradiction by A1,VECTSP_1:def 26;
 end;

theorem
Th25: 1_ F+1_ F<>0.F implies a _|_ a
 proof
  assume A1: 1_ F+1_ F<>0.F;
  set 1F = 1_ F;
    now assume a <> 0.S;
    then consider c such that A2: not c _|_ a by Def2;
    consider k such that A3: a-k*c _|_ a by A2,Def2;
      a _|_ a-k*c by A3,Th12;
    then a _|_ a+(-k*c) & a _|_ (-k*c)+a by RLVECT_1:def 11;
    then -k*c _|_ a+a by Def2;
    then -k*c _|_ a+(1F)*a by VECTSP_1:def 26;
    then -k*c _|_ (1F)*a+(1F)*a by VECTSP_1:def 26;
    then (-1F)*(k*c) _|_ (1F)*a+(1F)*a by VECTSP_1:59;
    then (-1F)*(k*c) _|_ ((1F)+(1F))*a by VECTSP_1:def 26;
    then ((-1F)*k)*c _|_ ((1F)+(1F))*a by VECTSP_1:def 26;
    then (-(k*(1F)))*c _|_ ((1F)+(1F))*a by VECTSP_1:41;
    then (-k)*c _|_ ((1_ F)+(1F))*a by VECTSP_1:def 19;
    then ((1_ F)+(1_ F))*a _|_ (-k)*c by Th12;
    then ((1_ F)+(1_ F))"*(((1_ F)+(1_ F))*a) _|_ (-k)*c by Def2;
    then a _|_ (-k)*c by A1,VECTSP_1:67;
    then A4: (-k)*c _|_ a by Th12;
      a+(-k)*c _|_ a by A3,VECTSP_1:68;
    hence thesis by A4,Th14;
   end;
  hence thesis by Th11;
end;

::
::                      5. ORTHOGONAL PROJECTION
::

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

 func ProJ(a,b,x) -> Element of F means
 :Def6: 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,Def2;
   take k;
   let l be Element of F;
   assume x-l*b _|_ a;
   hence thesis by A1,A2,Th24;
  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,Def2;
     l1 = k by A3,A5;
   hence thesis by A4,A5;
  end;
end;

canceled;

theorem
Th27: 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 Def2;
  hence thesis by A1,Def6;
 end;

theorem
Th28: not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x)
 proof
  assume A1: not b _|_ a;
  set L = x-ProJ(a,b,x)*b;
  A2: L _|_ a by A1,Th27;
     l*L = l*x-l*(ProJ(a,b,x)*b) by VECTSP_1:70
          .= l*x-(l*ProJ(a,b,x))*b by VECTSP_1:def 26;
  then A3: l*x-(l*ProJ(a,b,x))*b _|_ a by A2,Def2;
    l*x - ProJ(a,b,l*x)*b _|_ a by A1,Th27;
  hence thesis by A1,A3,Th24;
end;

theorem
Th29:not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y)
 proof
  set 1F = 1_ F;
  assume A1: not b _|_ a;
  then A2: x-ProJ(a,b,x)*b _|_ a & y-ProJ(a,b,y)*b _|_ a by Th27;
  set L = (x-ProJ(a,b,x)*b)+(y-ProJ(a,b,y)*b);
  A3: L _|_ a by A2,Def2;
  A4: now thus L = (x+(-ProJ(a,b,x)*b))+(y-ProJ(a,b,y)*b) by RLVECT_1:def 11
        .= (x+(-ProJ(a,b,x)*b))+(y+(-ProJ(a,b,y)*b)) by RLVECT_1:def 11
        .= (((-ProJ(a,b,x)*b)+x)+y)+(-ProJ(a,b,y)*b) by RLVECT_1:def 6
        .= ((x+y)+(-ProJ(a,b,x)*b))+(-ProJ(a,b,y)*b) by RLVECT_1:def 6
        .= (x+y)+((-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by RLVECT_1:def 6
        .= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by VECTSP_1:def 26
        .= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(1F)*(-ProJ
(a,b,y)*b)) by VECTSP_1:def 26
        .= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*(-ProJ(a,b,y)*b)) by VECTSP_1:68
        .= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*((-ProJ
(a,b,y))*b)) by VECTSP_1:68
        .= (x+y)+(((1F)*(-ProJ(a,b,x)))*b+(1F)*((-ProJ
(a,b,y))*b)) by VECTSP_1:def 26
        .= (x+y)+(((-ProJ(a,b,x))*(1F))*b+((1F)*(-ProJ(a,b,y)))*b) by VECTSP_1:
def 26
        .= (x+y)+((-ProJ(a,b,x))*b+((-ProJ(a,b,y))*(1F))*b) by VECTSP_1:def 19
        .= (x+y)+((-ProJ(a,b,x))*b+(-ProJ(a,b,y))*b) by VECTSP_1:def 19
        .= (x+y)+((-ProJ(a,b,x))+(-ProJ(a,b,y)))*b by VECTSP_1:def 26
        .= (x+y)+(-(ProJ(a,b,x)+ProJ(a,b,y)))*b by RLVECT_1:45
        .= (x+y)-(ProJ(a,b,x)+ProJ(a,b,y))*b by VECTSP_1:68; end;
    (x+y)-ProJ(a,b,x+y)*b _|_ a by A1,Th27;
  hence thesis by A1,A3,A4,Th24;
 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;
  A3: x-ProJ(a,b,x)*b _|_ a by A1,Th27;
A4:  not l*b _|_ a by A1,A2,Th15;
  set L = x-ProJ(a,l*b,x)*(l*b);
  A5: L _|_ a by A4,Th27;
    L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 26;
  then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A3,A5,Th24;
  then ProJ(a,b,x)*l" = ProJ(a,l*b,x)*(l*l") by VECTSP_1:def 16;
  then l"*ProJ(a,b,x) = ProJ(a,l*b,x)*(1_ F) by A2,VECTSP_1:def 22;
  hence thesis by VECTSP_1:def 19;
 end;

theorem
Th31: 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,Th15;
  then A3: x-ProJ(a,b,x)*b _|_ a & x-ProJ(l*a,b,x)*b _|_ l*a by A1,Th27;
  then l*a _|_ x-ProJ(l*a,b,x)*b by Th12;
  then l"*(l*a) _|_ x-ProJ(l*a,b,x)*b by Def2;
  then (l"*l)*a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 26;
  then 1_ F*a _|_ x-ProJ(l*a,b,x)*b by A2,VECTSP_1:def 22;
  then a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 26;
  then x-ProJ(l*a,b,x)*b _|_ a by Th12;
  hence thesis by A1,A3,Th24;
 end;

theorem
Th32: 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 A1: not b _|_ a & p _|_ a;
  then not b+p _|_ a by Th14;
  then A2: c-ProJ(a,b,c)*b _|_ a & c+p-ProJ(a,b,c+p)*b _|_ a &
          c-ProJ(a,b+p,c)*(b+p) _|_ a by A1,Th27;
  A3: ProJ(a,b+p,c)*p _|_ a by A1,Def2;
  A4: -p _|_ a by A1,Th16;
    c-(ProJ(a,b+p,c)*b+ProJ(a,b+p,c)*p) _|_ a by A2,VECTSP_1:def 26;
  then c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p _|_ a by VECTSP_1:64;
  then c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p+ProJ(a,b+p,c)*p _|_ a by A3,Def2;
  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 11;
  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 11;
  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 6;
  then c+(-ProJ(a,b+p,c)*b)+0V _|_ a by RLVECT_1:16;
  then c+(-ProJ(a,b+p,c)*b) _|_ a by RLVECT_1:10;
  then A5: c-ProJ(a,b+p,c)*b _|_ a by RLVECT_1:def 11;
    -p+(p+c-ProJ(a,b,c+p)*b) _|_ a by A2,A4,Def2;
  then -p+(p+c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 11;
  then -p+(p+(c+(-ProJ(a,b,c+p)*b))) _|_ a by RLVECT_1:def 6;
  then (-p+p)+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 6;
  then 0V+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:16;
  then c+(-ProJ(a,b,c+p)*b) _|_ a by RLVECT_1:10;
  then c-ProJ(a,b,c+p)*b _|_ a by RLVECT_1:def 11;
  hence thesis by A1,A2,A5,Th24;
 end;

theorem
Th33: not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c)
 proof
  assume A1: not b _|_ a & p _|_ b & p _|_ c;
  then not a _|_ b by Th12;
  then not a+p _|_ b by A1,Th14;
  then A2: not b _|_ a+p by Th12;
  then A3: c-ProJ(a,b,c)*b _|_ a & c-ProJ(a+p,b,c)*b _|_ a+p by A1,Th27;
    c _|_ p & b _|_ p by A1,Th12;
  then c _|_ p & ProJ(a,b,c)*b _|_ p by Def2;
  then c _|_ p & -(ProJ(a,b,c)*b) _|_ p by Th16;
  then c+(-(ProJ(a,b,c)*b)) _|_ p by Def2;
  then c-ProJ(a,b,c)*b _|_ p by RLVECT_1:def 11;
  then A4: p _|_ c-ProJ(a,b,c)*b by Th12;
    a _|_ c-ProJ(a,b,c)*b by A3,Th12;
  then a+p _|_ c-ProJ(a,b,c)*b by A4,Def2;
  then c-ProJ(a,b,c)*b _|_ a+p by Th12;
  hence thesis by A2,A3,Th24;
 end;

theorem
Th34: not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_ F
 proof
  assume A1: not b _|_ a & c-b _|_ a;
  then A2: c-(1_ F)*b _|_ a by VECTSP_1:def 26;
    c-ProJ(a,b,c)*b _|_ a by A1,Th27;
  hence thesis by A1,A2,Th24;
 end;

theorem
Th35: not b _|_ a implies ProJ(a,b,b) = 1_ F
 proof
  assume A1: not b _|_ a;
    b+(-b) = 0.S by RLVECT_1:16;
  then b-b = 0.S by RLVECT_1:def 11;
  then b-b _|_ a by Th11;
  hence thesis by A1,Th34;
 end;

theorem
Th36: not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F )
 proof
  set 0F = 0.F, 0V = 0.S;
   A1: now assume A2: not b _|_ a & x _|_ a;
   then A3: x-ProJ(a,b,x)*b _|_ a by Th27;
     x+0V _|_ a by A2,RLVECT_1:10;
   then x+(-0V) _|_ a by RLVECT_1:25;
   then x+(-(0F*b)) _|_ a by VECTSP_1:59;
   then x-0F*b _|_ a by RLVECT_1:def 11;
   hence ProJ(a,b,x) = 0.F by A2,A3,Th24;
   end;
     now assume not b _|_ a & ProJ(a,b,x) = 0.F;
   then x-0F*b _|_ a by Th27;
   then x-0V _|_ a by VECTSP_1:59;
   then x+(-0V) _|_ a by RLVECT_1:def 11;
   then x+0V _|_ a by RLVECT_1:25;
   hence x _|_ a by RLVECT_1:10;
  end;
  hence thesis by A1;
 end;

theorem
Th37: not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p)
 proof
  assume A1: not b _|_ a & not q _|_ a;
  then A2: p-ProJ(a,b,p)*b _|_ a & ProJ(a,q,p)*q-
  ProJ(a,b,ProJ(a,q,p)*q)*b _|_ a &
  p-ProJ(a,q,p)*q _|_ a by Th27;
  then (p-ProJ(a,q,p)*q)+(ProJ(a,q,p)*q-ProJ(a,b,ProJ(a,q,p)*q)*b) _|_ a
  by Def2;
  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 11;
  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 11;
  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 6;
  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 6;
  then p+0.S+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:16;
  then p+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:10;
  then p-(ProJ(a,b,ProJ(a,q,p)*q)*b) _|_ a by RLVECT_1:def 11;
  then p-(ProJ(a,q,p)*ProJ(a,b,q))*b _|_ a by A1,Th28;
  then A3: ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A2,Th24;
  A4: ProJ(a,b,q) <> 0.F by A1,Th36;
    ProJ(a,q,p)*(ProJ(a,b,q)*ProJ(a,b,q)") = ProJ(a,b,p)*ProJ
(a,b,q)" by A3,VECTSP_1:def 16;
  then ProJ(a,q,p)*1_ F = ProJ(a,b,p)*ProJ(a,b,q)" by A4,VECTSP_1:def 22;
  hence thesis by VECTSP_1:def 19;
 end;

theorem
Th38: not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"
 proof
  set 1F = 1_ F, 0F = 0.F;
  assume A1: not b _|_ a & not c _|_ a;
  then ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by Th37;
  then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th35;
  then A2: ProJ(a,b,c)" = ProJ(a,c,b) by VECTSP_1:def 19;
  A3: ProJ(a,c,b) <> 0F & ProJ(a,b,c) <> 0F by A1,Th36;
  then 1F = ProJ(a,c,b)*ProJ(a,b,c) by A2,VECTSP_1:def 22;
  then ProJ(a,c,b)" = ProJ(a,c,b)"*(ProJ(a,c,b)*ProJ(a,b,c)) by VECTSP_1:def 19
               .= (ProJ(a,c,b)"*ProJ(a,c,b))*ProJ(a,b,c) by VECTSP_1:def 16
               .= ProJ(a,b,c)*1F by A3,VECTSP_1:def 22;
  hence thesis by VECTSP_1:def 19;
 end;

theorem
Th39: not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = ProJ(c,b,a)
 proof
  assume A1: not b _|_ a & b _|_ c+a;
  then not a _|_ b & c+a _|_ b by Th12;
  then not c _|_ b by Th13;
  then A2: not b _|_ c by Th12;
    c-ProJ(a,b,c)*b _|_ a by A1,Th27;
  then -ProJ(a,b,c)*b+c _|_ a by RLVECT_1:def 11;
  then A3: a _|_ -ProJ(a,b,c)*b+c by Th12;
    ProJ(a,b,c)*b _|_ c+a by A1,Def2;
  then -ProJ(a,b,c)*b _|_ c+a by Th16;
  then c _|_ a+(-ProJ(a,b,c)*b) by A3,Def2;
  then c _|_ a-ProJ(a,b,c)*b by RLVECT_1:def 11;
  then A4: a-ProJ(a,b,c)*b _|_ c by Th12;
    a-ProJ(c,b,a)*b _|_ c by A2,Th27;
  hence thesis by A2,A4,Th24;
 end;

theorem
Th40: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 A1: not a _|_ b & not c _|_ b;
   then A2: ProJ(b,a,c) <> 0.F by Th36;
   then (-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by VECTSP_1:def 22;
   then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F)*(1F) by VECTSP_1:def 16;
   then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F) by VECTSP_1:def 19;
   then (-(ProJ(b,a,c)"*(1F)))*ProJ(b,a,c) = -1F by VECTSP_1:41;
   then (-ProJ(b,a,c)")*ProJ(b,a,c) = -1F by VECTSP_1:def 19;
   then ProJ(b,a,(-ProJ(b,a,c)")*c) = -1F by A1,Th28;
   then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th27;
   then (-ProJ(b,a,c)")*c-(-a) _|_ b by VECTSP_1:59;
   then (-ProJ(b,a,c)")*c+(-(-(a))) _|_ b by RLVECT_1:def 11;
   then (-ProJ(b,a,c)")*c+a _|_ b by RLVECT_1:30;
   then A3: b _|_ (-ProJ(b,a,c)")*c+a by Th12;
   A4:not b _|_ a & not b _|_ c by A1,Th12;
   then A5: ProJ(a,b,(-ProJ(b,a,c)")*c) = ProJ((-ProJ
(b,a,c)")*c,b,a) by A3,Th39;
     -ProJ(b,a,c)" <> 0.F by A2,VECTSP_1:74;
   then ProJ(a,b,(-ProJ(b,a,c)")*c) = ProJ(c,b,a) by A4,A5,Th31;
   hence thesis by A4,Th28;
  end;

theorem
Th41: (1_ F+1_ F<>0.F) & not a _|_ p & not a _|_ q & not b _|_ p & not b _|_ q
  implies
      ProJ(a,p,q)*ProJ(b,q,p) = ProJ(p,a,b)*ProJ(q,b,a)
 proof
  assume A1: (1_ F+1_ F<>0.F) & not a _|_ p & not a _|_ q & not b _|_ p &
  not b _|_ q;
   A2: now assume A3: not p _|_ q;
   then A4:not p _|_ a & not q _|_ b & not q _|_ p by A1,Th12;
   then ProJ(a,p,q) = (-ProJ(p,q,a)")*ProJ(q,p,a) &
   ProJ(b,q,p) = (-(ProJ(q,p,b)"))*ProJ(p,q,b) by A1,A3,Th40;
   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 VECTSP_1:def 16
   .= (ProJ(q,p,a)*((-ProJ(p,q,a)")*(-ProJ(q,p,b)")))*ProJ
(p,q,b) by VECTSP_1:def 16
   .= (ProJ(q,p,a)*(ProJ(q,p,b)"*ProJ(p,q,a)"))*ProJ(p,q,b) by VECTSP_1:42
   .= ((ProJ(q,p,a)*ProJ(q,p,b)")*ProJ(p,q,a)")*ProJ(p,q,b) by VECTSP_1:def 16
   .= (ProJ(q,b,a)*ProJ(p,q,a)")*ProJ(p,q,b) by A1,A3,Th37
   .= ProJ(q,b,a)*(ProJ(p,q,b)*ProJ(p,q,a)") by VECTSP_1:def 16
   .= ProJ(q,b,a)*ProJ(p,a,b) by A1,A4,Th37;
   hence thesis;
   end;
   A5: now assume A6: not a _|_ b;
   then A7: not b _|_ a & not p _|_ a & not q _|_ a & not p _|_ b & not q _|_
b by A1,Th12;
   then ProJ(p,a,b) = (-ProJ(a,b,p)")*ProJ(b,a,p) &
   ProJ(q,b,a) = (-ProJ(b,a,q)")*ProJ(a,b,q) by A6,Th40;
   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 VECTSP_1:def 16
   .= (ProJ(b,a,p)*((-ProJ(a,b,p)")*(-ProJ(b,a,q)")))*ProJ
(a,b,q) by VECTSP_1:def 16
   .= (ProJ(b,a,p)*(ProJ(b,a,q)"*ProJ(a,b,p)"))*ProJ(a,b,q) by VECTSP_1:42
   .= ((ProJ(b,a,p)*ProJ(b,a,q)")*ProJ(a,b,p)")*ProJ(a,b,q) by VECTSP_1:def 16
   .= (ProJ(b,q,p)*ProJ(a,b,p)")*ProJ(a,b,q) by A6,A7,Th37
   .= ProJ(b,q,p)*(ProJ(a,b,q)*ProJ(a,b,p)") by VECTSP_1:def 16
   .= ProJ(b,q,p)*ProJ(a,p,q) by A7,Th37;
   hence thesis;
   end;
      now assume A8: p _|_ q & a _|_ b;
   then A9: q _|_ p & b _|_ a & not p _|_ a & not q _|_ a & not p _|_ b &
   not q _|_ b & a _|_ a by A1,Th12,Th25;
   then A10: ProJ(a,p,q) = ProJ(a,p+a,q) & ProJ(b,q,p) = ProJ
(b,q,p+a) by A8,Th32;
   A11:not p+a _|_ a by A9,Th14;
   A12: not p+a _|_ q by A1,A8,Th14;
   then A13: not a _|_ p+a & not q _|_ p+a & not p+a _|_ q by A11,Th12;
   then ProJ(a,p+a,q) = (-ProJ(p+a,q,a)")*ProJ(q,p+a,a) &
   ProJ(b,q,p+a) = (-ProJ(q,p+a,b)")*ProJ(p+a,q,b) by A1,Th40;
   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 A10,VECTSP_1:def 16
   .= (ProJ(q,p+a,a)*((-ProJ(p+a,q,a)")*(-ProJ(q,p+a,b)")))*ProJ
(p+a,q,b) by VECTSP_1:def 16
   .= (ProJ(q,p+a,a)*(ProJ(q,p+a,b)"*ProJ(p+a,q,a)"))*ProJ(p+a,q,b) by VECTSP_1
:42
   .= ((ProJ(q,p+a,a)*ProJ(q,p+a,b)")*ProJ(p+a,q,a)")*ProJ
(p+a,q,b) by VECTSP_1:def 16
   .= (ProJ(q,b,a)*ProJ(p+a,q,a)")*ProJ(p+a,q,b) by A1,A12,Th37
   .= ProJ(q,b,a)*(ProJ(p+a,q,b)*ProJ(p+a,q,a)") by VECTSP_1:def 16
   .= ProJ(q,b,a)*ProJ(p+a,a,b) by A13,Th37
   .= ProJ(q,b,a)*ProJ(p,a,b) by A1,A8,A9,Th33;
   hence thesis;
   end;
   hence thesis by A2,A5;
  end;

theorem
Th42: (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 A1: (1_ F+1_ F<>0.F) & not p _|_ a & not p _|_ x & not q _|_ a &
  not q _|_ x;
  then A2: not a _|_ p & not x _|_ p & not a _|_ q & not x _|_ q by Th12;
    ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,p,q)*ProJ(x,q,p) by A1,Th41;
  then A3: ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,q,p)"*ProJ(x,q,p) by A1,Th38;
  A4: ProJ(a,q,p) <> 0F by A1,Th36;
    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 A3,VECTSP_1:def 16;
  then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ
(x,q,p)*(1F) by A4,VECTSP_1:def 22;
  then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ(x,q,p) by VECTSP_1:def 19;
  then (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,x,a) = ProJ(x,q,p) by VECTSP_1:def 16;
  then A5: (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,a,x)" = ProJ(x,q,p) by A2,Th38;
  A6: ProJ(q,a,x) <> 0F by A2,Th36;
    (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 A5,VECTSP_1:def 16;
  then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(x,q,p)*ProJ
(q,a,x) by A6,VECTSP_1:def 22;
  hence thesis by VECTSP_1:def 19;
 end;

theorem
Th43: (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 A1: (1_ F+1_ F<>0.F) & not p _|_ a & not p _|_ x & not q _|_ a &
  not q _|_ x & not b _|_ a;
   A2: now assume y _|_ x;
    then ProJ(x,p,y) = 0F & ProJ(x,q,y) = 0F by A1,Th36;
    then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F &
    ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y) = 0F by VECTSP_1:39;
    hence thesis;
   end;
      now assume A3: not y _|_ x;
     ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x) by A1,Th42;
   then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ
(q,a,x) by A1,Th37;
   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 A1,A3,Th37;
   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 VECTSP_1:def 16;
   then A4: (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 VECTSP_1:def 16;
     ProJ(a,b,q) <> 0F by A1,Th36;
   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 A4,VECTSP_1:def 22;
   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 19
;
   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 A1,A3,Th38;
   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 VECTSP_1:def 16;
   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 VECTSP_1:def 16
;
   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 VECTSP_1:def 16;
   then A5: 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 VECTSP_1:def 16;
     ProJ(x,p,y) <> 0F by A1,A3,Th36;
   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 A5,VECTSP_1:def 22;
   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 19;
   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 A1,A3,Th38;
   hence thesis by VECTSP_1:def 16;
  end;
  hence thesis by A2;
 end;

theorem
Th44: 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 A1: not a _|_ p & not x _|_ p & not y _|_ p;
  then A2: not a _|_ p & not x _|_ p & not y _|_ p & not p _|_ a &
  not p _|_ x & not p _|_ y by Th12;
   A3: now assume y _|_ x;
    then y _|_ x & x _|_ y by Th12;
    then ProJ(x,p,y) = 0F & ProJ(y,p,x) = 0F by A2,Th36;
    then ProJ(p,a,x)*ProJ(x,p,y) = 0F & (-ProJ(p,a,y))*ProJ
(y,p,x) = 0F by VECTSP_1:39;
    hence thesis;
   end;
     now assume A4: not y _|_ x;
   then A5: not y _|_ x & not x _|_ y by Th12;
     ProJ(p,a,y)*ProJ(p,a,x)" = ProJ(p,x,y) by A1,Th37;
   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 A2,A4,Th40;
   then A6: 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 VECTSP_1:def 16;
     ProJ(p,a,x) <> 0F by A1,Th36;
   then ProJ(p,a,y)*(1F) =
         ((-ProJ(x,y,p)")*ProJ(y,x,p))*ProJ(p,a,x) by A6,VECTSP_1:def 22;
   then ProJ(p,a,y) = (ProJ(y,x,p)*(-ProJ(x,y,p)"))*ProJ
(p,a,x) by VECTSP_1:def 19;
   then ProJ(p,a,y) = ProJ(y,x,p)*((-ProJ(x,y,p)")*ProJ
(p,a,x)) by VECTSP_1:def 16;
   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 A2,A5,Th38;
   then A7: 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 VECTSP_1:def 16;
     ProJ(y,p,x) <> 0F by A2,A5,Th36;
   then ProJ(y,p,x)*ProJ(p,a,y) =
            ((-ProJ(x,y,p)")*ProJ(p,a,x))*(1F) by A7,VECTSP_1:def 22;
   then ProJ(p,a,y)*ProJ(y,p,x) =
            (-ProJ(x,y,p)")*ProJ(p,a,x) by VECTSP_1:def 19;
   then -(ProJ(p,a,y)*ProJ(y,p,x)) = -(-ProJ(x,y,p)"*ProJ
(p,a,x)) by VECTSP_1:41;
   then -(ProJ(p,a,y)*ProJ(y,p,x)) = ProJ(x,y,p)"*ProJ(p,a,x) by RLVECT_1:30;
   then (-ProJ(p,a,y))*ProJ(y,p,x) = ProJ(x,y,p)"*ProJ(p,a,x) by VECTSP_1:41;
   hence thesis by A2,A4,Th38;
   end;
  hence thesis by A3;
 end;

::
::                   6. BILINEAR ANTISYMMETRIC FORM
::

definition let F,S,x,y,a,b;
 assume that A1: not b _|_ a and A2: 1_ F+1_ F<>0.F;
 func PProJ(a,b,x,y) -> Element of F means
 :Def7: 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) ,
       it = 0.F if for p holds p _|_ a or p _|_ x;
 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 A3: 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
      ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(a,b,q)*ProJ(q,a,x)*ProJ
(x,q,y) by A1,A2,A3,Th43;
   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 A4: not p _|_ a & not p _|_ x;
     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);
     consider r such that A7: not r _|_ a & not r _|_ x by A4;
        IT1 = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A5,A7;
     hence thesis by A6,A7;
    end;
   thus thesis;
  end;
 consistency;
end;

canceled 2;

theorem
Th47: (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) and A2: not b _|_ a & x=0.S;
    for p holds p _|_ a or p _|_ x
   proof
   let p be Element of S;
     x _|_ p by A2,Th11;
   hence thesis by Th12;
   end;
  hence thesis by A1,A2,Def7;
 end;

Lm6: x _|_ 0.S
 proof
    0.S _|_ x by Th11;
  hence thesis by Th12;
 end;

theorem
Th48: (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,Lm6;
  A4: PProJ(a,b,x,y) = 0.F implies y _|_ x
     proof
      assume A5: PProJ(a,b,x,y) = 0.F;
      A6: now assume for p holds p _|_ a or p _|_ x;
       then x = 0.S by A3,Th21;
       hence thesis by Lm6; end;
         now given p such that A7: not p _|_ a & not p _|_ x;
        ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A2,A5,A7,Def7;
      then ProJ(a,b,p)*ProJ(p,a,x) = 0F or ProJ(x,p,y) = 0F by VECTSP_1:44;
      then A8: ProJ(a,b,p) = 0.F or ProJ(p,a,x) = 0.F or ProJ(x,p,y) = 0.F
      by VECTSP_1:44;
          now assume A9: ProJ(p,a,x) = 0.F;
          not a _|_ p by A7,Th12;
        then x _|_ p by A9,Th36;
        hence contradiction by A7,Th12; end;
      hence thesis by A2,A7,A8,Th36; end;
     hence thesis by A6; end;
     y _|_ x implies PProJ(a,b,x,y) = 0.F
  proof
   assume A10: y _|_ x;
   A11: now assume x = 0.S;
        then for p holds p _|_ a or p _|_ x by Lm6;
        hence thesis by A1,A2,Def7; end;
      now assume x<>0.S;
        then consider p such that A12: not p _|_ a & not p _|_ x by A3,Th21;
          ProJ(x,p,y) = 0F by A10,A12,Th36;
        then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F by VECTSP_1:39;
        hence thesis by A1,A2,A12,Def7; end;
   hence thesis by A11; 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 A1: (1_ F+1_ F<>0.F) & not b _|_ a;
   A2: now assume x _|_ y;
    then y _|_ x & x _|_ y by Th12;
    then PProJ(a,b,x,y) = 0F & (-1F)*PProJ(a,b,y,x) = (-1F)*0F by A1,Th48;
    then PProJ(a,b,x,y) = 0F & -(PProJ
(a,b,y,x)*(1F)) = (-1F)*0F by VECTSP_1:41;
    then PProJ(a,b,x,y) = 0F & -PProJ(a,b,y,x) = (-1F)*0F by VECTSP_1:def 19;
    hence thesis by VECTSP_1:39;
   end;
     now assume not x _|_ y;
    then x <> 0.S & y <> 0.S & a <> 0.S by A1,Lm6,Th11;
    then consider r such that
    A3: not r _|_ a & not r _|_ x & not r _|_ y by A1,Th22;
    A4: not a _|_ b & not a _|_ r & not x _|_ r & not y _|_ r by A1,A3,Th12;
    A5: PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A3,Def7;
       PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A3,Def7;
    then PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,y)*ProJ
(y,r,x)) by VECTSP_1:def 16;
    then PProJ(a,b,y,x) = ProJ(a,b,r)*((-(ProJ(r,a,x)))*ProJ
(x,r,y)) by A4,Th44;
    then PProJ(a,b,y,x) = ((-(ProJ(r,a,x)))*ProJ(a,b,r))*ProJ
(x,r,y) by VECTSP_1:def 16;
    then PProJ(a,b,y,x) = (-ProJ(r,a,x)*ProJ(a,b,r))*ProJ
(x,r,y) by VECTSP_1:41;
    then (-1F)*PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ
(x,r,y)) by VECTSP_1:41;
    then -(PProJ(a,b,y,x)*(1F)) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ
(x,r,y)) by VECTSP_1:41;
    then -PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ
(x,r,y)) by VECTSP_1:def 19;
    then -PProJ(a,b,y,x) = (ProJ(a,b,r)*ProJ(r,a,x)*ProJ
(x,r,y))*(1F) by VECTSP_1:42;
    hence thesis by A5,VECTSP_1:def 19;
  end;
 hence thesis by A2;
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 A4: x _|_ y;
     then y _|_ x by Th12;
     then l*y _|_ x by Def2;
     then x _|_ y & y _|_ x & l*y _|_ x & x _|_ l*y by A4,Th12;
     then l*PProJ(a,b,x,y) = l*0F & PProJ(a,b,x,l*y) = 0F by A1,A2,Th48;
     hence thesis by VECTSP_1:39;
    end;
      now assume not x _|_ y;
    then a <> 0.S & x <> 0.S by A2,Lm6,Th11;
    then consider p such that A5: not p _|_ a & not p _|_ x by Th21;
    A6: PProJ(a,b,x,l*y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ
(x,p,l*y) by A1,A2,A5,Def7;
    A7: PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A2,A5,Def7;
      PProJ(a,b,x,l*y) = (l*ProJ(x,p,y))*(ProJ(a,b,p)*ProJ(p,a,x)) by A5,A6,
Th28
;
    hence thesis by A7,VECTSP_1:def 16;
   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;
  set 0F = 0.F;
   A3: now assume x = 0.S;
    then PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F & PProJ
(a,b,x,z) = 0F by A1,A2,Th47;
    hence thesis by RLVECT_1:10;
    end;
      now assume x <> 0.S;
    then a <> 0.S & x <> 0.S by A2,Lm6;
    then consider p such that A4: not p _|_ a & not p _|_ x by Th21;
    A5: PProJ(a,b,x,y+z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ
(x,p,y+z) by A1,A2,A4,Def7;
    A6: PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A2,A4,Def7;
    A7: PProJ(a,b,x,z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,z) by A1,A2,A4,Def7;
      ProJ(x,p,y+z) = ProJ(x,p,y) + ProJ(x,p,z) by A4,Th29;
    hence thesis by A5,A6,A7,VECTSP_1:def 18;
    end;
  hence thesis by A3;
 end;

Back to top