The abstract of 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

MML identifier: SYMSP_1

[ Mizar article, 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;


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

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

definition let F;
 cluster Abelian add-associative right_zeroed right_complementable
                   (non empty SymStr over F);
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
:: SYMSP_1:def 2
  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));
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 :: SYMSP_1:11
 0.S _|_ a;

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

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

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

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

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

canceled 2;

theorem :: SYMSP_1:19
 not a _|_ c implies not a+b _|_ c or not (1_ F+1_ F)*a+b _|_ c;

theorem :: SYMSP_1:20
 not a' _|_ a & a' _|_ b & not b' _|_ b & b' _|_ a implies not a'+b' _|_
a & not a'+b' _|_ b;

theorem :: SYMSP_1:21
 a<>0.S & b<>0.S implies ex p st not p _|_ a & not p _|_ b;

theorem :: SYMSP_1:22
 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;

theorem :: SYMSP_1:23
 a-b _|_ d & a-c _|_ d implies b-c _|_ d;

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

theorem :: SYMSP_1:25
 1_ F+1_ F<>0.F implies a _|_ a;

::
::                      5. ORTHOGONAL PROJECTION
::

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

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

canceled;

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

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

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

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

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

theorem :: SYMSP_1:32
 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 :: SYMSP_1:33
 not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c);

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

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

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

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

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

theorem :: SYMSP_1:39
 not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = ProJ(c,b,a);

theorem :: SYMSP_1:40
not a _|_ b & not c _|_ b implies ProJ(c,b,a) =
  (-ProJ(b,a,c)")*ProJ(a,b,c);

theorem :: SYMSP_1:41
 (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);

theorem :: SYMSP_1:42
 (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);

theorem :: SYMSP_1:43
 (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);

theorem :: SYMSP_1:44
 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 ANTISYMMETRIC FORM
::

definition let F,S,x,y,a,b;
 assume that  not b _|_ a and  1_ F+1_ F<>0.F;
 func PProJ(a,b,x,y) -> Element of F means
:: SYMSP_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 :: SYMSP_1:47
 (1_ F+1_ F<>0.F) & not b _|_ a & x=0.S implies PProJ(a,b,x,y) = 0.F;

theorem :: SYMSP_1:48
 (1_ F+1_ F<>0.F) & not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x);

theorem :: SYMSP_1:49
   (1_ F+1_ F<>0.F) & not b _|_ a implies PProJ(a,b,x,y) = -PProJ(a,b,y,x);

theorem :: SYMSP_1:50
   (1_ F+1_ F<>0.F) & not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y);

theorem :: SYMSP_1:51
   (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);