:: Construction of a bilinear antisymmetric form in symplectic vector space :: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski :: :: Received November 23, 1989 :: Copyright (c) 1990-2021 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, ORDERS_2, STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_0, XXREAL_0, CARD_1, TARSKI, RLVECT_1, SUPINF_2, ARYTM_1, ARYTM_3, GROUP_1, MESFUNC1, SYMSP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, ORDERS_2, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, RELSET_1; constructors BINOP_1, DOMAIN_1, RLVECT_1, VECTSP_1, ORDERS_2, GROUP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1; requirements SUBSET, BOOLE; begin :: 1. SYMPLECTIC VECTOR SPACE STRUCTURE reserve F for Field; definition let F; struct (RelStr,ModuleStr over F) SymStr over F (# carrier -> set, addF -> BinOp of the carrier, ZeroF -> Element of the carrier, lmult -> Function of [: the carrier of F, the carrier:], the carrier, InternalRel -> Relation of the carrier #); end; registration let F; cluster non empty for SymStr over F; end; notation let F; let S be SymStr over F; let a,b be Element of S; synonym a _|_ b for a <= b; end; registration 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; registration let F; cluster Abelian add-associative right_zeroed right_complementable for 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 1 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 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; registration let F; cluster SymSp-like vector-distributive scalar-distributive scalar-associative scalar-unital strict for Abelian add-associative right_zeroed right_complementable non empty SymStr over F; end; definition let F; mode SymSp of F is SymSp-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 SymSp of F; reserve a,b,c,d,a9,b9,p,q,r,s,x,y,z for Element of S; reserve k,l for Element of F; theorem :: SYMSP_1:1 0.S _|_ a; theorem :: SYMSP_1:2 a _|_ b implies b _|_ a; theorem :: SYMSP_1:3 not a _|_ b & c+a _|_ b implies not c _|_ b; theorem :: SYMSP_1:4 not b _|_ a & c _|_ a implies not b+c _|_ a; theorem :: SYMSP_1:5 not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a; theorem :: SYMSP_1:6 a _|_ b implies -a _|_ b; theorem :: SYMSP_1:7 not a _|_ c implies not a+b _|_ c or not (1_F+1_F)*a+b _|_ c; theorem :: SYMSP_1:8 not a9 _|_ a & a9 _|_ b & not b9 _|_ b & b9 _|_ a implies not a9 +b9 _|_ a & not a9+b9 _|_ b; theorem :: SYMSP_1:9 a<>0.S & b<>0.S implies ex p st not p _|_ a & not p _|_ b; theorem :: SYMSP_1:10 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:11 a-b _|_ d & a-c _|_ d implies b-c _|_ d; theorem :: SYMSP_1:12 not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l; theorem :: SYMSP_1:13 1_F+1_F<>0.F implies a _|_ a; :: 5. ORTHOGONAL PROJECTION definition let F; let S,a,b,x; assume not b _|_ a; func ProJ(a,b,x) -> Element of F means :: SYMSP_1:def 2 for l being Element of F st x-l*b _|_ a holds it = l; end; theorem :: SYMSP_1:14 not b _|_ a implies x-ProJ(a,b,x)*b _|_ a; theorem :: SYMSP_1:15 not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x); theorem :: SYMSP_1:16 not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y); theorem :: SYMSP_1:17 not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x); theorem :: SYMSP_1:18 not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x); theorem :: SYMSP_1:19 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:20 not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b ,c); theorem :: SYMSP_1:21 not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_F; theorem :: SYMSP_1:22 not b _|_ a implies ProJ(a,b,b) = 1_F; theorem :: SYMSP_1:23 not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F ); theorem :: SYMSP_1:24 not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p); theorem :: SYMSP_1:25 not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"; theorem :: SYMSP_1:26 not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = ProJ(c,b,a); theorem :: SYMSP_1:27 not a _|_ b & not c _|_ b implies ProJ(c,b,a) = (-ProJ(b,a,c)")* ProJ(a,b,c); theorem :: SYMSP_1:28 1_F+1_F<>0.F & not a _|_ p & not a _|_ q & not b _|_ q implies ProJ(a,p,q)*ProJ(b,q,p) = ProJ(p,a,b)*ProJ(q,b,a); theorem :: SYMSP_1:29 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:30 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:31 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 ( not b _|_ a)& 1_F+1_F<>0.F; func PProJ(a,b,x,y) -> Element of F means :: SYMSP_1:def 3 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; end; theorem :: SYMSP_1:32 1_F+1_F<>0.F & not b _|_ a & x=0.S implies PProJ(a,b,x,y) = 0.F; theorem :: SYMSP_1:33 1_F+1_F<>0.F & not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x); theorem :: SYMSP_1:34 1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,y) = -PProJ(a,b,y,x); theorem :: SYMSP_1:35 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:36 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);