Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Construction of a bilinear antisymmetric form in symplectic vector space

by
Eugeniusz Kusak,
Wojciech Leonczuk, and
Michal Muzalewski

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;
(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
(non empty SymStr over F));
end;

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