The abstract of the Mizar article:

Construction of a bilinear symmetric form in orthogonal vector space

by

Eugeniusz Kusak,

Wojciech Leonczuk, and

Michal Muzalewski

Received November 23, 1989

MML identifier: ORTSP_1

[ Mizar article, MML identifier index ]

environ

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


begin

::
::                 1. ORTHOGONAL VECTOR SPACE STRUCTURE
::

 reserve F for Field;

::
::                    2. ORTHOGONAL VECTOR SPACE
::

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

 attr IT is OrtSp-like means
:: ORTSP_1:def 2
  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;

definition let F;
 cluster OrtSp-like VectSp-like strict
  (Abelian add-associative right_zeroed right_complementable
    (non empty SymStr over F));
end;

definition let F;
 mode OrtSp of F is OrtSp-like VectSp-like
    (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;

canceled 10;

theorem :: ORTSP_1:11
 0.S _|_ a;

theorem :: ORTSP_1:12
 a _|_ b implies b _|_ a;

theorem :: ORTSP_1:13
 not a _|_ b & c+a _|_ b implies not c _|_ b;

theorem :: ORTSP_1:14
 not b _|_ a & c _|_ a implies not b+c _|_ a;

theorem :: ORTSP_1:15
 not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a;

theorem :: ORTSP_1:16
 a _|_ b implies -a _|_ b;

canceled 2;

theorem :: ORTSP_1:19
 a-b _|_ d & a-c _|_ d implies b-c _|_ d;

theorem :: ORTSP_1:20
 not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l;

theorem :: ORTSP_1:21
 a _|_ a & b _|_ b implies a+b _|_ a-b;

theorem :: ORTSP_1:22
   (1_ F+1_ F <> 0.F & (ex a st a<>0.S)) implies (ex b st not b _|_ b);

::
::                     5. ORTHOGONAL PROJECTION
::

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

 func ProJ(a,b,x) -> Element of F means
:: ORTSP_1:def 6
  for l being Element of F st x-l*b _|_ a
         holds it = l;
end;

canceled;

theorem :: ORTSP_1:24
 not b _|_ a implies x-ProJ(a,b,x)*b _|_ a;

theorem :: ORTSP_1:25
 not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x);

theorem :: ORTSP_1:26
 not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y);

theorem :: ORTSP_1:27
   not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x);

theorem :: ORTSP_1:28
 not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x);

theorem :: ORTSP_1:29
   not b _|_ a & p _|_ a implies
                 ProJ(a,b+p,c) = ProJ(a,b,c) & ProJ(a,b,c+p) = ProJ(a,b,c);

theorem :: ORTSP_1:30
   not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c);

theorem :: ORTSP_1:31
 not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_ F;

theorem :: ORTSP_1:32
 not b _|_ a implies ProJ(a,b,b) = 1_ F;

theorem :: ORTSP_1:33
 not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F );

theorem :: ORTSP_1:34
 not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p);

theorem :: ORTSP_1:35
 not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)";

theorem :: ORTSP_1:36
 not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = -ProJ(c,b,a);

theorem :: ORTSP_1:37
not a _|_ b & not c _|_ b implies ProJ(c,b,a) = ProJ(b,a,c)"*ProJ(a,b,c);

theorem :: ORTSP_1:38
 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);

theorem :: ORTSP_1:39
 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);

theorem :: ORTSP_1:40
 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);

::
::                   6. BILINEAR SYMMETRIC FORM
::

definition let F,S,x,y,a,b;
 assume  not b _|_ a;
 func PProJ(a,b,x,y) -> Element of F means
:: ORTSP_1:def 7
  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;
end;

canceled 2;

theorem :: ORTSP_1:43
 not b _|_ a & x = 0.S implies PProJ(a,b,x,y) = 0.F;



theorem :: ORTSP_1:44
  not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x);

theorem :: ORTSP_1:45
   not b _|_ a implies PProJ(a,b,x,y) = PProJ(a,b,y,x);

theorem :: ORTSP_1:46
   not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y);

theorem :: ORTSP_1:47
   not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) + PProJ(a,b,x,z);