:: Hermitan Functionals. {C}anonical Construction of Scalar Product in :: Quotient Vector Space :: by Jaros{\l}aw Kotowicz :: :: Received November 12, 2002 :: Copyright (c) 2002-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 NUMBERS, CARD_1, ARYTM_3, RELAT_1, XCMPLX_0, ARYTM_1, SUBSET_1, COMPLEX1, SQUARE_1, XXREAL_0, COMPLFLD, HAHNBAN1, GROUP_1, SUPINF_2, MESFUNC1, XBOOLE_0, VECTSP_1, HAHNBAN, FUNCT_1, RLVECT_1, ALGSTR_0, MSSUBFAM, STRUCT_0, UNIALG_1, ZFMISC_1, VECTSP10, TARSKI, RLSUB_1, GROUP_6, BILINEAR, REAL_1, HERMITAN, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, SQUARE_1, COMPLEX1, VECTSP_4, COMSEQ_2, COMPLFLD, HAHNBAN1, VECTSP10, BILINEAR; constructors REAL_1, SQUARE_1, BINOP_2, BORSUK_1, BILINEAR, FUNCOP_1, SUPINF_1, BINOP_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, VECTSP_1, COMPLFLD, HAHNBAN1, VECTSP10, BILINEAR, ORDINAL1, VALUED_0, MEMBERED, ALGSTR_0, GRCAT_1; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; begin theorem :: HERMITAN:1 for a be Complex st a = a*' holds Im a = 0; theorem :: HERMITAN:2 for a be Complex st a <> 0c holds |.(Re a)/|.a.|+ (-Im a)/|.a.|*.| = 1 & Re (((Re a)/|.a.|+ (-Im a)/|.a.|*) * a) = |.a.| & Im (( (Re a)/|.a.|+ (-Im a)/|.a.|*) * a)= 0; theorem :: HERMITAN:3 for a be Complex ex b be Complex st |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a)= 0; theorem :: HERMITAN:4 for a be Element of COMPLEX holds a*a*' = |.a.|^2+0*; theorem :: HERMITAN:5 for a be Element of F_Complex st a = a*' holds Im a = 0; theorem :: HERMITAN:6 i_FC * i_FC*' = 1_F_Complex; theorem :: HERMITAN:7 for a be Element of F_Complex st a <> 0.F_Complex holds |.[**(Re a)/|.a.|, (-Im a)/|.a.|**].| = 1 & Re ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a) = |.a.| & Im ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a) = 0; theorem :: HERMITAN:8 for a be Element of F_Complex ex b be Element of F_Complex st |.b .| = 1 & Re (b * a) = |.a.| & Im (b * a)= 0; theorem :: HERMITAN:9 for a,b be Element of F_Complex holds Re (a - b) = Re a - Re b & Im (a - b) = Im a - Im b; theorem :: HERMITAN:10 for a,b be Element of F_Complex st Im a = 0 holds Re (a*b) = Re a * Re b & Im (a*b) = Re a * Im b; theorem :: HERMITAN:11 for a,b be Element of F_Complex st Im a = 0 & Im b = 0 holds Im (a*b) = 0; theorem :: HERMITAN:12 for a be Element of F_Complex st Im a = 0 holds a = a*'; theorem :: HERMITAN:13 for a be Element of F_Complex holds a*a*' = |.a.|^2; theorem :: HERMITAN:14 for a be Element of F_Complex st 0 <= Re a & Im a = 0 holds |.a .| = Re a; theorem :: HERMITAN:15 for a be Element of F_Complex holds Re a + Re (a*') = 2 * Re a; begin :: Antilinear Functionals in Complex Vector Spaces definition let V be non empty ModuleStr over F_Complex; let f be Functional of V; attr f is cmplxhomogeneous means :: HERMITAN:def 1 for v be Vector of V, a be Scalar of V holds f.(a*v) = (a*')*f.v; end; registration let V be non empty ModuleStr over F_Complex; cluster 0Functional(V) -> cmplxhomogeneous; end; registration let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex; cluster cmplxhomogeneous -> 0-preserving for Functional of V; end; registration let V be non empty ModuleStr over F_Complex; cluster additive cmplxhomogeneous 0-preserving for Functional of V; end; definition let V be non empty ModuleStr over F_Complex; mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V; end; registration let V be non empty ModuleStr over F_Complex; let f,g be cmplxhomogeneous Functional of V; cluster f+g -> cmplxhomogeneous; end; registration let V be non empty ModuleStr over F_Complex; let f be cmplxhomogeneous Functional of V; cluster -f -> cmplxhomogeneous; end; registration let V be non empty ModuleStr over F_Complex; let a be Scalar of V; let f be cmplxhomogeneous Functional of V; cluster a*f -> cmplxhomogeneous; end; registration let V be non empty ModuleStr over F_Complex; let f,g be cmplxhomogeneous Functional of V; cluster f-g -> cmplxhomogeneous; end; definition let V be non empty ModuleStr over F_Complex; let f be Functional of V; redefine func f*' -> Functional of V means :: HERMITAN:def 2 for v being Vector of V holds it.v = (f.v)*'; end; registration let A be non empty addMagma; let f be additive Function of A,F_Complex; cluster f*' -> additive for Function of A,F_Complex; end; registration let V be non empty ModuleStr over F_Complex; let f be homogeneous Functional of V; cluster f*' -> cmplxhomogeneous for Functional of V; end; registration let V be non empty ModuleStr over F_Complex; let f be cmplxhomogeneous Functional of V; cluster f*' -> homogeneous for Functional of V; end; registration let V be non trivial VectSp of F_Complex; let f be non constant Functional of V; cluster f*' -> non constant; end; registration let V be non trivial VectSp of F_Complex; cluster additive cmplxhomogeneous non constant non trivial for Functional of V; end; theorem :: HERMITAN:16 for V be non empty ModuleStr over F_Complex, f be Functional of V holds (f*')*' = f; theorem :: HERMITAN:17 for V be non empty ModuleStr over F_Complex holds (0Functional(V))*' = 0Functional(V); theorem :: HERMITAN:18 for V be non empty ModuleStr over F_Complex, f,g be Functional of V holds (f+g)*'=f*'+ g*'; theorem :: HERMITAN:19 for V be non empty ModuleStr over F_Complex, f be Functional of V holds (-f)*'=-(f*'); theorem :: HERMITAN:20 for V be non empty ModuleStr over F_Complex for f be Functional of V, a be Scalar of V holds (a*f)*' = a*' * (f*'); theorem :: HERMITAN:21 for V be non empty ModuleStr over F_Complex, f,g be Functional of V holds (f-g)*'=f*'- g*'; theorem :: HERMITAN:22 for V be non empty ModuleStr over F_Complex, f be Functional of V for v be Vector of V holds f.v = 0.F_Complex iff f*'.v = 0.F_Complex; theorem :: HERMITAN:23 for V be non empty ModuleStr over F_Complex, f be Functional of V holds ker f = ker f*'; theorem :: HERMITAN:24 for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex for f be antilinear-Functional of V holds ker f is linearly-closed; theorem :: HERMITAN:25 for V be VectSp of F_Complex, W be Subspace of V for f be antilinear-Functional of V st the carrier of W c= ker f*' holds QFunctional(f,W) is cmplxhomogeneous; definition let V be VectSp of F_Complex; let f be antilinear-Functional of V; func QcFunctional(f) -> antilinear-Functional of VectQuot(V,Ker(f*')) equals :: HERMITAN:def 3 QFunctional(f,Ker(f*')); end; theorem :: HERMITAN:26 for V be VectSp of F_Complex, f be antilinear-Functional of V for A be Vector of VectQuot(V,Ker (f*')), v be Vector of V st A = v+Ker (f*') holds (QcFunctional(f)).A = f.v; registration let V be non trivial VectSp of F_Complex; let f be non constant antilinear-Functional of V; cluster QcFunctional(f) -> non constant; end; registration let V be VectSp of F_Complex; let f be antilinear-Functional of V; cluster QcFunctional(f) -> non degenerated; end; begin ::Sesquilinear Forms in Complex Vector Spaces definition let V,W be non empty ModuleStr over F_Complex; let f be Form of V,W; attr f is cmplxhomogeneousFAF means :: HERMITAN:def 4 for v be Vector of V holds FunctionalFAF(f,v) is cmplxhomogeneous; end; theorem :: HERMITAN:27 for V,W be non empty ModuleStr over F_Complex for v be Vector of V,w be Vector of W, a be Element of F_Complex for f be Form of V,W st f is cmplxhomogeneousFAF holds f.(v,a*w) = (a*')*f.(v,w); definition let V be non empty ModuleStr over F_Complex; let f be Form of V,V; attr f is hermitan means :: HERMITAN:def 5 for v,u be Vector of V holds f.(v,u) = (f.(u ,v))*'; attr f is diagRvalued means :: HERMITAN:def 6 for v be Vector of V holds Im (f.(v,v)) = 0; attr f is diagReR+0valued means :: HERMITAN:def 7 for v be Vector of V holds 0 <= Re (f .(v,v)); end; registration let V,W be non empty ModuleStr over F_Complex; cluster NulForm(V,W) -> cmplxhomogeneousFAF; end; registration let V be non empty ModuleStr over F_Complex; cluster NulForm(V,V) -> hermitan; cluster NulForm(V,V) -> diagReR+0valued; end; registration let V be non empty ModuleStr over F_Complex; cluster hermitan -> diagRvalued for Form of V,V; end; registration let V be non empty ModuleStr over F_Complex; cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF for Form of V,V; end; registration let V,W be non empty ModuleStr over F_Complex; cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF for Form of V,W; end; definition let V,W be non empty ModuleStr over F_Complex; mode sesquilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF Form of V,W; end; registration let V be non empty ModuleStr over F_Complex; cluster hermitan additiveFAF -> additiveSAF for Form of V,V; end; registration let V be non empty ModuleStr over F_Complex; cluster hermitan additiveSAF -> additiveFAF for Form of V,V; end; registration let V be non empty ModuleStr over F_Complex; cluster hermitan homogeneousSAF -> cmplxhomogeneousFAF for Form of V,V; end; registration let V be non empty ModuleStr over F_Complex; cluster hermitan cmplxhomogeneousFAF -> homogeneousSAF for Form of V,V; end; definition let V be non empty ModuleStr over F_Complex; mode hermitan-Form of V is hermitan additiveSAF homogeneousSAF Form of V,V; end; registration let V,W be non empty ModuleStr over F_Complex; let f be Functional of V, g be cmplxhomogeneous Functional of W; cluster FormFunctional(f,g) -> cmplxhomogeneousFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be cmplxhomogeneousFAF Form of V,W; let v be Vector of V; cluster FunctionalFAF(f,v) -> cmplxhomogeneous; end; registration let V,W be non empty ModuleStr over F_Complex; let f,g be cmplxhomogeneousFAF Form of V,W; cluster f+g -> cmplxhomogeneousFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be cmplxhomogeneousFAF Form of V,W; let a be Scalar of V; cluster a*f -> cmplxhomogeneousFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be cmplxhomogeneousFAF Form of V,W; cluster -f -> cmplxhomogeneousFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f,g be cmplxhomogeneousFAF Form of V,W; cluster f-g -> cmplxhomogeneousFAF; end; registration let V,W be non trivial VectSp of F_Complex; cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF non constant non trivial for Form of V,W; end; definition let V,W be non empty ModuleStr over F_Complex; let f be Form of V,W; func f*' -> Form of V,W means :: HERMITAN:def 8 for v be Vector of V, w be Vector of W holds it.(v,w) = (f.(v,w))*'; end; registration let V,W be non empty ModuleStr over F_Complex; let f be additiveFAF Form of V,W; cluster f*' -> additiveFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be additiveSAF Form of V,W; cluster f*' -> additiveSAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be homogeneousFAF Form of V,W; cluster f*' -> cmplxhomogeneousFAF; end; registration let V,W be non empty ModuleStr over F_Complex; let f be cmplxhomogeneousFAF Form of V,W; cluster f*' -> homogeneousFAF; end; registration let V,W be non trivial VectSp of F_Complex; let f be non constant Form of V,W; cluster f*' -> non constant; end; theorem :: HERMITAN:28 for V be non empty ModuleStr over F_Complex, f be Functional of V, v be Vector of V holds (FormFunctional(f,f*')).(v,v) = |. f.v .|^2; registration let V be non empty ModuleStr over F_Complex; let f be Functional of V; cluster FormFunctional(f,f*') -> diagReR+0valued hermitan diagRvalued; end; registration let V be non trivial VectSp of F_Complex; cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF non constant non trivial for Form of V,V; end; theorem :: HERMITAN:29 for V,W be non empty ModuleStr over F_Complex, f be Form of V,W holds (f*')*' = f; theorem :: HERMITAN:30 for V,W be non empty ModuleStr over F_Complex holds (NulForm(V,W))*' = NulForm(V,W); theorem :: HERMITAN:31 for V,W be non empty ModuleStr over F_Complex, f,g be Form of V, W holds (f+g)*'=f*'+ g*'; theorem :: HERMITAN:32 for V,W be non empty ModuleStr over F_Complex, f be Form of V,W holds (-f)*'=-(f*'); theorem :: HERMITAN:33 for V,W be non empty ModuleStr over F_Complex for f be Form of V,W, a be Element of F_Complex holds (a*f)*' = a*' * (f*'); theorem :: HERMITAN:34 for V,W be non empty ModuleStr over F_Complex, f,g be Form of V,W holds (f-g)*'=f*'- g*'; theorem :: HERMITAN:35 for V,W be VectSp of F_Complex, v be Vector of V, w,t be Vector of W for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds f.(v,w-t) = f.( v,w) - f.(v,t); theorem :: HERMITAN:36 for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be Vector of W for f be sesquilinear-Form of V,W holds f.(v-u,w-t) = f.(v,w) - f.( v,t) -(f.(u,w) - f.(u,t)); theorem :: HERMITAN:37 for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex for v,u be Vector of V, w,t be Vector of W for a,b be Element of F_Complex for f be sesquilinear-Form of V,W holds f.(v+a*u,w+b*t) = f.(v,w) + b*' * f.(v,t) + (a*f.(u,w) + a*(b*' *f.(u,t)) ); theorem :: HERMITAN:38 for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be Vector of W for a,b be Element of F_Complex for f be sesquilinear-Form of V,W holds f.(v-a*u,w-b*t) = f.(v,w) - b*'*f.(v,t) - (a*f.(u,w) - a*(b*'*f.(u,t))) ; theorem :: HERMITAN:39 for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex for f be cmplxhomogeneousFAF Form of V,V for v be Vector of V holds f.(v,0.V) = 0.F_Complex; theorem :: HERMITAN:40 :: Polarization Formulae for V be VectSp of F_Complex, v,w be Vector of V, f be hermitan-Form of V holds f.(v,w) + f.(v,w) + f.(v,w) + f.(v,w) = f.(v+w,v+w) - f.(v-w,v-w) + i_FC *f.(v+i_FC*w,v+i_FC*w) -i_FC *f.(v-i_FC*w,v-i_FC*w); definition let V be non empty ModuleStr over F_Complex; let f be Form of V,V; let v be Vector of V; func signnorm(f,v) -> Real equals :: HERMITAN:def 9 Re (f.(v,v)); end; theorem :: HERMITAN:41 for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex for f be diagReR+0valued diagRvalued Form of V,V for v be Vector of V holds |. f.(v,v) .| = Re (f.(v,v)) & signnorm (f,v) = |. f.(v,v) .|; :: :: Lemmas for Schwarz inequality :: theorem :: HERMITAN:42 for V be VectSp of F_Complex, v,w be Vector of V for f be sesquilinear-Form of V,V, r be Real, a be Element of F_Complex st |.a.| =1 holds f.(v-[**r,0**]*a*w, v-[**r,0**]*a*w) = f.(v,v) - [**r,0**]*(a* f.(w,v) ) - [**r,0**]*(a*'*f.(v,w)) + [**r^2,0**]*f.(w,w); theorem :: HERMITAN:43 for V be VectSp of F_Complex, v,w be Vector of V for f be diagReR+0valued hermitan-Form of V, r be Real, a be Element of F_Complex st |.a.| =1 & Re (a * f.(w,v)) = |.f.(w,v).| holds Re( f.(v-[**r,0**]*a*w, v- [**r,0**]*a*w)) = signnorm(f,v) - 2*|.f.(w,v).|*r + signnorm(f,w) * r^2 & 0 <= signnorm(f,v) - 2*|.f.(w,v).|*r + signnorm(f,w) * r^2; theorem :: HERMITAN:44 for V be VectSp of F_Complex, v,w be Vector of V for f be diagReR+0valued hermitan-Form of V st signnorm(f,w)= 0 holds |.f.(w,v).| = 0; ::$N Cauchy-Schwarz inequality theorem :: HERMITAN:45 for V be VectSp of F_Complex, v,w be Vector of V for f be diagReR+0valued hermitan-Form of V holds |. f.(v,w) .|^2 <= signnorm(f,v) * signnorm(f,w); theorem :: HERMITAN:46 :: Schwarz inequality - second version for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of V for v,w be Vector of V holds |. f.(v,w) .|^2 <= |. f.(v,v).| * |. f.(w,w) .|; ::$N Minkowski inequality theorem :: HERMITAN:47 for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of V for v,w be Vector of V holds signnorm(f,v+w) <= (sqrt( signnorm(f,v)) + sqrt(signnorm(f,w)))^2; theorem :: HERMITAN:48 ::Minkowski inequality - second version for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of V for v,w be Vector of V holds |. f.(v+w,v+w) .| <= (sqrt(|. f.(v,v) .|) + sqrt (|. f.(w,w) .|))^2; theorem :: HERMITAN:49 :: Parallerogram equality for V be VectSp of F_Complex for f be hermitan-Form of V for v,w be Element of V holds signnorm(f,v+w) + signnorm(f,v-w) =2* signnorm(f,v)+ 2* signnorm(f,w); theorem :: HERMITAN:50 :: Parallerogram equality - second version (stronger assumption) for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of V for v,w be Element of V holds |. f.(v+w,v+w) .| + |. f.(v-w,v-w) .| = 2*|. f. (v,v) .| + 2*|. f.(w,w) .|; definition let V be non empty ModuleStr over F_Complex; let f be Form of V,V; func quasinorm(f) -> RFunctional of V means :: HERMITAN:def 10 for v be Element of V holds it.v = sqrt (signnorm(f,v)); end; registration let V be VectSp of F_Complex; let f be diagReR+0valued hermitan-Form of V; cluster quasinorm(f) -> subadditive homogeneous; end; begin :: Kernel of Hermitan Forms and Hermitan Forms in Quotinet Vector Spaces registration let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex; let f be cmplxhomogeneousFAF Form of V,V; cluster diagker f -> non empty; end; theorem :: HERMITAN:51 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed; theorem :: HERMITAN:52 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds diagker f = leftker f; theorem :: HERMITAN:53 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds diagker f = rightker f; theorem :: HERMITAN:54 for V be non empty ModuleStr over F_Complex, f be Form of V,V holds diagker f = diagker f*'; theorem :: HERMITAN:55 for V,W be non empty ModuleStr over F_Complex, f be Form of V,W holds leftker f = leftker f*' & rightker f = rightker f*'; theorem :: HERMITAN:56 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds LKer f = RKer (f*'); theorem :: HERMITAN:57 for V be VectSp of F_Complex, f be diagReR+0valued diagRvalued Form of V,V for v be Vector of V st Re (f.(v,v))= 0 holds f.(v,v)= 0.F_Complex; theorem :: HERMITAN:58 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v be Vector of V st Re (f.(v,v))= 0 & (f is non degenerated-on-left or f is non degenerated-on-right) holds v=0.V; definition let V be non empty ModuleStr over F_Complex, W be VectSp of F_Complex; let f be additiveFAF cmplxhomogeneousFAF Form of V,W; func RQ*Form(f) -> additiveFAF cmplxhomogeneousFAF Form of V,VectQuot(W,RKer (f*')) equals :: HERMITAN:def 11 (RQForm(f*'))*'; end; theorem :: HERMITAN:59 for V be non empty ModuleStr over F_Complex, W be VectSp of F_Complex for f be additiveFAF cmplxhomogeneousFAF Form of V,W for v be Vector of V, w be Vector of W holds (RQ*Form(f)).(v,w+RKer (f*')) = f.(v,w); registration let V,W be VectSp of F_Complex; let f be sesquilinear-Form of V,W; cluster LQForm(f) -> additiveFAF cmplxhomogeneousFAF; cluster RQ*Form(f) -> additiveSAF homogeneousSAF; end; definition let V,W be VectSp of F_Complex; let f be sesquilinear-Form of V,W; func Q*Form(f) -> sesquilinear-Form of VectQuot(V,LKer(f)),VectQuot(W,RKer(f *')) means :: HERMITAN:def 12 for A be Vector of VectQuot(V,LKer f), B be Vector of VectQuot(W, RKer(f*')) for v be Vector of V, w be Vector of W st A = v + LKer f & B = w + RKer (f*') holds it.(A,B)= f.(v,w); end; registration let V,W be non trivial VectSp of F_Complex; let f be non constant sesquilinear-Form of V,W; cluster Q*Form(f) -> non constant; end; registration let V be right_zeroed non empty ModuleStr over F_Complex, W be VectSp of F_Complex; let f be additiveFAF cmplxhomogeneousFAF Form of V,W; cluster RQ*Form(f) -> non degenerated-on-right; end; theorem :: HERMITAN:60 for V be non empty ModuleStr over F_Complex, W be VectSp of F_Complex for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f); theorem :: HERMITAN:61 for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds RKer f*' = RKer (LQForm f)*'; theorem :: HERMITAN:62 for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds LKer f = LKer (RQ*Form f); theorem :: HERMITAN:63 for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds Q*Form(f) = RQ*Form(LQForm(f)) & Q*Form(f) = LQForm(RQ*Form(f)); theorem :: HERMITAN:64 for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds leftker Q*Form(f) = leftker (RQ*Form(LQForm(f))) & rightker Q*Form(f) = rightker (RQ*Form(LQForm(f))) & leftker Q*Form(f) = leftker (LQForm(RQ*Form(f)) ) & rightker Q*Form(f) = rightker (LQForm(RQ*Form(f))); registration let V,W be VectSp of F_Complex; let f be sesquilinear-Form of V,W; cluster RQ*Form(LQForm(f)) -> non degenerated-on-left non degenerated-on-right; cluster LQForm(RQ*Form(f)) -> non degenerated-on-left non degenerated-on-right; end; registration let V,W be VectSp of F_Complex; let f be sesquilinear-Form of V,W; cluster Q*Form(f) -> non degenerated-on-left non degenerated-on-right; end; begin :: Scalar Product in Quotient Vector Space Generated by Nonnegative Hermitan Form definition let V be non empty ModuleStr over F_Complex; let f be Form of V,V; attr f is positivediagvalued means :: HERMITAN:def 13 for v be Vector of V st v <> 0.V holds 0 < Re (f.(v,v)); end; registration let V be right_zeroed non empty ModuleStr over F_Complex; cluster positivediagvalued additiveSAF -> diagReR+0valued for Form of V,V; end; registration let V be right_zeroed non empty ModuleStr over F_Complex; cluster positivediagvalued additiveFAF -> diagReR+0valued for Form of V,V; end; definition let V be VectSp of F_Complex; let f be diagReR+0valued hermitan-Form of V; func ScalarForm(f) -> diagReR+0valued hermitan-Form of VectQuot(V,LKer(f)) equals :: HERMITAN:def 14 Q*Form(f); end; theorem :: HERMITAN:65 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V for A,B be Vector of VectQuot(V,LKer(f)), v,w be Vector of V st A = v + LKer f & B = w + LKer f holds (ScalarForm(f)).(A,B) = f.(v,w); theorem :: HERMITAN:66 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds leftker ScalarForm(f) = leftker Q*Form(f); theorem :: HERMITAN:67 for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V holds rightker ScalarForm(f) = rightker Q*Form(f); :: :: The From in Quotient Space Generated by Non negative Hermitan Form is the Scalar Product :: registration let V be VectSp of F_Complex; let f be diagReR+0valued hermitan-Form of V; cluster ScalarForm(f) -> non degenerated-on-left non degenerated-on-right positivediagvalued; end; registration let V be non trivial VectSp of F_Complex; let f be diagReR+0valued non constant hermitan-Form of V; cluster ScalarForm(f) -> non constant; end;