:: Construction of a bilinear symmetric form in orthogonal 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, CARD_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_1, ZFMISC_1, TARSKI, RELAT_1, STRUCT_0, SYMSP_1, RLVECT_1, ALGSTR_0, ARYTM_3, SUPINF_2, ARYTM_1, GROUP_1, FUNCOP_1, ORTSP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, DOMAIN_1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RELSET_1, SYMSP_1; constructors BINOP_1, DOMAIN_1, FUNCOP_1, SYMSP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, SYMSP_1; 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; attr IT is OrtSp-like means :: ORTSP_1:def 1 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; registration let F; cluster OrtSp-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 OrtSp of F is OrtSp-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 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; theorem :: ORTSP_1:1 0.S _|_ a; theorem :: ORTSP_1:2 a _|_ b implies b _|_ a; theorem :: ORTSP_1:3 not a _|_ b & c+a _|_ b implies not c _|_ b; theorem :: ORTSP_1:4 not b _|_ a & c _|_ a implies not b+c _|_ a; theorem :: ORTSP_1:5 not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a; theorem :: ORTSP_1:6 a _|_ b implies -a _|_ b; theorem :: ORTSP_1:7 a-b _|_ d & a-c _|_ d implies b-c _|_ d; theorem :: ORTSP_1:8 not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l; theorem :: ORTSP_1:9 a _|_ a & b _|_ b implies a+b _|_ a-b; theorem :: ORTSP_1:10 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; func ProJ(a,b,x) -> Element of F means :: ORTSP_1:def 2 for l being Element of F st x-l*b _|_ a holds it = l; end; theorem :: ORTSP_1:11 not b _|_ a implies x-ProJ(a,b,x)*b _|_ a; theorem :: ORTSP_1:12 not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x); theorem :: ORTSP_1:13 not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y); theorem :: ORTSP_1:14 not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x); theorem :: ORTSP_1:15 not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x); theorem :: ORTSP_1:16 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:17 not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c); theorem :: ORTSP_1:18 not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_F; theorem :: ORTSP_1:19 not b _|_ a implies ProJ(a,b,b) = 1_F; theorem :: ORTSP_1:20 not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F ); theorem :: ORTSP_1:21 not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p); theorem :: ORTSP_1:22 not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"; theorem :: ORTSP_1:23 not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = -ProJ(c,b,a); theorem :: ORTSP_1:24 not a _|_ b & not c _|_ b implies ProJ(c,b,a) = ProJ(b,a,c)"* ProJ(a,b,c); theorem :: ORTSP_1:25 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:26 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:27 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 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 :: ORTSP_1:28 not b _|_ a & x = 0.S implies PProJ(a,b,x,y) = 0.F; theorem :: ORTSP_1:29 not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x); theorem :: ORTSP_1:30 not b _|_ a implies PProJ(a,b,x,y) = PProJ(a,b,y,x); theorem :: ORTSP_1:31 not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y); theorem :: ORTSP_1:32 not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) + PProJ(a,b,x,z);