hermitan.miz

begin



 Lm1: 0 = ( 0 + ( 0 * ));

 theorem :: HERMITAN:1



 Th1: for a be Complex st a = (a *' ) holds ( Im a) = 0

 proof

 let z be Complex;

 assume z = (z *' );

 then ( Im z) = ( 0 + ( - ( Im z))) by COMPLEX1: 27;

 hence thesis;

 end;

 theorem :: HERMITAN:2



 Th2: 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

 proof

 let z be Complex;

 set r = |.z.|, a = ((( Re z) / r) + ((( - ( Im z)) / r) * ));

 assume z <> 0c ;

 then

 A1: 0 < r by COMPLEX1: 47;

 |.(z * z).| = ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 68;

 then 0 <= ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 46;

 then

 A2: (r ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 )) by SQUARE_1:def 2;



 A3: ( Re a) = (( Re z) / r) & ( Im a) = (( - ( Im z)) / r) by COMPLEX1: 12;



 then ((( Re a) ^2 ) + (( Im a) ^2 )) = (((( Re z) ^2 ) / (r ^2 )) + ((( - ( Im z)) / r) ^2 )) by XCMPLX_1: 76

 .= (((( Re z) ^2 ) / (r ^2 )) + ((( - ( Im z)) ^2 ) / (r ^2 ))) by XCMPLX_1: 76

 .= (((( Re z) ^2 ) + (( Im z) ^2 )) / (r ^2 )) by XCMPLX_1: 62

 .= (1 ^2 ) by A1, A2, XCMPLX_1: 60;

 hence |.a.| = 1 by SQUARE_1: 18;



 thus ( Re (a * z)) = (((( Re z) / r) * ( Re z)) - ((( - ( Im z)) / r) * ( Im z))) by A3, COMPLEX1: 9

 .= (((( Re z) * ( Re z)) / r) - ((( - ( Im z)) / r) * ( Im z))) by XCMPLX_1: 74

 .= (((( Re z) ^2 ) / r) - ((( - ( Im z)) * ( Im z)) / r)) by XCMPLX_1: 74

 .= (((( Re z) ^2 ) - ( - (( Im z) * ( Im z)))) / r) by XCMPLX_1: 120

 .= r by A1, A2, XCMPLX_1: 89;



 thus ( Im (a * z)) = (((( Re z) / r) * ( Im z)) + (( Re z) * (( - ( Im z)) / r))) by A3, COMPLEX1: 9

 .= (((( Re z) * ( Im z)) / r) + (( Re z) * (( - ( Im z)) / r))) by XCMPLX_1: 74

 .= (((( Re z) * ( Im z)) / r) + ((( - ( Im z)) * ( Re z)) / r)) by XCMPLX_1: 74

 .= (((( Re z) * ( Im z)) + ( - (( Im z) * ( Re z)))) / r) by XCMPLX_1: 62

 .= 0 ;

 end;

 theorem :: HERMITAN:3

 for a be Complex holds ex b be Complex st |.b.| = 1 & ( Re (b * a)) = |.a.| & ( Im (b * a)) = 0

 proof

 let z be Complex;

 set r = |.z.|;



 A1: r = 0 implies ex a be Element of COMPLEX st |.a.| = 1 & ( Re (a * z)) = r & ( Im (a * z)) = 0

 proof

 assume

 A2: r = 0 ;

 take 1r ;

 thus thesis by A2, COMPLEX1: 4, COMPLEX1: 45, COMPLEX1: 48;

 end;

 0 < r implies ex a be Complex st |.a.| = 1 & ( Re (a * z)) = r & ( Im (a * z)) = 0

 proof

 assume

 A3: 0 < r;

 take ((( Re z) / r) + ((( - ( Im z)) / r) * ));

 thus thesis by A3, Th2, COMPLEX1: 44;

 end;

 hence thesis by A1, COMPLEX1: 46;

 end;

 theorem :: HERMITAN:4



 Th4: for a be Element of COMPLEX holds (a * (a *' )) = (( |.a.| ^2 ) + ( 0 * ))

 proof

 let z be Element of COMPLEX ;

 0 <= (( Re z) ^2 ) & 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then ((( Re z) ^2 ) + (( Im z) ^2 )) = ( |.z.| ^2 ) by SQUARE_1:def 2;

 then

 A1: ( Re (z * (z *' ))) = ( |.z.| ^2 ) by COMPLEX1: 40;

 ( Im (z * (z *' ))) = 0 by COMPLEX1: 40;

 hence thesis by A1, COMPLEX1: 13;

 end;

 theorem :: HERMITAN:5

 for a be Element of F_Complex st a = (a *' ) holds ( Im a) = 0 by Th1;

 theorem :: HERMITAN:6

 ( i_FC * ( i_FC *' )) = ( 1_ F_Complex ) by COMPLEX1: 7, COMPLFLD: 8;

 theorem :: HERMITAN:7



 Th7: 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 by Th2, COMPLFLD: 7;

 theorem :: HERMITAN:8



 Th8: for a be Element of F_Complex holds ex b be Element of F_Complex st |.b.| = 1 & ( Re (b * a)) = |.a.| & ( Im (b * a)) = 0

 proof

 let z be Element of F_Complex ;

 set r = |.z.|;



 A1: r = 0 implies ex a be Element of F_Complex st |.a.| = 1 & ( Re (a * z)) = r & ( Im (a * z)) = 0

 proof

 assume

 A2: r = 0 ;

 take a = ( 1. F_Complex );

 thus |.a.| = 1 by COMPLFLD: 60;

 z = ( 0. F_Complex ) by A2, COMPLFLD: 58

 .= 0 by COMPLFLD:def 1;

 hence thesis by A2, Lm1, COMPLEX1: 12;

 end;

 0 < r implies ex a be Element of F_Complex st |.a.| = 1 & ( Re (a * z)) = r & ( Im (a * z)) = 0

 proof

 assume

 A3: 0 < r;

 take [**(( Re z) / r), (( - ( Im z)) / r)**];

 thus thesis by A3, Th7, COMPLFLD: 57;

 end;

 hence thesis by A1, COMPLEX1: 46;

 end;

 theorem :: HERMITAN:9



 Th9: for a,b be Element of F_Complex holds ( Re (a - b)) = (( Re a) - ( Re b)) & ( Im (a - b)) = (( Im a) - ( Im b))

 proof

 let a,b be Element of F_Complex ;

 reconsider x = a, y = b as Element of COMPLEX by COMPLFLD:def 1;



 thus ( Re (a - b)) = ( Re (x - y)) by COMPLFLD: 3

 .= (( Re a) - ( Re b)) by COMPLEX1: 19;



 thus ( Im (a - b)) = ( Im (x - y)) by COMPLFLD: 3

 .= (( Im a) - ( Im b)) by COMPLEX1: 19;

 end;

 theorem :: HERMITAN:10



 Th10: 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))

 proof

 let a,b be Element of F_Complex ;

 assume

 A1: ( Im a) = 0 ;



 hence ( Re (a * b)) = ((( Re a) * ( Re b)) - ( 0 * ( Im b))) by HAHNBAN1: 11

 .= (( Re a) * ( Re b));



 thus ( Im (a * b)) = ((( Re a) * ( Im b)) + (( Re b) * 0 )) by A1, HAHNBAN1: 11

 .= (( Re a) * ( Im b));

 end;

 theorem :: HERMITAN:11

 for a,b be Element of F_Complex st ( Im a) = 0 & ( Im b) = 0 holds ( Im (a * b)) = 0

 proof

 let a,b be Element of F_Complex ;

 assume ( Im a) = 0 & ( Im b) = 0 ;



 hence ( Im (a * b)) = (( Re b) * 0 ) by Th10

 .= 0 ;

 end;

 theorem :: HERMITAN:12



 Th12: for a be Element of F_Complex st ( Im a) = 0 holds a = (a *' )

 proof

 let x be Element of F_Complex ;

 reconsider d = x as Element of COMPLEX by COMPLFLD:def 1;

 assume ( Im x) = 0 ;



 hence x = (( Re d) + (( - ( Im d)) * )) by COMPLEX1: 13

 .= (x *' );

 end;

 theorem :: HERMITAN:13



 Th13: for a be Element of F_Complex holds (a * (a *' )) = ( |.a.| ^2 )

 proof

 let z be Element of F_Complex ;

 reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;



 thus (z * (z *' )) = (( |.a.| ^2 ) + ( 0 * )) by Th4

 .= ( |.z.| ^2 );

 end;

 theorem :: HERMITAN:14



 Th14: for a be Element of F_Complex st 0 <= ( Re a) & ( Im a) = 0 holds |.a.| = ( Re a)

 proof

 let z be Element of F_Complex ;

 assume that

 A1: 0 <= ( Re z) and

 A2: ( Im z) = 0 ;

 reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;

 |.a.| = |.( Re a).| by A2, COMPLEX1: 50;

 hence thesis by A1, ABSVALUE:def 1;

 end;

 theorem :: HERMITAN:15



 Th15: for a be Element of F_Complex holds (( Re a) + ( Re (a *' ))) = (2 * ( Re a))

 proof

 let z be Element of F_Complex ;



 thus (( Re z) + ( Re (z *' ))) = (( Re z) + ( Re z)) by COMPLEX1: 27

 .= (2 * ( Re z));

 end;

 begin

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Functional of V;

 :: HERMITAN:def1

 attr f is cmplxhomogeneous means

 : Def1: 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;

 coherence

 proof

 let x be Vector of V, r be Scalar of V;

 (( 0Functional V) . x) = ( 0. F_Complex ) by HAHNBAN1: 14;

 hence thesis by HAHNBAN1: 14;

 end;

 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;

 coherence

 proof

 let F be Functional of V;

 assume

 A1: F is cmplxhomogeneous;



 thus (F . ( 0. V)) = (F . (( 0. F_Complex ) * ( 0. V))) by VECTSP10: 1

 .= ((( 0. F_Complex ) *' ) * (F . ( 0. V))) by A1

 .= ( 0. F_Complex ) by COMPLFLD: 47;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster additive cmplxhomogeneous 0-preserving for Functional of V;

 existence

 proof

 take ( 0Functional V);

 thus thesis;

 end;

 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;

 coherence

 proof

 let v be Vector of V, a be Scalar of V;



 thus ((f + g) . (a * v)) = ((f . (a * v)) + (g . (a * v))) by HAHNBAN1:def 3

 .= (((a *' ) * (f . v)) + (g . (a * v))) by Def1

 .= (((a *' ) * (f . v)) + ((a *' ) * (g . v))) by Def1

 .= ((a *' ) * ((f . v) + (g . v)))

 .= ((a *' ) * ((f + g) . v)) by HAHNBAN1:def 3;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 let f be cmplxhomogeneous Functional of V;

 cluster ( - f) -> cmplxhomogeneous;

 coherence

 proof

 let v be Vector of V, a be Scalar of V;



 thus (( - f) . (a * v)) = ( - (f . (a * v))) by HAHNBAN1:def 4

 .= ( - ((a *' ) * (f . v))) by Def1

 .= ((a *' ) * ( - (f . v))) by VECTSP_1: 9

 .= ((a *' ) * (( - f) . v)) by HAHNBAN1:def 4;

 end;

 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;

 coherence

 proof

 let v be Vector of V, b be Scalar of V;



 thus ((a * f) . (b * v)) = (a * (f . (b * v))) by HAHNBAN1:def 6

 .= (a * ((b *' ) * (f . v))) by Def1

 .= ((b *' ) * (a * (f . v)))

 .= ((b *' ) * ((a * f) . v)) by HAHNBAN1:def 6;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 let f,g be cmplxhomogeneous Functional of V;

 cluster (f - g) -> cmplxhomogeneous;

 coherence ;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Functional of V;

 :: original: *'

 redefine

 :: HERMITAN:def2

 func f *' -> Functional of V means

 : Def2: for v be Vector of V holds (it . v) = ((f . v) *' );

 coherence

 proof



 A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;

 then

 reconsider f as Function of V, COMPLEX ;

 (f *' ) is Function of V, COMPLEX ;

 hence thesis by A1;

 end;

 compatibility

 proof

 let g be Functional of V;



 A2: ( dom g) = the carrier of V by FUNCT_2:def 1;

 hence g = (f *' ) implies for v be Vector of V holds (g . v) = ((f . v) *' ) by COMSEQ_2:def 1;

 assume for v be Vector of V holds (g . v) = ((f . v) *' );

 then

 A3: for c be set st c in ( dom g) holds (g . c) = ((f . c) *' );

 ( dom f) = the carrier of V by FUNCT_2:def 1;

 hence g = (f *' ) by A2, A3, COMSEQ_2:def 1;

 end;

 end

 registration

 let A be non empty addMagma;

 let f be additive Function of A, F_Complex ;

 cluster (f *' ) -> additive;

 coherence

 proof

 let g be Function of A, F_Complex such that

 A1: g = (f *' );



 A2: ( dom g) = the carrier of A by FUNCT_2:def 1;

 let x,y be Element of A;



 A3: (g . x) = ((f . x) *' ) & (g . y) = ((f . y) *' ) by A1, A2, COMSEQ_2:def 1;

 (f . (x + y)) = ((f . x) + (f . y)) by VECTSP_1:def 20;



 hence ((g . x) + (g . y)) = ((f . (x + y)) *' ) by A3, COMPLEX1: 32

 .= (g . (x + y)) by A1, A2, COMSEQ_2:def 1;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 let f be homogeneous Functional of V;

 cluster (f *' ) -> cmplxhomogeneous;

 coherence

 proof

 let g be Functional of V such that

 A1: g = (f *' );

 let v be Vector of V, r be Scalar of V;



 thus (g . (r * v)) = ((f . (r * v)) *' ) by A1, Def2

 .= ((r * (f . v)) *' ) by HAHNBAN1:def 8

 .= ((r *' ) * ((f . v) *' )) by COMPLFLD: 54

 .= ((r *' ) * (g . v)) by A1, Def2;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 let f be cmplxhomogeneous Functional of V;

 cluster (f *' ) -> homogeneous;

 coherence

 proof

 let g be Functional of V such that

 A1: g = (f *' );

 let v be Vector of V, r be Scalar of V;



 thus (g . (r * v)) = ((f . (r * v)) *' ) by A1, Def2

 .= (((r *' ) * (f . v)) *' ) by Def1

 .= (((r *' ) *' ) * ((f . v) *' )) by COMPLFLD: 54

 .= (r * (g . v)) by A1, Def2;

 end;

 end

 registration

 let V be non trivial VectSp of F_Complex ;

 let f be non constant Functional of V;

 cluster (f *' ) -> non constant;

 coherence

 proof

 consider x,y be object such that

 A1: x in ( dom f) and

 A2: y in ( dom f) and

 A3: (f . x) <> (f . y) by FUNCT_1:def 10;

 reconsider v = x, w = y as Vector of V by A1, A2;

 take x, y;

 now

 assume ((f . v) *' ) = ((f . w) *' );

 then (f . v) = (((f . w) *' ) *' );

 hence contradiction by A3;

 end;

 then ( dom (f *' )) = the carrier of V & ((f *' ) . x) <> ((f . w) *' ) by Def2, FUNCT_2:def 1;

 hence thesis by A1, Def2;

 end;

 end

 registration

 let V be non trivial VectSp of F_Complex ;

 cluster additive cmplxhomogeneous non constant non trivial for Functional of V;

 existence

 proof

 take ( the additive homogeneous non constant non trivial Functional of V *' );

 thus thesis;

 end;

 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)

 proof

 let V be non empty ModuleStr over F_Complex ;

 set f = ( 0Functional V);

 now

 let v be Vector of V;



 thus ((f *' ) . v) = ((f . v) *' ) by Def2

 .= ( 0. F_Complex ) by COMPLFLD: 47, HAHNBAN1: 14

 .= (f . v) by HAHNBAN1: 14;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HERMITAN:18



 Th18: for V be non empty ModuleStr over F_Complex , f,g be Functional of V holds ((f + g) *' ) = ((f *' ) + (g *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f,g be Functional of V;

 now

 let v be Vector of V;



 thus (((f + g) *' ) . v) = (((f + g) . v) *' ) by Def2

 .= (((f . v) + (g . v)) *' ) by HAHNBAN1:def 3

 .= (((f . v) *' ) + ((g . v) *' )) by COMPLFLD: 51

 .= (((f *' ) . v) + ((g . v) *' )) by Def2

 .= (((f *' ) . v) + ((g *' ) . v)) by Def2

 .= (((f *' ) + (g *' )) . v) by HAHNBAN1:def 3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HERMITAN:19



 Th19: for V be non empty ModuleStr over F_Complex , f be Functional of V holds (( - f) *' ) = ( - (f *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V;

 now

 let v be Vector of V;



 thus ((( - f) *' ) . v) = ((( - f) . v) *' ) by Def2

 .= (( - (f . v)) *' ) by HAHNBAN1:def 4

 .= ( - ((f . v) *' )) by COMPLFLD: 52

 .= ( - ((f *' ) . v)) by Def2

 .= (( - (f *' )) . v) by HAHNBAN1:def 4;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HERMITAN:20

 for V be non empty ModuleStr over F_Complex holds for f be Functional of V, a be Scalar of V holds ((a * f) *' ) = ((a *' ) * (f *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V, a be Scalar of V;

 now

 let v be Vector of V;



 thus (((a * f) *' ) . v) = (((a * f) . v) *' ) by Def2

 .= ((a * (f . v)) *' ) by HAHNBAN1:def 6

 .= ((a *' ) * ((f . v) *' )) by COMPLFLD: 54

 .= ((a *' ) * ((f *' ) . v)) by Def2

 .= (((a *' ) * (f *' )) . v) by HAHNBAN1:def 6;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HERMITAN:21

 for V be non empty ModuleStr over F_Complex , f,g be Functional of V holds ((f - g) *' ) = ((f *' ) - (g *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f,g be Functional of V;



 thus ((f - g) *' ) = ((f *' ) + (( - g) *' )) by Th18

 .= ((f *' ) - (g *' )) by Th19;

 end;

 theorem :: HERMITAN:22



 Th22: for V be non empty ModuleStr over F_Complex , f be Functional of V holds for v be Vector of V holds (f . v) = ( 0. F_Complex ) iff ((f *' ) . v) = ( 0. F_Complex )

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V;

 let v be Vector of V;

 thus (f . v) = ( 0. F_Complex ) implies ((f *' ) . v) = ( 0. F_Complex ) by Def2, COMPLFLD: 47;

 assume ((f *' ) . v) = ( 0. F_Complex );

 then (((f . v) *' ) *' ) = ( 0. F_Complex ) by Def2, COMPLFLD: 47;

 hence thesis;

 end;

 theorem :: HERMITAN:23



 Th23: for V be non empty ModuleStr over F_Complex , f be Functional of V holds ( ker f) = ( ker (f *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V;

 thus ( ker f) c= ( ker (f *' ))

 proof

 let x be object;

 assume x in ( ker f);

 then

 consider v be Vector of V such that

 A1: x = v and

 A2: (f . v) = ( 0. F_Complex );

 ((f *' ) . v) = ( 0. F_Complex ) by A2, Th22;

 hence thesis by A1;

 end;

 let x be object;

 assume x in ( ker (f *' ));

 then

 consider v be Vector of V such that

 A3: x = v and

 A4: ((f *' ) . v) = ( 0. F_Complex );

 (f . v) = ( 0. F_Complex ) by A4, Th22;

 hence thesis by A3;

 end;

 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 holds for f be antilinear-Functional of V holds ( ker f) is linearly-closed

 proof

 let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex , f be antilinear-Functional of V;

 ( ker f) = ( ker (f *' )) by Th23;

 hence thesis by VECTSP10: 33;

 end;

 theorem :: HERMITAN:25



 Th25: for V be VectSp of F_Complex , W be Subspace of V holds for f be antilinear-Functional of V st the carrier of W c= ( ker (f *' )) holds ( QFunctional (f,W)) is cmplxhomogeneous

 proof

 let V be VectSp of F_Complex , W be Subspace of V, f be antilinear-Functional of V;

 assume

 A1: the carrier of W c= ( ker (f *' ));

 set vq = ( VectQuot (V,W));

 set qf = ( QFunctional (f,W));



 A2: ( ker (f *' )) = ( ker f) by Th23;

 now

 set C = ( CosetSet (V,W));

 let A be Vector of vq;

 let r be Scalar of vq;



 A3: C = the carrier of vq by VECTSP10:def 6;

 then A in C;

 then

 consider aa be Coset of W such that

 A4: A = aa;

 consider a be Vector of V such that

 A5: aa = (a + W) by VECTSP_4:def 6;

 (r * A) = (( lmultCoset (V,W)) . (r,A)) by VECTSP10:def 6

 .= ((r * a) + W) by A3, A4, A5, VECTSP10:def 5;



 hence (qf . (r * A)) = (f . (r * a)) by A1, A2, VECTSP10:def 12

 .= ((r *' ) * (f . a)) by Def1

 .= ((r *' ) * (qf . A)) by A1, A2, A4, A5, VECTSP10:def 12;

 end;

 hence thesis;

 end;

 definition

 let V be VectSp of F_Complex ;

 let f be antilinear-Functional of V;

 :: HERMITAN:def3

 func QcFunctional (f) -> antilinear-Functional of ( VectQuot (V,( Ker (f *' )))) equals ( QFunctional (f,( Ker (f *' ))));

 correctness

 proof

 the carrier of ( Ker (f *' )) = ( ker (f *' )) by VECTSP10:def 11;

 hence thesis by Th25;

 end;

 end

 theorem :: HERMITAN:26



 Th26: for V be VectSp of F_Complex , f be antilinear-Functional of V holds 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)

 proof

 let V be VectSp of F_Complex , f be antilinear-Functional of V;

 let A be Vector of ( VectQuot (V,( Ker (f *' )))), v be Vector of V;

 assume

 A1: A = (v + ( Ker (f *' )));

 the carrier of ( Ker (f *' )) = ( ker (f *' )) by VECTSP10:def 11

 .= ( ker f) by Th23;

 hence thesis by A1, VECTSP10:def 12;

 end;

 registration

 let V be non trivial VectSp of F_Complex ;

 let f be non constant antilinear-Functional of V;

 cluster ( QcFunctional f) -> non constant;

 coherence

 proof

 set W = ( Ker (f *' )), qf = ( QcFunctional f), qv = ( VectQuot (V,W));

 consider v be Vector of V such that v <> ( 0. V) and

 A1: (f . v) <> ( 0. F_Complex ) by VECTSP10: 28;

 reconsider cv = (v + W) as Vector of qv by VECTSP10: 23;

 assume qf is constant;

 then qf = ( 0Functional qv);



 then ( 0. F_Complex ) = (qf . cv) by HAHNBAN1: 14

 .= (f . v) by Th26;

 hence contradiction by A1;

 end;

 end

 registration

 let V be VectSp of F_Complex ;

 let f be antilinear-Functional of V;

 cluster ( QcFunctional f) -> non degenerated;

 coherence

 proof

 set qf = ( QcFunctional f), W = ( Ker (f *' )), qV = ( VectQuot (V,W)), K = F_Complex ;



 A1: the carrier of W = ( ker (f *' )) by VECTSP10:def 11

 .= ( ker f) by Th23;



 A2: the carrier of qV = ( CosetSet (V,W)) by VECTSP10:def 6;

 thus ( ker qf) c= {( 0. qV)}

 proof

 let x be object;

 assume x in ( ker qf);

 then

 consider w be Vector of qV such that

 A3: x = w and

 A4: (qf . w) = ( 0. K);

 w in ( CosetSet (V,W)) by A2;

 then

 consider A be Coset of W such that

 A5: w = A;

 consider v be Vector of V such that

 A6: A = (v + W) by VECTSP_4:def 6;

 (f . v) = ( 0. K) by A1, A4, A5, A6, VECTSP10:def 12;

 then v in ( ker f);

 then v in W by A1, STRUCT_0:def 5;



 then w = ( zeroCoset (V,W)) by A5, A6, VECTSP_4: 49

 .= ( 0. qV) by VECTSP10: 21;

 hence thesis by A3, TARSKI:def 1;

 end;

 thus {( 0. qV)} c= ( ker qf)

 proof

 let x be object;

 assume x in {( 0. qV)};

 then

 A7: x = ( 0. qV) by TARSKI:def 1;

 (qf . ( 0. qV)) = ( 0. K) by HAHNBAN1:def 9;

 hence thesis by A7;

 end;

 end;

 end

 begin

 definition

 let V,W be non empty ModuleStr over F_Complex ;

 let f be Form of V, W;

 :: HERMITAN:def4

 attr f is cmplxhomogeneousFAF means

 : Def4: for v be Vector of V holds ( FunctionalFAF (f,v)) is cmplxhomogeneous;

 end

 theorem :: HERMITAN:27



 Th27: for V,W be non empty ModuleStr over F_Complex holds for v be Vector of V, w be Vector of W, a be Element of F_Complex holds for f be Form of V, W st f is cmplxhomogeneousFAF holds (f . (v,(a * w))) = ((a *' ) * (f . (v,w)))

 proof

 let V,W be non empty ModuleStr over F_Complex , v1 be Vector of V, w be Vector of W, r be Element of F_Complex , f be Form of V, W;

 set F = ( FunctionalFAF (f,v1));

 assume f is cmplxhomogeneousFAF;

 then

 A1: F is cmplxhomogeneous;



 thus (f . (v1,(r * w))) = (F . (r * w)) by BILINEAR: 8

 .= ((r *' ) * (F . w)) by A1

 .= ((r *' ) * (f . (v1,w))) by BILINEAR: 8;

 end;

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Form of V, V;

 :: HERMITAN:def5

 attr f is hermitan means

 : Def5: for v,u be Vector of V holds (f . (v,u)) = ((f . (u,v)) *' );

 :: HERMITAN:def6

 attr f is diagRvalued means

 : Def6: for v be Vector of V holds ( Im (f . (v,v))) = 0 ;

 :: HERMITAN:def7

 attr f is diagReR+0valued means

 : Def7: for v be Vector of V holds 0 <= ( Re (f . (v,v)));

 end

 Lm2:

 now

 let V be non empty ModuleStr over F_Complex , f be Functional of V;

 set 0F = ( 0Functional V);

 let v1,w be Vector of V;



 thus (( FormFunctional (f,0F)) . (v1,w)) = ((f . v1) * (0F . w)) by BILINEAR:def 10

 .= ((f . v1) * ( 0. F_Complex )) by HAHNBAN1: 14

 .= ( 0. F_Complex );

 end;



 Lm3: for V be non empty ModuleStr over F_Complex holds for f be Functional of V holds ( FormFunctional (f,( 0Functional V))) is hermitan

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V, v1,w be Vector of V;

 set 0F = ( 0Functional V), F = ( FormFunctional (f,0F));



 thus (F . (v1,w)) = ( 0. F_Complex ) by Lm2

 .= ((F . (w,v1)) *' ) by Lm2, COMPLFLD: 47;

 end;

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 cluster ( NulForm (V,W)) -> cmplxhomogeneousFAF;

 coherence

 proof

 let v be Vector of V;

 ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W) by BILINEAR: 10;

 hence thesis;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster ( NulForm (V,V)) -> hermitan;

 coherence

 proof

 ( NulForm (V,V)) = ( FormFunctional (( 0Functional V),( 0Functional V))) by BILINEAR: 22;

 hence thesis by Lm3;

 end;

 cluster ( NulForm (V,V)) -> diagReR+0valued;

 coherence

 proof

 let v be Vector of V;

 ( Re ( 0. F_Complex )) = ( In ( 0 , REAL )) by COMPLEX1:def 1, COMPLFLD: 7;

 hence thesis by FUNCOP_1: 70;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster hermitan -> diagRvalued for Form of V, V;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is hermitan;

 let v be Vector of V;

 (f . (v,v)) = ((f . (v,v)) *' ) by A1;

 hence thesis by Th1;

 end;

 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;

 existence

 proof

 take ( NulForm (V,V));

 thus thesis;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF for Form of V, W;

 existence

 proof

 take ( NulForm (V,W));

 thus thesis;

 end;

 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;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is hermitan additiveFAF;

 let w be Vector of V;

 set F = ( FunctionalSAF (f,w)), F1 = ( FunctionalFAF (f,w));

 now

 let x,y be Vector of V;



 thus (F . (x + y)) = (f . ((x + y),w)) by BILINEAR: 9

 .= ((f . (w,(x + y))) *' ) by A1

 .= ((F1 . (x + y)) *' ) by BILINEAR: 8

 .= (((F1 . x) + (F1 . y)) *' ) by A1, VECTSP_1:def 20

 .= (((f . (w,x)) + (F1 . y)) *' ) by BILINEAR: 8

 .= (((f . (w,x)) + (f . (w,y))) *' ) by BILINEAR: 8

 .= (((f . (w,x)) *' ) + ((f . (w,y)) *' )) by COMPLFLD: 51

 .= ((f . (x,w)) + ((f . (w,y)) *' )) by A1

 .= ((f . (x,w)) + (f . (y,w))) by A1

 .= ((F . x) + (f . (y,w))) by BILINEAR: 9

 .= ((F . x) + (F . y)) by BILINEAR: 9;

 end;

 hence thesis;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster hermitan additiveSAF -> additiveFAF for Form of V, V;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is hermitan additiveSAF;

 let v1 be Vector of V;

 set F = ( FunctionalFAF (f,v1)), F2 = ( FunctionalSAF (f,v1));

 now

 let x,y be Vector of V;



 thus (F . (x + y)) = (f . (v1,(x + y))) by BILINEAR: 8

 .= ((f . ((x + y),v1)) *' ) by A1

 .= ((F2 . (x + y)) *' ) by BILINEAR: 9

 .= (((F2 . x) + (F2 . y)) *' ) by A1, VECTSP_1:def 20

 .= (((f . (x,v1)) + (F2 . y)) *' ) by BILINEAR: 9

 .= (((f . (x,v1)) + (f . (y,v1))) *' ) by BILINEAR: 9

 .= (((f . (x,v1)) *' ) + ((f . (y,v1)) *' )) by COMPLFLD: 51

 .= ((f . (v1,x)) + ((f . (y,v1)) *' )) by A1

 .= ((f . (v1,x)) + (f . (v1,y))) by A1

 .= ((F . x) + (f . (v1,y))) by BILINEAR: 8

 .= ((F . x) + (F . y)) by BILINEAR: 8;

 end;

 hence thesis;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster hermitan homogeneousSAF -> cmplxhomogeneousFAF for Form of V, V;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is hermitan homogeneousSAF;

 let v1 be Vector of V;

 set F = ( FunctionalFAF (f,v1)), F2 = ( FunctionalSAF (f,v1));

 now

 let x be Vector of V, r be Scalar of V;



 thus (F . (r * x)) = (f . (v1,(r * x))) by BILINEAR: 8

 .= ((f . ((r * x),v1)) *' ) by A1

 .= ((F2 . (r * x)) *' ) by BILINEAR: 9

 .= ((r * (F2 . x)) *' ) by A1, HAHNBAN1:def 8

 .= ((r *' ) * ((F2 . x) *' )) by COMPLFLD: 54

 .= ((r *' ) * ((f . (x,v1)) *' )) by BILINEAR: 9

 .= ((r *' ) * (f . (v1,x))) by A1

 .= ((r *' ) * (F . x)) by BILINEAR: 8;

 end;

 hence thesis;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster hermitan cmplxhomogeneousFAF -> homogeneousSAF for Form of V, V;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is hermitan cmplxhomogeneousFAF;

 let w be Vector of V;

 set F = ( FunctionalSAF (f,w)), F2 = ( FunctionalFAF (f,w));



 A2: F2 is cmplxhomogeneous by A1;

 now

 let x be Vector of V, r be Scalar of V;



 thus (F . (r * x)) = (f . ((r * x),w)) by BILINEAR: 9

 .= ((f . (w,(r * x))) *' ) by A1

 .= ((F2 . (r * x)) *' ) by BILINEAR: 8

 .= (((r *' ) * (F2 . x)) *' ) by A2

 .= (((r *' ) *' ) * ((F2 . x) *' )) by COMPLFLD: 54

 .= (r * ((f . (w,x)) *' )) by BILINEAR: 8

 .= (r * (f . (x,w))) by A1

 .= (r * (F . x)) by BILINEAR: 9;

 end;

 hence thesis;

 end;

 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;

 coherence

 proof

 let v be Vector of V;

 set fg = ( FormFunctional (f,g)), F = ( FunctionalFAF (fg,v));

 let y be Vector of W, r be Scalar of W;



 A1: F = ((f . v) * g) by BILINEAR: 24;



 hence (F . (r * y)) = ((f . v) * (g . (r * y))) by HAHNBAN1:def 6

 .= ((f . v) * ((r *' ) * (g . y))) by Def1

 .= ((r *' ) * ((f . v) * (g . y)))

 .= ((r *' ) * (F . y)) by A1, HAHNBAN1:def 6;

 end;

 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;

 coherence

 proof

 let y be Vector of W, r be Scalar of W;

 set F = ( FunctionalFAF (f,v));



 thus (F . (r * y)) = (f . (v,(r * y))) by BILINEAR: 8

 .= ((r *' ) * (f . (v,y))) by Th27

 .= ((r *' ) * (F . y)) by BILINEAR: 8;

 end;

 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;

 correctness

 proof

 let w be Vector of V;

 set Ffg = ( FunctionalFAF ((f + g),w)), Ff = ( FunctionalFAF (f,w));

 set Fg = ( FunctionalFAF (g,w));

 let v be Vector of W, a be Scalar of V;



 thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by BILINEAR: 13

 .= ((Ff . (a * v)) + (Fg . (a * v))) by HAHNBAN1:def 3

 .= (((a *' ) * (Ff . v)) + (Fg . (a * v))) by Def1

 .= (((a *' ) * (Ff . v)) + ((a *' ) * (Fg . v))) by Def1

 .= ((a *' ) * ((Ff . v) + (Fg . v)))

 .= ((a *' ) * ((Ff + Fg) . v)) by HAHNBAN1:def 3

 .= ((a *' ) * (Ffg . v)) by BILINEAR: 13;

 end;

 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;

 coherence

 proof

 let w be Vector of V;

 set Ffg = ( FunctionalFAF ((a * f),w)), Ff = ( FunctionalFAF (f,w));

 let v be Vector of W, b be Scalar of V;



 thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by BILINEAR: 15

 .= (a * (Ff . (b * v))) by HAHNBAN1:def 6

 .= (a * ((b *' ) * (Ff . v))) by Def1

 .= ((b *' ) * (a * (Ff . v)))

 .= ((b *' ) * ((a * Ff) . v)) by HAHNBAN1:def 6

 .= ((b *' ) * (Ffg . v)) by BILINEAR: 15;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 let f be cmplxhomogeneousFAF Form of V, W;

 cluster ( - f) -> cmplxhomogeneousFAF;

 coherence ;

 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;

 coherence ;

 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;

 existence

 proof

 set g = the additive cmplxhomogeneous non constant non trivial Functional of W;

 set f = the additive homogeneous non constant non trivial Functional of V;

 take ( FormFunctional (f,g));

 thus thesis;

 end;

 end

 definition

 let V,W be non empty ModuleStr over F_Complex ;

 let f be Form of V, W;

 :: HERMITAN:def8

 func f *' -> Form of V, W means

 : Def8: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . (v,w)) *' );

 existence

 proof

 set K = F_Complex , X = the carrier of V, Y = the carrier of W, Z = the carrier of K;

 deffunc F( Element of X, Element of Y) = ((f . ($1,$2)) *' );

 consider ff be Function of [:X, Y:], Z such that

 A1: for x be Element of X holds for y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

 reconsider ff as Form of V, W;

 take ff;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let F,G be Form of V, W such that

 A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = ((f . (v,w)) *' ) and

 A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = ((f . (v,w)) *' );

 now

 let v be Vector of V, w be Vector of W;



 thus (F . (v,w)) = ((f . (v,w)) *' ) by A2

 .= (G . (v,w)) by A3;

 end;

 hence thesis;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 let f be additiveFAF Form of V, W;

 cluster (f *' ) -> additiveFAF;

 coherence

 proof

 let v be Vector of V;

 let w,t be Vector of W;

 set fg = ( FunctionalFAF ((f *' ),v));



 thus (fg . (w + t)) = ((f *' ) . (v,(w + t))) by BILINEAR: 8

 .= ((f . (v,(w + t))) *' ) by Def8

 .= (((f . (v,w)) + (f . (v,t))) *' ) by BILINEAR: 27

 .= (((f . (v,w)) *' ) + ((f . (v,t)) *' )) by COMPLFLD: 51

 .= (((f *' ) . (v,w)) + ((f . (v,t)) *' )) by Def8

 .= (((f *' ) . (v,w)) + ((f *' ) . (v,t))) by Def8

 .= ((fg . w) + ((f *' ) . (v,t))) by BILINEAR: 8

 .= ((fg . w) + (fg . t)) by BILINEAR: 8;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 let f be additiveSAF Form of V, W;

 cluster (f *' ) -> additiveSAF;

 coherence

 proof

 let w be Vector of W;

 let v,t be Vector of V;

 set fg = ( FunctionalSAF ((f *' ),w));



 thus (fg . (v + t)) = ((f *' ) . ((v + t),w)) by BILINEAR: 9

 .= ((f . ((v + t),w)) *' ) by Def8

 .= (((f . (v,w)) + (f . (t,w))) *' ) by BILINEAR: 26

 .= (((f . (v,w)) *' ) + ((f . (t,w)) *' )) by COMPLFLD: 51

 .= (((f *' ) . (v,w)) + ((f . (t,w)) *' )) by Def8

 .= (((f *' ) . (v,w)) + ((f *' ) . (t,w))) by Def8

 .= ((fg . v) + ((f *' ) . (t,w))) by BILINEAR: 9

 .= ((fg . v) + (fg . t)) by BILINEAR: 9;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 let f be homogeneousFAF Form of V, W;

 cluster (f *' ) -> cmplxhomogeneousFAF;

 coherence

 proof

 let v be Vector of V;

 let w be Vector of W, r be Scalar of W;

 set fg = ( FunctionalFAF ((f *' ),v));



 thus (fg . (r * w)) = ((f *' ) . (v,(r * w))) by BILINEAR: 8

 .= ((f . (v,(r * w))) *' ) by Def8

 .= ((r * (f . (v,w))) *' ) by BILINEAR: 32

 .= ((r *' ) * ((f . (v,w)) *' )) by COMPLFLD: 54

 .= ((r *' ) * ((f *' ) . (v,w))) by Def8

 .= ((r *' ) * (fg . w)) by BILINEAR: 8;

 end;

 end

 registration

 let V,W be non empty ModuleStr over F_Complex ;

 let f be cmplxhomogeneousFAF Form of V, W;

 cluster (f *' ) -> homogeneousFAF;

 coherence

 proof

 let v be Vector of V;

 let w be Vector of W, r be Scalar of W;

 set fg = ( FunctionalFAF ((f *' ),v));



 thus (fg . (r * w)) = ((f *' ) . (v,(r * w))) by BILINEAR: 8

 .= ((f . (v,(r * w))) *' ) by Def8

 .= (((r *' ) * (f . (v,w))) *' ) by Th27

 .= (((r *' ) *' ) * ((f . (v,w)) *' )) by COMPLFLD: 54

 .= (r * ((f *' ) . (v,w))) by Def8

 .= (r * (fg . w)) by BILINEAR: 8;

 end;

 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;

 coherence

 proof



 A1: ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

 consider x,y be object such that

 A2: x in ( dom f) and

 A3: y in ( dom f) and

 A4: (f . x) <> (f . y) by FUNCT_1:def 10;

 consider vy be Vector of V, wy be Vector of W such that

 A5: y = [vy, wy] by A3, DOMAIN_1: 1;

 take x, y;

 consider vx be Vector of V, wx be Vector of W such that

 A6: x = [vx, wx] by A2, DOMAIN_1: 1;

 now

 assume ((f *' ) . (vx,wx)) = ((f *' ) . (vy,wy));

 then (((f . (vx,wx)) *' ) *' ) = (((f *' ) . (vy,wy)) *' ) by Def8;

 then (f . (vx,wx)) = (((f . (vy,wy)) *' ) *' ) by Def8;

 hence contradiction by A4, A6, A5;

 end;

 hence thesis by A2, A3, A1, A6, A5, FUNCT_2:def 1;

 end;

 end

 theorem :: HERMITAN:28



 Th28: 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 )

 proof

 let V be non empty ModuleStr over F_Complex , f be Functional of V, v be Vector of V;

 set g = ( FormFunctional (f,(f *' )));



 thus (g . (v,v)) = ((f . v) * ((f *' ) . v)) by BILINEAR:def 10

 .= ((f . v) * ((f . v) *' )) by Def2

 .= ( |.(f . v).| ^2 ) by Th13;

 end;

 registration

 let V be non empty ModuleStr over F_Complex ;

 let f be Functional of V;

 cluster ( FormFunctional (f,(f *' ))) -> diagReR+0valued hermitan diagRvalued;

 coherence

 proof

 set g = ( FormFunctional (f,(f *' )));

 thus g is diagReR+0valued

 proof

 let v be Vector of V;

 (g . (v,v)) = (( |.(f . v).| ^2 ) + ( 0 * )) & (g . (v,v)) = (( Re (g . (v,v))) + (( Im (g . (v,v))) * )) by Th28, COMPLEX1: 13;

 then ( Re (g . (v,v))) = ( |.(f . v).| ^2 ) by COMPLEX1: 77;

 hence thesis by XREAL_1: 63;

 end;

 thus g is hermitan

 proof

 let v,w be Vector of V;



 thus (g . (v,w)) = ((((f . v) * ((f *' ) . w)) *' ) *' ) by BILINEAR:def 10

 .= ((((f . v) * ((f . w) *' )) *' ) *' ) by Def2

 .= ((((f . v) *' ) * (((f . w) *' ) *' )) *' ) by COMPLFLD: 54

 .= (((f . w) * ((f *' ) . v)) *' ) by Def2

 .= ((g . (w,v)) *' ) by BILINEAR:def 10;

 end;

 let v be Vector of V;

 (g . (v,v)) = [**( |.(f . v).| ^2 ), 0 **] & (g . (v,v)) = (( Re (g . (v,v))) + (( Im (g . (v,v))) * )) by Th28, COMPLEX1: 13;

 hence thesis by COMPLEX1: 77;

 end;

 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;

 existence

 proof

 set f = the additive homogeneous non constant non trivial Functional of V;

 take ( FormFunctional (f,(f *' )));

 thus thesis;

 end;

 end

 theorem :: HERMITAN:29

 for V,W be non empty ModuleStr over F_Complex , f be Form of V, W holds ((f *' ) *' ) = f

 proof

 let V,W be non empty ModuleStr over F_Complex ;

 let f be Form of V, W;

 now

 let v be Vector of V, w be Vector of W;



 thus (((f *' ) *' ) . (v,w)) = (((f *' ) . (v,w)) *' ) by Def8

 .= (((f . (v,w)) *' ) *' ) by Def8

 .= (f . (v,w));

 end;

 hence thesis;

 end;

 theorem :: HERMITAN:30

 for V,W be non empty ModuleStr over F_Complex holds (( NulForm (V,W)) *' ) = ( NulForm (V,W))

 proof

 let V,W be non empty ModuleStr over F_Complex ;

 set f = ( NulForm (V,W));

 now

 let v be Vector of V, w be Vector of W;



 thus ((f *' ) . (v,w)) = ((f . (v,w)) *' ) by Def8

 .= ( 0. F_Complex ) by COMPLFLD: 47, FUNCOP_1: 70

 .= (f . (v,w)) by FUNCOP_1: 70;

 end;

 hence thesis;

 end;

 theorem :: HERMITAN:31



 Th31: for V,W be non empty ModuleStr over F_Complex , f,g be Form of V, W holds ((f + g) *' ) = ((f *' ) + (g *' ))

 proof

 let V,W be non empty ModuleStr over F_Complex , f,g be Form of V, W;

 now

 let v be Vector of V, w be Vector of W;



 thus (((f + g) *' ) . (v,w)) = (((f + g) . (v,w)) *' ) by Def8

 .= (((f . (v,w)) + (g . (v,w))) *' ) by BILINEAR:def 2

 .= (((f . (v,w)) *' ) + ((g . (v,w)) *' )) by COMPLFLD: 51

 .= (((f *' ) . (v,w)) + ((g . (v,w)) *' )) by Def8

 .= (((f *' ) . (v,w)) + ((g *' ) . (v,w))) by Def8

 .= (((f *' ) + (g *' )) . (v,w)) by BILINEAR:def 2;

 end;

 hence thesis;

 end;

 theorem :: HERMITAN:32



 Th32: for V,W be non empty ModuleStr over F_Complex , f be Form of V, W holds (( - f) *' ) = ( - (f *' ))

 proof

 let V,W be non empty ModuleStr over F_Complex , f be Form of V, W;

 now

 let v be Vector of V, w be Vector of W;



 thus ((( - f) *' ) . (v,w)) = ((( - f) . (v,w)) *' ) by Def8

 .= (( - (f . (v,w))) *' ) by BILINEAR:def 4

 .= ( - ((f . (v,w)) *' )) by COMPLFLD: 52

 .= ( - ((f *' ) . (v,w))) by Def8

 .= (( - (f *' )) . (v,w)) by BILINEAR:def 4;

 end;

 hence thesis;

 end;

 theorem :: HERMITAN:33

 for V,W be non empty ModuleStr over F_Complex holds for f be Form of V, W, a be Element of F_Complex holds ((a * f) *' ) = ((a *' ) * (f *' ))

 proof

 let V,W be non empty ModuleStr over F_Complex , f be Form of V, W, a be Element of F_Complex ;

 now

 let v be Vector of V, w be Vector of W;



 thus (((a * f) *' ) . (v,w)) = (((a * f) . (v,w)) *' ) by Def8

 .= ((a * (f . (v,w))) *' ) by BILINEAR:def 3

 .= ((a *' ) * ((f . (v,w)) *' )) by COMPLFLD: 54

 .= ((a *' ) * ((f *' ) . (v,w))) by Def8

 .= (((a *' ) * (f *' )) . (v,w)) by BILINEAR:def 3;

 end;

 hence thesis;

 end;

 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 *' ))

 proof

 let V,W be non empty ModuleStr over F_Complex , f,g be Form of V, W;



 thus ((f - g) *' ) = ((f *' ) + (( - g) *' )) by Th31

 .= ((f *' ) - (g *' )) by Th32;

 end;

 theorem :: HERMITAN:35



 Th35: for V,W be VectSp of F_Complex , v be Vector of V, w,t be Vector of W holds for f be additiveFAF cmplxhomogeneousFAF Form of V, W holds (f . (v,(w - t))) = ((f . (v,w)) - (f . (v,t)))

 proof

 set K = F_Complex ;

 let V,W be VectSp of K, v1 be Vector of V, w,w2 be Vector of W, f be additiveFAF cmplxhomogeneousFAF Form of V, W;



 thus (f . (v1,(w - w2))) = ((f . (v1,w)) + (f . (v1,( - w2)))) by BILINEAR: 27

 .= ((f . (v1,w)) + (f . (v1,(( - ( 1_ K)) * w2)))) by VECTSP_1: 14

 .= ((f . (v1,w)) + ((( - ( 1. F_Complex )) *' ) * (f . (v1,w2)))) by Th27

 .= ((f . (v1,w)) + (( - ( 1_ K)) * (f . (v1,w2)))) by COMPLFLD: 49, COMPLFLD: 52

 .= ((f . (v1,w)) - (f . (v1,w2))) by VECTSP_6: 48;

 end;

 theorem :: HERMITAN:36



 Th36: for V,W be VectSp of F_Complex , v,u be Vector of V, w,t be Vector of W holds 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))))

 proof

 let V,W be VectSp of F_Complex , v1,w1 be Vector of V, w,w2 be Vector of W;

 let f be sesquilinear-Form of V, W;

 set v3 = (f . (v1,w)), v4 = (f . (v1,w2)), v5 = (f . (w1,w)), v6 = (f . (w1,w2));



 thus (f . ((v1 - w1),(w - w2))) = ((f . (v1,(w - w2))) - (f . (w1,(w - w2)))) by BILINEAR: 35

 .= ((v3 - v4) - (f . (w1,(w - w2)))) by Th35

 .= ((v3 - v4) - (v5 - v6)) by Th35;

 end;

 theorem :: HERMITAN:37



 Th37: for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex holds for v,u be Vector of V, w,t be Vector of W holds for a,b be Element of F_Complex holds 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))))))

 proof

 let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex ;

 let v1,w1 be Vector of V, w,w2 be Vector of W, r,s be Element of F_Complex , f be sesquilinear-Form of V, W;

 set v3 = (f . (v1,w)), v4 = (f . (v1,w2)), v5 = (f . (w1,w)), v6 = (f . (w1,w2));



 thus (f . ((v1 + (r * w1)),(w + (s * w2)))) = ((v3 + (f . (v1,(s * w2)))) + ((f . ((r * w1),w)) + (f . ((r * w1),(s * w2))))) by BILINEAR: 28

 .= ((v3 + ((s *' ) * v4)) + ((f . ((r * w1),w)) + (f . ((r * w1),(s * w2))))) by Th27

 .= ((v3 + ((s *' ) * v4)) + ((r * v5) + (f . ((r * w1),(s * w2))))) by BILINEAR: 31

 .= ((v3 + ((s *' ) * v4)) + ((r * v5) + (r * (f . (w1,(s * w2)))))) by BILINEAR: 31

 .= ((v3 + ((s *' ) * v4)) + ((r * v5) + (r * ((s *' ) * v6)))) by Th27;

 end;

 theorem :: HERMITAN:38



 Th38: for V,W be VectSp of F_Complex , v,u be Vector of V, w,t be Vector of W holds for a,b be Element of F_Complex holds 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))))))

 proof

 let V,W be VectSp of F_Complex , v1,w1 be Vector of V, w,w2 be Vector of W, r,s be Element of F_Complex , f be sesquilinear-Form of V, W;

 set v3 = (f . (v1,w)), v4 = (f . (v1,w2)), v5 = (f . (w1,w)), v6 = (f . (w1,w2));



 thus (f . ((v1 - (r * w1)),(w - (s * w2)))) = ((v3 - (f . (v1,(s * w2)))) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2))))) by Th36

 .= ((v3 - ((s *' ) * v4)) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2))))) by Th27

 .= ((v3 - ((s *' ) * v4)) - ((r * v5) - (f . ((r * w1),(s * w2))))) by BILINEAR: 31

 .= ((v3 - ((s *' ) * v4)) - ((r * v5) - (r * (f . (w1,(s * w2)))))) by BILINEAR: 31

 .= ((v3 - ((s *' ) * v4)) - ((r * v5) - (r * ((s *' ) * v6)))) by Th27;

 end;

 theorem :: HERMITAN:39



 Th39: for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex holds for f be cmplxhomogeneousFAF Form of V, V holds for v be Vector of V holds (f . (v,( 0. V))) = ( 0. F_Complex )

 proof

 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, v be Vector of V;

 set F = ( FunctionalFAF (f,v));



 thus (f . (v,( 0. V))) = (f . (v,(( 0. F_Complex ) * ( 0. V)))) by VECTSP10: 1

 .= (F . (( 0. F_Complex ) * ( 0. V))) by BILINEAR: 8

 .= ((( 0. F_Complex ) *' ) * (F . ( 0. V))) by Def1

 .= ( 0. F_Complex ) by COMPLFLD: 47;

 end;

 theorem :: HERMITAN:40

 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))))))

 proof

 let V be VectSp of F_Complex , v1,w be Vector of V, f be hermitan-Form of V;

 set v3 = (f . (v1,v1)), v4 = (f . (v1,w)), w2 = (f . (w,w)), w1 = (f . (w,v1));

 (f . ((v1 + w),(v1 + w))) = ((v3 + v4) + (w1 + w2)) & (f . ((v1 - w),(v1 - w))) = ((v3 - v4) - (w1 - w2)) by Th36, BILINEAR: 28;



 then

 A1: ((f . ((v1 + w),(v1 + w))) - (f . ((v1 - w),(v1 - w)))) = (((v3 + v4) - ((v3 - v4) - (w1 - w2))) + (w1 + w2))

 .= ((((v3 + v4) - (v3 - v4)) + (w1 - w2)) + (w1 + w2)) by RLVECT_1: 29

 .= ((((v3 - (v3 - v4)) + v4) + (w1 - w2)) + (w1 + w2))

 .= (((((v3 - v3) + v4) + v4) + (w1 - w2)) + (w1 + w2)) by RLVECT_1: 29

 .= ((((( 0. F_Complex ) + v4) + v4) + (w1 - w2)) + (w1 + w2)) by RLVECT_1: 15

 .= (((v4 + v4) + (w1 - w2)) + (w1 + w2)) by RLVECT_1:def 4

 .= ((v4 + v4) + (((w1 - w2) + w2) + w1))

 .= ((v4 + v4) + ((w1 - (w2 - w2)) + w1)) by RLVECT_1: 29

 .= ((v4 + v4) + ((w1 - ( 0. F_Complex )) + w1)) by RLVECT_1: 15

 .= ((v4 + v4) + (w1 + w1)) by RLVECT_1: 13;

 (f . ((v1 + ( i_FC * w)),(v1 + ( i_FC * w)))) = ((v3 + (( i_FC *' ) * v4)) + (( i_FC * w1) + ( i_FC * (( i_FC *' ) * w2)))) by Th37

 .= ((v3 + (( i_FC *' ) * v4)) + ( i_FC * (w1 + (( i_FC *' ) * w2))));



 then

 A2: ( i_FC * (f . ((v1 + ( i_FC * w)),(v1 + ( i_FC * w))))) = (( i_FC * (v3 + (( i_FC *' ) * v4))) + (( i_FC * i_FC ) * (w1 + (( i_FC *' ) * w2))))

 .= ((( i_FC * v3) + v4) - (w1 + (( i_FC *' ) * w2))) by COMPLEX1: 7, HAHNBAN1: 4, VECTSP_6: 48;

 (f . ((v1 - ( i_FC * w)),(v1 - ( i_FC * w)))) = ((f . (v1,(v1 - ( i_FC * w)))) - (f . (( i_FC * w),(v1 - ( i_FC * w))))) by BILINEAR: 35

 .= ((v3 - (f . (v1,( i_FC * w)))) - (f . (( i_FC * w),(v1 - ( i_FC * w))))) by Th35

 .= ((v3 - (( i_FC *' ) * v4)) - (f . (( i_FC * w),(v1 - ( i_FC * w))))) by Th27

 .= ((v3 - (( i_FC *' ) * v4)) - ( i_FC * (f . (w,(v1 - ( i_FC * w)))))) by BILINEAR: 31

 .= ((v3 - (( i_FC *' ) * v4)) - ( i_FC * (w1 - (f . (w,( i_FC * w)))))) by Th35

 .= ((v3 - (( i_FC *' ) * v4)) - ( i_FC * (w1 - (( i_FC *' ) * w2)))) by Th27;



 then ( i_FC * (f . ((v1 - ( i_FC * w)),(v1 - ( i_FC * w))))) = (( i_FC * (v3 - (( i_FC *' ) * v4))) - ( i_FC * ( i_FC * (w1 - (( i_FC *' ) * w2))))) by VECTSP_1: 11

 .= (( i_FC * (v3 - (( i_FC *' ) * v4))) - (( i_FC * i_FC ) * (w1 - (( i_FC *' ) * w2))))

 .= (( i_FC * (v3 - (( i_FC *' ) * v4))) - ( - (w1 - (( i_FC *' ) * w2)))) by HAHNBAN1: 4, VECTSP_6: 48

 .= (( i_FC * (v3 - (( i_FC *' ) * v4))) + (w1 - (( i_FC *' ) * w2))) by COMPLFLD: 11

 .= ((( i_FC * v3) - ( i_FC * (( i_FC *' ) * v4))) + (w1 - (( i_FC *' ) * w2))) by VECTSP_1: 11

 .= ((( i_FC * v3) - v4) + (w1 - (( i_FC *' ) * w2))) by COMPLEX1: 7;



 then (( i_FC * (f . ((v1 + ( i_FC * w)),(v1 + ( i_FC * w))))) - ( i_FC * (f . ((v1 - ( i_FC * w)),(v1 - ( i_FC * w)))))) = ((((( i_FC * v3) + v4) - (w1 + (( i_FC *' ) * w2))) - (( i_FC * v3) - v4)) - (w1 - (( i_FC *' ) * w2))) by A2, RLVECT_1: 27

 .= ((((( i_FC * v3) + v4) - (( i_FC * v3) - v4)) - (w1 + (( i_FC *' ) * w2))) - (w1 - (( i_FC *' ) * w2)))

 .= (((((v4 + ( i_FC * v3)) - ( i_FC * v3)) + v4) - (w1 + (( i_FC *' ) * w2))) - (w1 - (( i_FC *' ) * w2))) by RLVECT_1: 29

 .= ((((v4 + (( i_FC * v3) - ( i_FC * v3))) + v4) - (w1 + (( i_FC *' ) * w2))) - (w1 - (( i_FC *' ) * w2)))

 .= ((((v4 + ( 0. F_Complex )) + v4) - (w1 + (( i_FC *' ) * w2))) - (w1 - (( i_FC *' ) * w2))) by RLVECT_1: 15

 .= (((v4 + v4) - (w1 + (( i_FC *' ) * w2))) - (w1 - (( i_FC *' ) * w2))) by RLVECT_1:def 4

 .= ((v4 + v4) - ((w1 + (( i_FC *' ) * w2)) + (w1 - (( i_FC *' ) * w2)))) by RLVECT_1: 27

 .= ((v4 + v4) - ((w1 + w1) + ((( i_FC *' ) * w2) - (( i_FC *' ) * w2))))

 .= ((v4 + v4) - ((w1 + w1) + ( 0. F_Complex ))) by RLVECT_1: 15

 .= ((v4 + v4) - (w1 + w1)) by RLVECT_1:def 4;



 then ((((f . ((v1 + w),(v1 + w))) - (f . ((v1 - w),(v1 - w)))) + ( i_FC * (f . ((v1 + ( i_FC * w)),(v1 + ( i_FC * w)))))) - ( i_FC * (f . ((v1 - ( i_FC * w)),(v1 - ( i_FC * w)))))) = ((v4 + v4) + (((w1 + w1) + (v4 + v4)) - (w1 + w1))) by A1

 .= ((v4 + v4) + (v4 + v4)) by COMPLFLD: 12

 .= (((v4 + v4) + v4) + v4);

 hence thesis;

 end;

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Form of V, V;

 let v be Vector of V;

 :: HERMITAN:def9

 func signnorm (f,v) -> Real equals ( Re (f . (v,v)));

 coherence ;

 end

 theorem :: HERMITAN:41



 Th41: for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex holds for f be diagReR+0valued diagRvalued Form of V, V holds for v be Vector of V holds |.(f . (v,v)).| = ( Re (f . (v,v))) & ( signnorm (f,v)) = |.(f . (v,v)).|

 proof

 let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex , f be diagReR+0valued diagRvalued Form of V, V, v be Vector of V;

 set v1 = (f . (v,v));

 0 <= ( Re v1) & ( Im v1) = 0 by Def6, Def7;

 hence thesis by Th14;

 end;

 theorem :: HERMITAN:42



 Th42: for V be VectSp of F_Complex , v,w be Vector of V holds 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))))

 proof

 let V be VectSp of F_Complex , v1,w be Vector of V, f be sesquilinear-Form of V, V, r be Real, a be Element of F_Complex such that

 A1: |.a.| = 1;

 set r1 = ( [**r, 0 **] * a);

 set v3 = (f . (v1,v1)), v4 = (f . (v1,w)), w1 = (f . (w,v1)), w2 = (f . (w,w));



 A2: (( [**r, 0 **] * a) * (( [**r, 0 **] * (a *' )) * w2)) = (( [**(r ^2 ), 0 **] * (a * (a *' ))) * w2)

 .= ( [**((r ^2 ) * (1 ^2 )), 0 **] * w2) by A1, Th13;

 (f . ((v1 - (r1 * w)),(v1 - (r1 * w)))) = ((v3 - ((r1 *' ) * v4)) - ((r1 * w1) - (r1 * ((r1 *' ) * w2)))) by Th38

 .= ((v3 - ((( [**r, 0 **] *' ) * (a *' )) * v4)) - ((( [**r, 0 **] * a) * w1) - (( [**r, 0 **] * a) * ((( [**r, 0 **] * a) *' ) * w2)))) by COMPLFLD: 54

 .= ((v3 - (( [**r, 0 **] * (a *' )) * v4)) - ((( [**r, 0 **] * a) * w1) - (( [**r, 0 **] * a) * ((( [**r, 0 **] * a) *' ) * w2)))) by Th12, COMPLEX1: 12

 .= ((v3 - (( [**r, 0 **] * (a *' )) * v4)) - ((( [**r, 0 **] * a) * w1) - (( [**r, 0 **] * a) * ((( [**r, 0 **] *' ) * (a *' )) * w2)))) by COMPLFLD: 54

 .= ((v3 - ( [**r, 0 **] * ((a *' ) * v4))) - ((( [**r, 0 **] * a) * w1) - (( [**r, 0 **] * a) * (( [**r, 0 **] * (a *' )) * w2)))) by Th12, COMPLEX1: 12

 .= (((v3 - ( [**r, 0 **] * ((a *' ) * v4))) - ( [**r, 0 **] * (a * w1))) + (( [**r, 0 **] * a) * (( [**r, 0 **] * (a *' )) * w2))) by RLVECT_1: 29

 .= (((v3 - ( [**r, 0 **] * (a * w1))) - ( [**r, 0 **] * ((a *' ) * v4))) + (( [**r, 0 **] * a) * (( [**r, 0 **] * (a *' )) * w2)));

 hence thesis by A2;

 end;

 theorem :: HERMITAN:43



 Th43: for V be VectSp of F_Complex , v,w be Vector of V holds 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 )))

 proof

 let V be VectSp of F_Complex , v1,w be Vector of V, f be diagReR+0valued hermitan-Form of V, r be Real, a be Element of F_Complex such that

 A1: |.a.| = 1 and

 A2: ( Re (a * (f . (w,v1)))) = |.(f . (w,v1)).|;

 set v3 = (f . (v1,v1)), v4 = (f . (v1,w)), w1 = (f . (w,v1)), w2 = (f . (w,w)), A = ( signnorm (f,v1)), B = |.w1.|, C = ( signnorm (f,w));



 A3: ( Re [**r, 0 **]) = r & ( Im [**r, 0 **]) = 0 by COMPLEX1: 12;

 then

 A4: ( Re ( [**r, 0 **] * (a * w1))) = (r * B) by A2, Th10;

 ((a *' ) * v4) = ((((a *' ) * v4) *' ) *' )

 .= ((((a *' ) *' ) * (v4 *' )) *' ) by COMPLFLD: 54

 .= ((a * w1) *' ) by Def5;



 then

 A5: ( Re ( [**r, 0 **] * ((a *' ) * v4))) = (r * ( Re ((a * w1) *' ))) by A3, Th10

 .= (r * B) by A2, COMPLEX1: 27;

 ( Re [**(r ^2 ), 0 **]) = (r ^2 ) & ( Im [**(r ^2 ), 0 **]) = 0 by COMPLEX1: 12;

 then

 A6: ( Re ( [**(r ^2 ), 0 **] * w2)) = ((r ^2 ) * C) by Th10;

 (f . ((v1 - (( [**r, 0 **] * a) * w)),(v1 - (( [**r, 0 **] * a) * w)))) = (((v3 - ( [**r, 0 **] * (a * w1))) - ( [**r, 0 **] * ((a *' ) * v4))) + ( [**(r ^2 ), 0 **] * w2)) by A1, Th42;



 then ( Re (f . ((v1 - (( [**r, 0 **] * a) * w)),(v1 - (( [**r, 0 **] * a) * w))))) = (( Re ((v3 - ( [**r, 0 **] * (a * w1))) - ( [**r, 0 **] * ((a *' ) * v4)))) + (C * (r ^2 ))) by A6, HAHNBAN1: 10

 .= ((( Re (v3 - ( [**r, 0 **] * (a * w1)))) - (r * B)) + (C * (r ^2 ))) by A5, Th9

 .= (((A - (r * B)) - (r * B)) + (C * (r ^2 ))) by A4, Th9

 .= ((A - ((2 * B) * r)) + (C * (r ^2 )));

 hence thesis by Def7;

 end;

 theorem :: HERMITAN:44



 Th44: for V be VectSp of F_Complex , v,w be Vector of V holds for f be diagReR+0valued hermitan-Form of V st ( signnorm (f,w)) = 0 holds |.(f . (w,v)).| = 0

 proof

 let V be VectSp of F_Complex , v1,w be Vector of V, f be diagReR+0valued hermitan-Form of V;

 set w1 = (f . (w,v1)), A = ( signnorm (f,v1)), B = |.w1.|, C = ( signnorm (f,w));

 reconsider A as Real;

 assume that

 A1: C = 0 and

 A2: B <> 0 ;



 A3: ex a be Element of F_Complex st |.a.| = 1 & ( Re (a * w1)) = |.w1.| & ( Im (a * w1)) = 0 by Th8;

 A4:

 now

 A5:

 now

 assume

 A6: A > 0 ;

 ((A - ((2 * B) * (A / B))) + (C * ((A / B) ^2 ))) = (A - ((A * (2 * B)) / B)) by A1, XCMPLX_1: 74

 .= (A - (((A * 2) * B) / B))

 .= (A - (A + A)) by A2, XCMPLX_1: 89

 .= ( - A);

 hence contradiction by A3, A6, Th43;

 end;

 A7:

 now

 assume

 A8: A < 0 ;

 0 <= ((A - ((2 * B) * 0 )) + (C * ( 0 ^2 ))) by A3, Th43;

 hence contradiction by A8;

 end;

 assume A <> 0 ;

 hence contradiction by A7, A5;

 end;

 now

 assume

 A9: A = 0 ;

 A10:

 now

 assume

 A11: 0 < B;

 0 <= ((A - ((2 * B) * 1)) + (C * (1 ^2 ))) by A3, Th43;

 hence contradiction by A1, A9, A11;

 end;

 now

 assume

 A12: B < 0 ;

 0 <= ((A - ((2 * B) * ( - 1))) + (C * (( - 1) ^2 ))) by A3, Th43;

 hence contradiction by A1, A9, A12;

 end;

 hence contradiction by A2, A10;

 end;

 hence contradiction by A4;

 end;

 ::$Notion-Name

 theorem :: HERMITAN:45



 Th45: for V be VectSp of F_Complex , v,w be Vector of V holds for f be diagReR+0valued hermitan-Form of V holds ( |.(f . (v,w)).| ^2 ) <= (( signnorm (f,v)) * ( signnorm (f,w)))

 proof

 let V be VectSp of F_Complex , v1,w be Vector of V, f be diagReR+0valued hermitan-Form of V;

 set v4 = (f . (v1,w)), w1 = (f . (w,v1)), A = ( signnorm (f,v1)), B = |.w1.|, C = ( signnorm (f,w));

 reconsider A, B, C as Real;



 A1: C = ( 0 ^2 ) implies (B ^2 ) <= (A * C) by Th44;



 A2: ex a be Element of F_Complex st |.a.| = 1 & ( Re (a * w1)) = |.w1.| & ( Im (a * w1)) = 0 by Th8;



 A3: C > 0 implies (B ^2 ) <= (A * C)

 proof

 assume

 A4: C > 0 ;

 ((A - ((2 * B) * (B / C))) + (C * ((B / C) ^2 ))) = ((A - ((B * (2 * B)) / C)) + (C * ((B / C) ^2 ))) by XCMPLX_1: 74

 .= ((A - (((B ^2 ) * 2) / C)) + (C * ((B / C) ^2 )))

 .= ((A - (2 * ((B ^2 ) / C))) + (C * ((B / C) ^2 ))) by XCMPLX_1: 74

 .= ((A - (2 * ((B ^2 ) / C))) + (C * ((B ^2 ) / (C * C)))) by XCMPLX_1: 76

 .= ((A - (2 * ((B ^2 ) / C))) + ((C * (B ^2 )) / (C * C))) by XCMPLX_1: 74

 .= ((A - (2 * ((B ^2 ) / C))) + ((B ^2 ) / C)) by A4, XCMPLX_1: 91

 .= (A - ((B ^2 ) / C))

 .= (((A * C) - (B ^2 )) / C) by A4, XCMPLX_1: 127;

 then 0 <= ((A * C) - (B ^2 )) by A2, A4, Th43;

 then ( 0 + (B ^2 )) <= (((A * C) - (B ^2 )) + (B ^2 )) by XREAL_1: 6;

 hence thesis;

 end;

 B = |.(v4 *' ).| by Def5

 .= |.v4.| by COMPLEX1: 53;

 hence thesis by A1, A3, Def7;

 end;

 theorem :: HERMITAN:46



 Th46: for V be VectSp of F_Complex holds for f be diagReR+0valued hermitan-Form of V holds for v,w be Vector of V holds ( |.(f . (v,w)).| ^2 ) <= ( |.(f . (v,v)).| * |.(f . (w,w)).|)

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V, v1,w be Vector of V;

 set v3 = (f . (v1,v1)), s1 = ( signnorm (f,v1)), s2 = ( signnorm (f,w));

 ( |.(f . (v1,w)).| ^2 ) <= (s1 * s2) & s1 = |.v3.| by Th41, Th45;

 hence thesis by Th41;

 end;

 ::$Notion-Name

 theorem :: HERMITAN:47



 Th47: for V be VectSp of F_Complex holds for f be diagReR+0valued hermitan-Form of V holds for v,w be Vector of V holds ( signnorm (f,(v + w))) <= ((( sqrt ( signnorm (f,v))) + ( sqrt ( signnorm (f,w)))) ^2 )

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V, v,w be Vector of V;

 set v3 = (f . (v,v)), v4 = (f . (v,w)), w1 = (f . (w,v)), w2 = (f . (w,w)), sv = ( signnorm (f,v)), sw = ( signnorm (f,w)), svw = ( signnorm (f,(v + w)));



 A1: 0 <= sv by Def7;



 A2: svw = ( Re ((v3 + v4) + (w1 + w2))) by BILINEAR: 28

 .= (( Re (v3 + v4)) + ( Re (w1 + w2))) by HAHNBAN1: 10

 .= ((( Re v3) + ( Re v4)) + ( Re (w1 + w2))) by HAHNBAN1: 10

 .= ((( Re v3) + ( Re v4)) + (( Re w1) + ( Re w2))) by HAHNBAN1: 10

 .= ((sv + (( Re v4) + ( Re w1))) + sw)

 .= ((sv + (( Re v4) + ( Re (v4 *' )))) + sw) by Def5

 .= ((sv + (2 * ( Re v4))) + sw) by Th15

 .= ((sv + sw) + (2 * ( Re v4)));



 A3: 0 <= sw by Def7;

 0 <= |.v4.| by COMPLEX1: 46;

 then ( sqrt ( |.v4.| ^2 )) <= ( sqrt (sv * sw)) by Th45, SQUARE_1: 26;

 then |.v4.| <= ( sqrt (sv * sw)) by COMPLEX1: 46, SQUARE_1: 22;

 then ( Re v4) <= |.v4.| & |.v4.| <= (( sqrt sv) * ( sqrt sw)) by A1, A3, COMPLEX1: 54, SQUARE_1: 29;

 then ( Re v4) <= (( sqrt sv) * ( sqrt sw)) by XXREAL_0: 2;

 then (2 * ( Re v4)) <= (2 * (( sqrt sv) * ( sqrt sw))) by XREAL_1: 64;

 then svw <= ((sv + sw) + (2 * (( sqrt sv) * ( sqrt sw)))) by A2, XREAL_1: 6;

 then svw <= (((( sqrt sv) ^2 ) + sw) + (2 * (( sqrt sv) * ( sqrt sw)))) by A1, SQUARE_1:def 2;

 then svw <= (((( sqrt sv) ^2 ) + (( sqrt sw) ^2 )) + (2 * (( sqrt sv) * ( sqrt sw)))) by A3, SQUARE_1:def 2;

 hence thesis;

 end;

 theorem :: HERMITAN:48

 for V be VectSp of F_Complex holds for f be diagReR+0valued hermitan-Form of V holds for v,w be Vector of V holds |.(f . ((v + w),(v + w))).| <= ((( sqrt |.(f . (v,v)).|) + ( sqrt |.(f . (w,w)).|)) ^2 )

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V, v1,w be Vector of V;

 set v3 = (f . (v1,v1)), v4 = (f . ((v1 + w),(v1 + w))), s1 = ( signnorm (f,v1)), s2 = ( signnorm (f,w)), s12 = ( signnorm (f,(v1 + w)));



 A1: |.v4.| = s12 by Th41;

 s12 <= ((( sqrt s1) + ( sqrt s2)) ^2 ) & |.v3.| = s1 by Th41, Th47;

 hence thesis by A1, Th41;

 end;

 theorem :: HERMITAN:49



 Th49: for V be VectSp of F_Complex holds for f be hermitan-Form of V holds for v,w be Element of V holds (( signnorm (f,(v + w))) + ( signnorm (f,(v - w)))) = ((2 * ( signnorm (f,v))) + (2 * ( signnorm (f,w))))

 proof

 let V be VectSp of F_Complex , f be hermitan-Form of V, v1,w be Element of V;

 set v3 = (f . (v1,v1)), v4 = (f . (v1,w)), w1 = (f . (w,v1)), w2 = (f . (w,w)), vp = (f . ((v1 + w),(v1 + w))), vm = (f . ((v1 - w),(v1 - w))), s1 = ( signnorm (f,v1)), s2 = ( signnorm (f,w)), sp = ( signnorm (f,(v1 + w))), sm = ( signnorm (f,(v1 - w)));

 vp = ((v3 + v4) + (w1 + w2)) by BILINEAR: 28;



 then

 A1: (vp + vm) = (((v3 + v4) + (w1 + w2)) + ((v3 - v4) - (w1 - w2))) by Th36

 .= (((v3 + ((v4 + v3) - v4)) + (w1 + w2)) - (w1 - w2))

 .= (((v3 + v3) + (w1 + w2)) - (w1 - w2)) by COMPLFLD: 12

 .= ((v3 + v3) + ((w1 + w2) - (w1 - w2)))

 .= ((v3 + v3) + (((w1 + w2) - w1) + w2)) by RLVECT_1: 29

 .= ((v3 + v3) + (w2 + w2)) by COMPLFLD: 12;



 thus (sp + sm) = ( Re (vp + vm)) by HAHNBAN1: 10

 .= (( Re (v3 + v3)) + ( Re (w2 + w2))) by A1, HAHNBAN1: 10

 .= ((( Re v3) + ( Re v3)) + ( Re (w2 + w2))) by HAHNBAN1: 10

 .= ((2 * ( Re v3)) + (( Re w2) + ( Re w2))) by HAHNBAN1: 10

 .= ((2 * s1) + (2 * s2));

 end;

 theorem :: HERMITAN:50

 for V be VectSp of F_Complex holds for f be diagReR+0valued hermitan-Form of V holds 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)).|))

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V, v1,w be Element of V;

 set s1 = ( signnorm (f,v1)), s2 = ( signnorm (f,w)), sp = ( signnorm (f,(v1 + w))), sm = ( signnorm (f,(v1 - w)));



 A1: sm = |.(f . ((v1 - w),(v1 - w))).| & s1 = |.(f . (v1,v1)).| by Th41;

 (sp + sm) = ((2 * s1) + (2 * s2)) & sp = |.(f . ((v1 + w),(v1 + w))).| by Th41, Th49;

 hence thesis by A1, Th41;

 end;

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Form of V, V;

 :: HERMITAN:def10

 func quasinorm (f) -> RFunctional of V means

 : Def10: for v be Element of V holds (it . v) = ( sqrt ( signnorm (f,v)));

 existence

 proof

 set C = the carrier of V;

 defpred P[ Element of C, set] means $2 = ( sqrt ( signnorm (f,$1)));

 A1:

 now

 let x be Element of C;

 reconsider y = ( sqrt ( signnorm (f,x))) as Element of REAL by XREAL_0:def 1;

 take y;

 thus P[x, y];

 end;

 consider F be Function of the carrier of V, REAL such that

 A2: for v be Element of V holds P[v, (F . v)] from FUNCT_2:sch 3( A1);

 reconsider F as RFunctional of V;

 take F;

 thus thesis by A2;

 end;

 uniqueness

 proof

 let h,g be RFunctional of V such that

 A3: for v be Element of V holds (h . v) = ( sqrt ( signnorm (f,v))) and

 A4: for v be Element of V holds (g . v) = ( sqrt ( signnorm (f,v)));

 now

 let v be Element of V;



 thus (h . v) = ( sqrt ( signnorm (f,v))) by A3

 .= (g . v) by A4;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 registration

 let V be VectSp of F_Complex ;

 let f be diagReR+0valued hermitan-Form of V;

 cluster ( quasinorm f) -> subadditive homogeneous;

 coherence

 proof

 set q = ( quasinorm f);

 thus ( quasinorm f) is subadditive

 proof

 let v,w be Vector of V;

 set fvw = ( signnorm (f,(v + w))), fv = ( signnorm (f,v)), fw = ( signnorm (f,w));



 A1: (q . v) = ( sqrt fv) by Def10;

 0 <= ( Re (f . (v,v))) by Def7;

 then

 A2: 0 <= (q . v) by A1, SQUARE_1:def 2;



 A3: (q . w) = ( sqrt fw) by Def10;

 0 <= ( Re (f . (w,w))) by Def7;

 then

 A4: 0 <= (q . w) by A3, SQUARE_1:def 2;

 0 <= ( Re (f . ((v + w),(v + w)))) & (q . (v + w)) = ( sqrt fvw) by Def7, Def10;

 then (q . (v + w)) <= ( sqrt (((q . v) + (q . w)) ^2 )) by A1, A3, Th47, SQUARE_1: 26;

 hence (q . (v + w)) <= ((q . v) + (q . w)) by A2, A4, SQUARE_1: 22;

 end;

 let v be Vector of V, r be Scalar of V;



 A5: 0 <= ( |.r.| ^2 ) & 0 <= ( Re (f . (v,v))) by Def7, XREAL_1: 63;



 A6: (f . ((r * v),(r * v))) = (r * (f . (v,(r * v)))) by BILINEAR: 31

 .= (r * ((r *' ) * (f . (v,v)))) by Th27

 .= ((r * (r *' )) * (f . (v,v)))

 .= ( [**( |.r.| ^2 ), 0 **] * (f . (v,v))) by Th13

 .= ( [**( |.r.| ^2 ), 0 **] * [**( Re (f . (v,v))), ( Im (f . (v,v)))**]) by COMPLEX1: 13

 .= ( [**( |.r.| ^2 ), 0 **] * [**( Re (f . (v,v))), 0 **]) by Def6

 .= [**(( |.r.| ^2 ) * ( Re (f . (v,v)))), 0 **];



 thus (q . (r * v)) = ( sqrt ( signnorm (f,(r * v)))) by Def10

 .= ( sqrt (( |.r.| ^2 ) * ( Re (f . (v,v))))) by A6, COMPLEX1: 12

 .= (( sqrt ( |.r.| ^2 )) * ( sqrt ( Re (f . (v,v))))) by A5, SQUARE_1: 29

 .= ( |.r.| * ( sqrt ( signnorm (f,v)))) by COMPLEX1: 46, SQUARE_1: 22

 .= ( |.r.| * (q . v)) by Def10;

 end;

 end

 begin

 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;

 coherence

 proof

 set F = F_Complex ;

 (f . (( 0. V),( 0. V))) = ( 0. F) by Th39;

 then ( 0. V) in ( diagker f);

 hence thesis;

 end;

 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

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 set V1 = ( diagker f);

 thus for v,u be Element of V st v in V1 & u in V1 holds (v + u) in V1

 proof

 let v,u be Element of V;

 assume that

 A1: v in V1 and

 A2: u in V1;



 A3: ex b be Vector of V st b = u & (f . (b,b)) = ( 0. F_Complex ) by A2;

 then ( |.(f . (v,u)).| ^2 ) <= ( |.(f . (v,v)).| * 0 ) by Th46, COMPLFLD: 57;

 then

 A4: |.(f . (v,u)).| = 0 by XREAL_1: 63;



 then 0 = |.((f . (v,u)) *' ).| by COMPLEX1: 53

 .= |.(f . (u,v)).| by Def5;

 then

 A5: (f . (u,v)) = ( 0. F_Complex ) by COMPLFLD: 58;

 ex a be Vector of V st a = v & (f . (a,a)) = ( 0. F_Complex ) by A1;



 then

 A6: (f . ((v + u),(v + u))) = ((( 0. F_Complex ) + (f . (v,u))) + ((f . (u,v)) + ( 0. F_Complex ))) by A3, BILINEAR: 28

 .= ((f . (v,u)) + ((f . (u,v)) + ( 0. F_Complex ))) by RLVECT_1: 4

 .= ((f . (v,u)) + (f . (u,v))) by RLVECT_1: 4;

 (f . (v,u)) = ( 0. F_Complex ) by A4, COMPLFLD: 58;

 then (f . ((v + u),(v + u))) = ( 0. F_Complex ) by A6, A5, RLVECT_1: 4;

 hence thesis;

 end;

 let a be Element of F_Complex ;

 let v be Element of V;

 assume v in V1;

 then

 A7: ex w be Vector of V st w = v & (f . (w,w)) = ( 0. F_Complex );

 (f . ((a * v),(a * v))) = (a * (f . (v,(a * v)))) by BILINEAR: 31

 .= (a * ((a *' ) * ( 0. F_Complex ))) by A7, Th27

 .= ( 0. F_Complex );

 hence thesis;

 end;

 theorem :: HERMITAN:52



 Th52: for V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V holds ( diagker f) = ( leftker f)

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 thus ( diagker f) c= ( leftker f)

 proof

 let x be object;

 assume x in ( diagker f);

 then

 consider a be Vector of V such that

 A1: a = x and

 A2: (f . (a,a)) = ( 0. F_Complex );

 now

 let w be Vector of V;

 ( |.(f . (a,w)).| ^2 ) <= ( 0 * |.(f . (w,w)).|) by A2, Th46, COMPLFLD: 57;

 then |.(f . (a,w)).| = 0 by XREAL_1: 63;

 hence (f . (a,w)) = ( 0. F_Complex ) by COMPLFLD: 58;

 end;

 hence thesis by A1;

 end;

 let x be object;

 assume x in ( leftker f);

 then

 consider a be Vector of V such that

 A3: a = x and

 A4: for w be Vector of V holds (f . (a,w)) = ( 0. F_Complex );

 (f . (a,a)) = ( 0. F_Complex ) by A4;

 hence thesis by A3;

 end;

 theorem :: HERMITAN:53



 Th53: for V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V holds ( diagker f) = ( rightker f)

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 thus ( diagker f) c= ( rightker f)

 proof

 let x be object;

 assume x in ( diagker f);

 then

 consider a be Vector of V such that

 A1: a = x and

 A2: (f . (a,a)) = ( 0. F_Complex );

 now

 let w be Vector of V;

 ( |.(f . (w,a)).| ^2 ) <= ( |.(f . (w,w)).| * 0 ) by A2, Th46, COMPLFLD: 57;

 then |.(f . (w,a)).| = 0 by XREAL_1: 63;

 hence (f . (w,a)) = ( 0. F_Complex ) by COMPLFLD: 58;

 end;

 hence thesis by A1;

 end;

 thus thesis by BILINEAR: 41;

 end;

 theorem :: HERMITAN:54

 for V be non empty ModuleStr over F_Complex , f be Form of V, V holds ( diagker f) = ( diagker (f *' ))

 proof

 let V be non empty ModuleStr over F_Complex , f be Form of V, V;

 set K = F_Complex ;

 thus ( diagker f) c= ( diagker (f *' ))

 proof

 let x be object;

 assume x in ( diagker f);

 then

 consider v be Vector of V such that

 A1: x = v and

 A2: (f . (v,v)) = ( 0. K);

 ((f *' ) . (v,v)) = ( 0. K) by A2, Def8, COMPLFLD: 47;

 hence thesis by A1;

 end;

 let x be object;

 assume x in ( diagker (f *' ));

 then

 consider v be Vector of V such that

 A3: x = v and

 A4: ((f *' ) . (v,v)) = ( 0. K);

 (((f . (v,v)) *' ) *' ) = ( 0. K) by A4, Def8, COMPLFLD: 47;

 hence thesis by A3;

 end;

 theorem :: HERMITAN:55



 Th55: 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 *' ))

 proof

 let V,W be non empty ModuleStr over F_Complex , f be Form of V, W;

 set K = F_Complex ;

 thus ( leftker f) c= ( leftker (f *' ))

 proof

 let x be object;

 assume x in ( leftker f);

 then

 consider v be Vector of V such that

 A1: x = v and

 A2: for w be Vector of W holds (f . (v,w)) = ( 0. K);

 now

 let w be Vector of W;

 ((f . (v,w)) *' ) = ( 0. K) by A2, COMPLFLD: 47;

 hence ((f *' ) . (v,w)) = ( 0. K) by Def8;

 end;

 hence thesis by A1;

 end;

 thus ( leftker (f *' )) c= ( leftker f)

 proof

 let x be object;

 assume x in ( leftker (f *' ));

 then

 consider v be Vector of V such that

 A3: x = v and

 A4: for w be Vector of W holds ((f *' ) . (v,w)) = ( 0. K);

 now

 let w be Vector of W;

 (((f *' ) . (v,w)) *' ) = ( 0. K) by A4, COMPLFLD: 47;

 then (((f . (v,w)) *' ) *' ) = ( 0. K) by Def8;

 hence (f . (v,w)) = ( 0. K);

 end;

 hence thesis by A3;

 end;

 thus ( rightker f) c= ( rightker (f *' ))

 proof

 let x be object;

 assume x in ( rightker f);

 then

 consider w be Vector of W such that

 A5: x = w and

 A6: for v be Vector of V holds (f . (v,w)) = ( 0. K);

 now

 let v be Vector of V;

 ((f . (v,w)) *' ) = ( 0. K) by A6, COMPLFLD: 47;

 hence ((f *' ) . (v,w)) = ( 0. K) by Def8;

 end;

 hence thesis by A5;

 end;

 let x be object;

 assume x in ( rightker (f *' ));

 then

 consider w be Vector of W such that

 A7: x = w and

 A8: for v be Vector of V holds ((f *' ) . (v,w)) = ( 0. K);

 now

 let v be Vector of V;

 (((f *' ) . (v,w)) *' ) = ( 0. K) by A8, COMPLFLD: 47;

 then (((f . (v,w)) *' ) *' ) = ( 0. K) by Def8;

 hence (f . (v,w)) = ( 0. K);

 end;

 hence thesis by A7;

 end;

 theorem :: HERMITAN:56



 Th56: for V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V holds ( LKer f) = ( RKer (f *' ))

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 the carrier of ( LKer f) = ( leftker f) by BILINEAR:def 18

 .= ( diagker f) by Th52

 .= ( rightker f) by Th53

 .= ( rightker (f *' )) by Th55

 .= the carrier of ( RKer (f *' )) by BILINEAR:def 19;

 hence thesis by VECTSP_4: 29;

 end;

 theorem :: HERMITAN:57



 Th57: for V be VectSp of F_Complex , f be diagReR+0valued diagRvalued Form of V, V holds for v be Vector of V st ( Re (f . (v,v))) = 0 holds (f . (v,v)) = ( 0. F_Complex )

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued diagRvalued Form of V, V, v be Vector of V;

 assume

 A1: ( Re (f . (v,v))) = 0 ;

 ( Im (f . (v,v))) = 0 by Def6;

 then (f . (v,v)) = ( 0 + ( 0 * )) by A1, COMPLEX1: 13;

 hence thesis by COMPLFLD: 7;

 end;

 theorem :: HERMITAN:58



 Th58: 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)

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V, v be Vector of V;

 assume that

 A1: ( Re (f . (v,v))) = 0 and

 A2: f is non degenerated-on-left or f is non degenerated-on-right;

 (f . (v,v)) = ( 0. F_Complex ) by A1, Th57;

 then

 A3: v in { w where w be Vector of V : (f . (w,w)) = ( 0. F_Complex ) };

 per cases by A2;

 suppose f is non degenerated-on-left;

 then {( 0. V)} = ( diagker f) by Th52;

 hence thesis by A3, TARSKI:def 1;

 end;

 suppose f is non degenerated-on-right;

 then {( 0. V)} = ( diagker f) by Th53;

 hence thesis by A3, TARSKI:def 1;

 end;

 end;

 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;

 :: HERMITAN:def11

 func RQ*Form (f) -> additiveFAF cmplxhomogeneousFAF Form of V, ( VectQuot (W,( RKer (f *' )))) equals (( RQForm (f *' )) *' );

 correctness ;

 end

 theorem :: HERMITAN:59



 Th59: for V be non empty ModuleStr over F_Complex , W be VectSp of F_Complex holds for f be additiveFAF cmplxhomogeneousFAF Form of V, W holds for v be Vector of V, w be Vector of W holds (( RQ*Form f) . (v,(w + ( RKer (f *' ))))) = (f . (v,w))

 proof

 let V be non empty ModuleStr over F_Complex , W be VectSp of F_Complex , f be additiveFAF cmplxhomogeneousFAF Form of V, W, v be Vector of V, w be Vector of W;

 reconsider A = (w + ( RKer (f *' ))) as Vector of ( VectQuot (W,( RKer (f *' )))) by VECTSP10: 23;



 thus (( RQ*Form f) . (v,(w + ( RKer (f *' ))))) = ((( RQForm (f *' )) . (v,A)) *' ) by Def8

 .= (((f *' ) . (v,w)) *' ) by BILINEAR:def 21

 .= (((f . (v,w)) *' ) *' ) by Def8

 .= (f . (v,w));

 end;

 registration

 let V,W be VectSp of F_Complex ;

 let f be sesquilinear-Form of V, W;

 cluster ( LQForm f) -> additiveFAF cmplxhomogeneousFAF;

 coherence

 proof

 set lf = ( LQForm f);

 thus ( LQForm f) is additiveFAF

 proof

 let A be Vector of ( VectQuot (V,( LKer f)));

 set flf = ( FunctionalFAF (lf,A));

 consider v be Vector of V such that

 A1: A = (v + ( LKer f)) by VECTSP10: 22;

 let w,t be Vector of W;



 thus (flf . (w + t)) = (lf . (A,(w + t))) by BILINEAR: 8

 .= (f . (v,(w + t))) by A1, BILINEAR:def 20

 .= ((f . (v,w)) + (f . (v,t))) by BILINEAR: 27

 .= ((lf . (A,w)) + (f . (v,t))) by A1, BILINEAR:def 20

 .= ((lf . (A,w)) + (lf . (A,t))) by A1, BILINEAR:def 20

 .= ((flf . w) + (lf . (A,t))) by BILINEAR: 8

 .= ((flf . w) + (flf . t)) by BILINEAR: 8;

 end;

 let A be Vector of ( VectQuot (V,( LKer f)));

 set flf = ( FunctionalFAF (lf,A));

 consider v be Vector of V such that

 A2: A = (v + ( LKer f)) by VECTSP10: 22;

 let w be Vector of W, r be Scalar of W;



 thus (flf . (r * w)) = (lf . (A,(r * w))) by BILINEAR: 8

 .= (f . (v,(r * w))) by A2, BILINEAR:def 20

 .= ((r *' ) * (f . (v,w))) by Th27

 .= ((r *' ) * (lf . (A,w))) by A2, BILINEAR:def 20

 .= ((r *' ) * (flf . w)) by BILINEAR: 8;

 end;

 cluster ( RQ*Form f) -> additiveSAF homogeneousSAF;

 coherence

 proof

 set lf = ( RQ*Form f);

 thus ( RQ*Form f) is additiveSAF

 proof

 let A be Vector of ( VectQuot (W,( RKer (f *' ))));

 set flf = ( FunctionalSAF (lf,A));

 consider w be Vector of W such that

 A3: A = (w + ( RKer (f *' ))) by VECTSP10: 22;

 let v,t be Vector of V;



 thus (flf . (v + t)) = (lf . ((v + t),A)) by BILINEAR: 9

 .= (f . ((v + t),w)) by A3, Th59

 .= ((f . (v,w)) + (f . (t,w))) by BILINEAR: 26

 .= ((lf . (v,A)) + (f . (t,w))) by A3, Th59

 .= ((lf . (v,A)) + (lf . (t,A))) by A3, Th59

 .= ((flf . v) + (lf . (t,A))) by BILINEAR: 9

 .= ((flf . v) + (flf . t)) by BILINEAR: 9;

 end;

 let A be Vector of ( VectQuot (W,( RKer (f *' ))));

 set flf = ( FunctionalSAF (lf,A));

 consider w be Vector of W such that

 A4: A = (w + ( RKer (f *' ))) by VECTSP10: 22;

 let v be Vector of V, r be Scalar of V;



 thus (flf . (r * v)) = (lf . ((r * v),A)) by BILINEAR: 9

 .= (f . ((r * v),w)) by A4, Th59

 .= (r * (f . (v,w))) by BILINEAR: 31

 .= (r * (lf . (v,A))) by A4, Th59

 .= (r * (flf . v)) by BILINEAR: 9;

 end;

 end

 definition

 let V,W be VectSp of F_Complex ;

 let f be sesquilinear-Form of V, W;

 :: HERMITAN:def12

 func Q*Form (f) -> sesquilinear-Form of ( VectQuot (V,( LKer f))), ( VectQuot (W,( RKer (f *' )))) means

 : Def12: for A be Vector of ( VectQuot (V,( LKer f))), B be Vector of ( VectQuot (W,( RKer (f *' )))) holds 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));

 existence

 proof

 set K = F_Complex , L = ( LKer f), vq = ( VectQuot (V,L)), Cv = ( CosetSet (V,L)), aCv = ( addCoset (V,L)), mCv = ( lmultCoset (V,L)), R = ( RKer (f *' )), wq = ( VectQuot (W,R)), Cw = ( CosetSet (W,R)), aCw = ( addCoset (W,R)), mCw = ( lmultCoset (W,R));

 defpred P[ set, set, set] means for v be Vector of V, w be Vector of W st $1 = (v + L) & $2 = (w + R) holds $3 = (f . (v,w));



 A1: ( rightker f) = ( rightker (f *' )) by Th55;

 A2:

 now

 let A be Vector of vq, B be Vector of wq;

 consider a be Vector of V such that

 A3: A = (a + L) by VECTSP10: 22;

 consider b be Vector of W such that

 A4: B = (b + R) by VECTSP10: 22;

 take y = (f . (a,b));

 now

 let a1 be Vector of V;

 let b1 be Vector of W;

 assume A = (a1 + L);

 then a in (a1 + L) by A3, VECTSP_4: 44;

 then

 consider vv be Vector of V such that

 A5: vv in L and

 A6: a = (a1 + vv) by VECTSP_4: 42;

 vv in the carrier of L by A5, STRUCT_0:def 5;

 then vv in ( leftker f) by BILINEAR:def 18;

 then

 A7: ex aa be Vector of V st aa = vv & for w0 be Vector of W holds (f . (aa,w0)) = ( 0. K);

 assume B = (b1 + R);

 then b in (b1 + R) by A4, VECTSP_4: 44;

 then

 consider ww be Vector of W such that

 A8: ww in R and

 A9: b = (b1 + ww) by VECTSP_4: 42;

 ww in the carrier of R by A8, STRUCT_0:def 5;

 then ww in ( rightker (f *' )) by BILINEAR:def 19;

 then

 A10: ex bb be Vector of W st bb = ww & for v0 be Vector of V holds (f . (v0,bb)) = ( 0. K) by A1;



 thus y = (((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww)))) by A6, A9, BILINEAR: 28

 .= (((f . (a1,b1)) + ( 0. K)) + ((f . (vv,b1)) + (f . (vv,ww)))) by A10

 .= (((f . (a1,b1)) + ( 0. K)) + (( 0. K) + (f . (vv,ww)))) by A7

 .= ((f . (a1,b1)) + (( 0. K) + (f . (vv,ww)))) by RLVECT_1:def 4

 .= ((f . (a1,b1)) + (f . (vv,ww))) by RLVECT_1: 4

 .= ((f . (a1,b1)) + ( 0. K)) by A7

 .= (f . (a1,b1)) by RLVECT_1:def 4;

 end;

 hence P[A, B, y];

 end;

 consider ff be Function of [:the carrier of vq, the carrier of wq:], the carrier of K such that

 A11: for A be Vector of vq, B be Vector of wq holds P[A, B, (ff . (A,B))] from BINOP_1:sch 3( A2);

 reconsider ff as Form of vq, wq;



 A12: Cv = the carrier of vq by VECTSP10:def 6;

 A13:

 now

 let ww be Vector of wq;

 consider w be Vector of W such that

 A14: ww = (w + R) by VECTSP10: 22;

 set ffw = ( FunctionalSAF (ff,ww));

 now

 let A be Vector of vq, r be Element of K;

 consider a be Vector of V such that

 A15: A = (a + L) by VECTSP10: 22;



 A16: the lmult of vq = mCv & (mCv . (r,A)) = ((r * a) + L) by A12, A15, VECTSP10:def 5, VECTSP10:def 6;



 thus (ffw . (r * A)) = (ff . ((the lmult of vq . (r,A)),ww)) by BILINEAR: 9

 .= (f . ((r * a),w)) by A11, A14, A16

 .= (r * (f . (a,w))) by BILINEAR: 31

 .= (r * (ff . (A,ww))) by A11, A14, A15

 .= (r * (ffw . A)) by BILINEAR: 9;

 end;

 hence ffw is homogeneous;

 end;



 A17: Cw = the carrier of wq by VECTSP10:def 6;

 A18:

 now

 let vv be Vector of vq;

 consider v be Vector of V such that

 A19: vv = (v + L) by VECTSP10: 22;

 set ffv = ( FunctionalFAF (ff,vv));

 now

 let A be Vector of wq, r be Element of K;

 consider a be Vector of W such that

 A20: A = (a + R) by VECTSP10: 22;



 A21: the lmult of wq = mCw & (mCw . (r,A)) = ((r * a) + R) by A17, A20, VECTSP10:def 5, VECTSP10:def 6;



 thus (ffv . (r * A)) = (ff . (vv,(the lmult of wq . (r,A)))) by BILINEAR: 8

 .= (f . (v,(r * a))) by A11, A19, A21

 .= ((r *' ) * (f . (v,a))) by Th27

 .= ((r *' ) * (ff . (vv,A))) by A11, A19, A20

 .= ((r *' ) * (ffv . A)) by BILINEAR: 8;

 end;

 hence ffv is cmplxhomogeneous;

 end;

 A22:

 now

 let ww be Vector of wq;

 consider w be Vector of W such that

 A23: ww = (w + R) by VECTSP10: 22;

 set ffw = ( FunctionalSAF (ff,ww));

 now

 let A,B be Vector of vq;

 consider a be Vector of V such that

 A24: A = (a + L) by VECTSP10: 22;

 consider b be Vector of V such that

 A25: B = (b + L) by VECTSP10: 22;



 A26: the addF of vq = aCv & (aCv . (A,B)) = ((a + b) + L) by A12, A24, A25, VECTSP10:def 3, VECTSP10:def 6;



 thus (ffw . (A + B)) = (ff . ((the addF of vq . (A,B)),ww)) by BILINEAR: 9

 .= (f . ((a + b),w)) by A11, A23, A26

 .= ((f . (a,w)) + (f . (b,w))) by BILINEAR: 26

 .= ((ff . (A,ww)) + (f . (b,w))) by A11, A23, A24

 .= ((ff . (A,ww)) + (ff . (B,ww))) by A11, A23, A25

 .= ((ffw . A) + (ff . (B,ww))) by BILINEAR: 9

 .= ((ffw . A) + (ffw . B)) by BILINEAR: 9;

 end;

 hence ffw is additive;

 end;

 now

 let vv be Vector of vq;

 consider v be Vector of V such that

 A27: vv = (v + L) by VECTSP10: 22;

 set ffv = ( FunctionalFAF (ff,vv));

 now

 let A,B be Vector of wq;

 consider a be Vector of W such that

 A28: A = (a + R) by VECTSP10: 22;

 consider b be Vector of W such that

 A29: B = (b + R) by VECTSP10: 22;



 A30: the addF of wq = aCw & (aCw . (A,B)) = ((a + b) + R) by A17, A28, A29, VECTSP10:def 3, VECTSP10:def 6;



 thus (ffv . (A + B)) = (ff . (vv,(the addF of wq . (A,B)))) by BILINEAR: 8

 .= (f . (v,(a + b))) by A11, A27, A30

 .= ((f . (v,a)) + (f . (v,b))) by BILINEAR: 27

 .= ((ff . (vv,A)) + (f . (v,b))) by A11, A27, A28

 .= ((ff . (vv,A)) + (ff . (vv,B))) by A11, A27, A29

 .= ((ffv . A) + (ff . (vv,B))) by BILINEAR: 8

 .= ((ffv . A) + (ffv . B)) by BILINEAR: 8;

 end;

 hence ffv is additive;

 end;

 then

 reconsider ff as sesquilinear-Form of vq, wq by A22, A13, A18, Def4, BILINEAR:def 11, BILINEAR:def 12, BILINEAR:def 14;

 take ff;

 thus thesis by A11;

 end;

 uniqueness

 proof

 set L = ( LKer f), vq = ( VectQuot (V,L)), R = ( RKer (f *' )), wq = ( VectQuot (W,R));

 let f1,f2 be sesquilinear-Form of vq, wq;

 assume that

 A31: for A be Vector of vq, B be Vector of wq holds for v be Vector of V, w be Vector of W st A = (v + L) & B = (w + R) holds (f1 . (A,B)) = (f . (v,w)) and

 A32: for A be Vector of vq, B be Vector of wq holds for v be Vector of V, w be Vector of W st A = (v + L) & B = (w + R) holds (f2 . (A,B)) = (f . (v,w));

 now

 let A be Vector of vq, B be Vector of wq;

 consider a be Vector of V such that

 A33: A = (a + L) by VECTSP10: 22;

 consider b be Vector of W such that

 A34: B = (b + R) by VECTSP10: 22;



 thus (f1 . (A,B)) = (f . (a,b)) by A31, A33, A34

 .= (f2 . (A,B)) by A32, A33, A34;

 end;

 hence thesis;

 end;

 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;

 coherence

 proof

 set K = F_Complex ;

 consider v be Vector of V, w be Vector of W such that

 A1: (f . (v,w)) <> ( 0. K) by BILINEAR: 40;

 reconsider B = (w + ( RKer (f *' ))) as Vector of ( VectQuot (W,( RKer (f *' )))) by VECTSP10: 23;

 reconsider A = (v + ( LKer f)) as Vector of ( VectQuot (V,( LKer f))) by VECTSP10: 23;

 (( Q*Form f) . (A,B)) = (f . (v,w)) by Def12;

 hence thesis by A1, BILINEAR: 40;

 end;

 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;

 coherence

 proof

 set K = F_Complex , qf = ( RQ*Form f), R = ( RKer (f *' )), qW = ( VectQuot (W,R));



 A1: ( rightker f) = ( rightker (f *' )) by Th55;

 thus ( rightker qf) c= {( 0. qW)}

 proof

 let x be object;

 assume x in ( rightker qf);

 then

 consider ww be Vector of qW such that

 A2: x = ww and

 A3: for v be Vector of V holds (qf . (v,ww)) = ( 0. K);

 consider w be Vector of W such that

 A4: ww = (w + R) by VECTSP10: 22;

 now

 let v be Vector of V;



 thus (f . (v,w)) = (qf . (v,ww)) by A4, Th59

 .= ( 0. K) by A3;

 end;

 then w in ( rightker f);

 then w in the carrier of R by A1, BILINEAR:def 19;

 then w in R by STRUCT_0:def 5;



 then (w + R) = ( zeroCoset (W,R)) by VECTSP_4: 49

 .= ( 0. qW) by VECTSP10: 21;

 hence thesis by A2, A4, TARSKI:def 1;

 end;

 let x be object;

 assume x in {( 0. qW)};

 then

 A5: x = ( 0. qW) by TARSKI:def 1;

 for v be Vector of V holds (qf . (v,( 0. qW))) = ( 0. K) by BILINEAR: 29;

 hence thesis by A5;

 end;

 end

 theorem :: HERMITAN:60



 Th60: for V be non empty ModuleStr over F_Complex , W be VectSp of F_Complex holds for f be additiveFAF cmplxhomogeneousFAF Form of V, W holds ( leftker f) = ( leftker ( RQ*Form f))

 proof

 set K = F_Complex ;

 let V be non empty ModuleStr over K, W be VectSp of K;

 let f be additiveFAF cmplxhomogeneousFAF Form of V, W;

 set rf = ( RQ*Form f), qw = ( VectQuot (W,( RKer (f *' ))));

 thus ( leftker f) c= ( leftker ( RQ*Form f))

 proof

 let x be object;

 assume x in ( leftker f);

 then

 consider v be Vector of V such that

 A1: x = v and

 A2: for w be Vector of W holds (f . (v,w)) = ( 0. K);

 now

 let A be Vector of qw;

 consider w be Vector of W such that

 A3: A = (w + ( RKer (f *' ))) by VECTSP10: 22;



 thus (rf . (v,A)) = (f . (v,w)) by A3, Th59

 .= ( 0. K) by A2;

 end;

 hence thesis by A1;

 end;

 let x be object;

 assume x in ( leftker rf);

 then

 consider v be Vector of V such that

 A4: x = v and

 A5: for A be Vector of qw holds (rf . (v,A)) = ( 0. K);

 now

 let w be Vector of W;

 reconsider A = (w + ( RKer (f *' ))) as Vector of qw by VECTSP10: 23;



 thus (f . (v,w)) = (rf . (v,A)) by Th59

 .= ( 0. K) by A5;

 end;

 hence thesis by A4;

 end;

 theorem :: HERMITAN:61



 Th61: for V,W be VectSp of F_Complex , f be sesquilinear-Form of V, W holds ( RKer (f *' )) = ( RKer (( LQForm f) *' ))

 proof

 set K = F_Complex ;

 let V,W be VectSp of K, f be sesquilinear-Form of V, W;

 the carrier of ( RKer (f *' )) = ( rightker (f *' )) by BILINEAR:def 19

 .= ( rightker f) by Th55

 .= ( rightker ( LQForm f)) by BILINEAR: 44

 .= ( rightker (( LQForm f) *' )) by Th55

 .= the carrier of ( RKer (( LQForm f) *' )) by BILINEAR:def 19;

 hence thesis by VECTSP_4: 29;

 end;

 theorem :: HERMITAN:62



 Th62: for V,W be VectSp of F_Complex , f be sesquilinear-Form of V, W holds ( LKer f) = ( LKer ( RQ*Form f))

 proof

 set K = F_Complex ;

 let V,W be VectSp of K, f be sesquilinear-Form of V, W;

 the carrier of ( LKer f) = ( leftker f) by BILINEAR:def 18

 .= ( leftker ( RQ*Form f)) by Th60

 .= the carrier of ( LKer ( RQ*Form f)) by BILINEAR:def 18;

 hence thesis by VECTSP_4: 29;

 end;

 theorem :: HERMITAN:63



 Th63: 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))

 proof

 set K = F_Complex ;

 let V,W be VectSp of K, f be sesquilinear-Form of V, W;

 set L = ( LKer f), vq = ( VectQuot (V,L)), R = ( RKer (f *' )), wq = ( VectQuot (W,R)), RL = ( RKer (( LQForm f) *' )), wqr = ( VectQuot (W,RL)), LR = ( LKer ( RQ*Form f)), vql = ( VectQuot (V,LR));



 A1: ( dom ( Q*Form f)) = [:the carrier of vq, the carrier of wq:] by FUNCT_2:def 1;

 A2:

 now



 A3: R = RL by Th61;

 let x be object;

 assume x in ( dom ( Q*Form f));

 then

 consider A,B be object such that

 A4: A in the carrier of vq and

 A5: B in the carrier of wq and

 A6: x = [A, B] by ZFMISC_1:def 2;

 reconsider A as Vector of vq by A4;

 consider v be Vector of V such that

 A7: A = (v + L) by VECTSP10: 22;

 reconsider B as Vector of wq by A5;

 consider w be Vector of W such that

 A8: B = (w + R) by VECTSP10: 22;



 thus (( Q*Form f) . x) = (( Q*Form f) . (A,B)) by A6

 .= (f . (v,w)) by A7, A8, Def12

 .= (( LQForm f) . (A,w)) by A7, BILINEAR:def 20

 .= (( RQ*Form ( LQForm f)) . (A,B)) by A8, A3, Th59

 .= (( RQ*Form ( LQForm f)) . x) by A6;

 end;

 ( dom ( RQ*Form ( LQForm f))) = [:the carrier of vq, the carrier of wqr:] & the carrier of wqr = the carrier of wq by Th61, FUNCT_2:def 1;

 hence ( Q*Form f) = ( RQ*Form ( LQForm f)) by A1, A2;

 A9:

 now



 A10: L = LR by Th62;

 let x be object;

 assume x in ( dom ( Q*Form f));

 then

 consider A,B be object such that

 A11: A in the carrier of vq and

 A12: B in the carrier of wq and

 A13: x = [A, B] by ZFMISC_1:def 2;

 reconsider A as Vector of vq by A11;

 consider v be Vector of V such that

 A14: A = (v + L) by VECTSP10: 22;

 reconsider B as Vector of wq by A12;

 consider w be Vector of W such that

 A15: B = (w + R) by VECTSP10: 22;



 thus (( Q*Form f) . x) = (( Q*Form f) . (A,B)) by A13

 .= (f . (v,w)) by A14, A15, Def12

 .= (( RQ*Form f) . (v,B)) by A15, Th59

 .= (( LQForm ( RQ*Form f)) . (A,B)) by A14, A10, BILINEAR:def 20

 .= (( LQForm ( RQ*Form f)) . x) by A13;

 end;

 ( dom ( LQForm ( RQ*Form f))) = [:the carrier of vql, the carrier of wq:] & the carrier of vql = the carrier of vq by Th62, FUNCT_2:def 1;

 hence thesis by A1, A9;

 end;

 theorem :: HERMITAN:64



 Th64: 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)))

 proof

 set K = F_Complex ;

 let V,W be VectSp of K, f be sesquilinear-Form of V, W;

 set vq = ( VectQuot (V,( LKer f))), wq = ( VectQuot (W,( RKer (f *' )))), wqr = ( VectQuot (W,( RKer (( LQForm f) *' )))), vql = ( VectQuot (V,( LKer ( RQ*Form f))));

 set rlf = ( RQ*Form ( LQForm f)), qf = ( Q*Form f), lrf = ( LQForm ( RQ*Form f));

 thus ( leftker qf) c= ( leftker rlf)

 proof

 let x be object;

 assume x in ( leftker qf);

 then

 consider vv be Vector of vq such that

 A1: x = vv and

 A2: for ww be Vector of wq holds (qf . (vv,ww)) = ( 0. K);

 now

 let ww be Vector of wqr;

 reconsider w = ww as Vector of wq by Th61;



 thus (rlf . (vv,ww)) = (qf . (vv,w)) by Th63

 .= ( 0. K) by A2;

 end;

 hence thesis by A1;

 end;

 thus ( leftker rlf) c= ( leftker qf)

 proof

 let x be object;

 assume x in ( leftker rlf);

 then

 consider vv be Vector of vq such that

 A3: x = vv and

 A4: for ww be Vector of wqr holds (rlf . (vv,ww)) = ( 0. K);

 now

 let ww be Vector of wq;

 reconsider w = ww as Vector of wqr by Th61;



 thus (qf . (vv,ww)) = (rlf . (vv,w)) by Th63

 .= ( 0. K) by A4;

 end;

 hence thesis by A3;

 end;

 thus ( rightker qf) c= ( rightker rlf)

 proof

 let x be object;

 assume x in ( rightker qf);

 then

 consider ww be Vector of wq such that

 A5: x = ww and

 A6: for vv be Vector of vq holds (qf . (vv,ww)) = ( 0. K);

 reconsider w = ww as Vector of wqr by Th61;

 now

 let vv be Vector of vq;



 thus (rlf . (vv,w)) = (qf . (vv,ww)) by Th63

 .= ( 0. K) by A6;

 end;

 hence thesis by A5;

 end;

 thus ( rightker rlf) c= ( rightker qf)

 proof

 let x be object;

 assume x in ( rightker rlf);

 then

 consider ww be Vector of wqr such that

 A7: x = ww and

 A8: for vv be Vector of vq holds (rlf . (vv,ww)) = ( 0. K);

 reconsider w = ww as Vector of wq by Th61;

 now

 let vv be Vector of vq;



 thus (qf . (vv,w)) = (rlf . (vv,ww)) by Th63

 .= ( 0. K) by A8;

 end;

 hence thesis by A7;

 end;

 thus ( leftker qf) c= ( leftker lrf)

 proof

 let x be object;

 assume x in ( leftker qf);

 then

 consider vv be Vector of vq such that

 A9: x = vv and

 A10: for ww be Vector of wq holds (qf . (vv,ww)) = ( 0. K);

 reconsider v = vv as Vector of vql by Th62;

 now

 let ww be Vector of wq;



 thus (lrf . (v,ww)) = (qf . (vv,ww)) by Th63

 .= ( 0. K) by A10;

 end;

 hence thesis by A9;

 end;

 thus ( leftker lrf) c= ( leftker qf)

 proof

 let x be object;

 assume x in ( leftker lrf);

 then

 consider vv be Vector of vql such that

 A11: x = vv and

 A12: for ww be Vector of wq holds (lrf . (vv,ww)) = ( 0. K);

 reconsider v = vv as Vector of vq by Th62;

 now

 let ww be Vector of wq;



 thus (qf . (v,ww)) = (lrf . (vv,ww)) by Th63

 .= ( 0. K) by A12;

 end;

 hence thesis by A11;

 end;

 thus ( rightker qf) c= ( rightker lrf)

 proof

 let x be object;

 assume x in ( rightker qf);

 then

 consider ww be Vector of wq such that

 A13: x = ww and

 A14: for vv be Vector of vq holds (qf . (vv,ww)) = ( 0. K);

 now

 let vv be Vector of vql;

 reconsider v = vv as Vector of vq by Th62;



 thus (lrf . (vv,ww)) = (qf . (v,ww)) by Th63

 .= ( 0. K) by A14;

 end;

 hence thesis by A13;

 end;

 let x be object;

 assume x in ( rightker lrf);

 then

 consider ww be Vector of wq such that

 A15: x = ww and

 A16: for vv be Vector of vql holds (lrf . (vv,ww)) = ( 0. K);

 now

 let vv be Vector of vq;

 reconsider v = vv as Vector of vql by Th62;



 thus (qf . (vv,ww)) = (lrf . (v,ww)) by Th63

 .= ( 0. K) by A16;

 end;

 hence thesis by A15;

 end;

 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;

 coherence

 proof

 ( leftker ( LQForm f)) = {( 0. ( VectQuot (V,( LKer f))))} by BILINEAR:def 23;

 then ( leftker ( RQ*Form ( LQForm f))) = {( 0. ( VectQuot (V,( LKer f))))} by Th60;

 hence thesis;

 end;

 cluster ( LQForm ( RQ*Form f)) -> non degenerated-on-left non degenerated-on-right;

 coherence

 proof

 ( rightker ( RQ*Form f)) = {( 0. ( VectQuot (W,( RKer (f *' )))))} by BILINEAR:def 24;

 then ( rightker ( LQForm ( RQ*Form f))) = {( 0. ( VectQuot (W,( RKer (f *' )))))} by BILINEAR: 44;

 hence thesis;

 end;

 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;

 coherence

 proof



 A1: ( leftker ( RQ*Form ( LQForm f))) = {( 0. ( VectQuot (V,( LKer f))))} & ( rightker ( LQForm ( RQ*Form f))) = {( 0. ( VectQuot (W,( RKer (f *' )))))} by BILINEAR:def 23, BILINEAR:def 24;

 ( leftker ( RQ*Form ( LQForm f))) = ( leftker ( Q*Form f)) & ( rightker ( LQForm ( RQ*Form f))) = ( rightker ( Q*Form f)) by Th64;

 hence thesis by A1;

 end;

 end

 begin

 definition

 let V be non empty ModuleStr over F_Complex ;

 let f be Form of V, V;

 :: HERMITAN:def13

 attr f is positivediagvalued means 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;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is positivediagvalued additiveSAF;

 let v be Vector of V;

 per cases ;

 suppose

 A2: v = ( 0. V);



 A3: [**( Re ( 0. F_Complex )), ( Im ( 0. F_Complex ))**] = [** 0 , 0 **] by COMPLEX1: 13, COMPLFLD: 7;

 (f . (v,v)) = ( 0. F_Complex ) by A1, A2, BILINEAR: 30;

 hence thesis by A3, COMPLEX1: 77;

 end;

 suppose v <> ( 0. V);

 hence thesis by A1;

 end;

 end;

 end

 registration

 let V be right_zeroed non empty ModuleStr over F_Complex ;

 cluster positivediagvalued additiveFAF -> diagReR+0valued for Form of V, V;

 coherence

 proof

 let f be Form of V, V;

 assume

 A1: f is positivediagvalued additiveFAF;

 let v be Vector of V;

 per cases ;

 suppose

 A2: v = ( 0. V);



 A3: [**( Re ( 0. F_Complex )), ( Im ( 0. F_Complex ))**] = [** 0 , 0 **] by COMPLEX1: 13, COMPLFLD: 7;

 (f . (v,v)) = ( 0. F_Complex ) by A1, A2, BILINEAR: 29;

 hence thesis by A3, COMPLEX1: 77;

 end;

 suppose v <> ( 0. V);

 hence thesis by A1;

 end;

 end;

 end

 definition

 let V be VectSp of F_Complex ;

 let f be diagReR+0valued hermitan-Form of V;

 :: HERMITAN:def14

 func ScalarForm (f) -> diagReR+0valued hermitan-Form of ( VectQuot (V,( LKer f))) equals ( Q*Form f);

 coherence

 proof

 set vq = ( VectQuot (V,( LKer f))), vr = ( VectQuot (V,( RKer (f *' ))));

 vr = vq by Th56;

 then

 reconsider sc = ( Q*Form f) as Form of vq, vq;



 A1: sc is homogeneousSAF

 proof

 let w be Vector of vq;

 set fg = ( FunctionalSAF (sc,w));

 let v be Vector of vq, r be Scalar of vq;

 consider va be Vector of V such that

 A2: v = (va + ( LKer f)) by VECTSP10: 22;



 A3: (r * v) = ((r * va) + ( LKer f)) by A2, VECTSP10: 25;

 reconsider A = w as Vector of vr by Th56;

 consider wa be Vector of V such that

 A4: A = (wa + ( RKer (f *' ))) by VECTSP10: 22;



 thus (fg . (r * v)) = (( Q*Form f) . ((r * v),w)) by BILINEAR: 9

 .= (f . ((r * va),wa)) by A4, A3, Def12

 .= (r * (f . (va,wa))) by BILINEAR: 31

 .= (r * (sc . (v,w))) by A4, A2, Def12

 .= (r * (fg . v)) by BILINEAR: 9;

 end;



 A5: sc is additiveSAF

 proof

 let w be Vector of vq;

 set fg = ( FunctionalSAF (sc,w));

 let v1,v2 be Vector of vq;

 consider va be Vector of V such that

 A6: v1 = (va + ( LKer f)) by VECTSP10: 22;

 consider vb be Vector of V such that

 A7: v2 = (vb + ( LKer f)) by VECTSP10: 22;

 reconsider A = w as Vector of vr by Th56;

 consider wa be Vector of V such that

 A8: A = (wa + ( RKer (f *' ))) by VECTSP10: 22;



 A9: (v1 + v2) = ((va + vb) + ( LKer f)) by A6, A7, VECTSP10: 26;



 thus (fg . (v1 + v2)) = (( Q*Form f) . ((v1 + v2),w)) by BILINEAR: 9

 .= (f . ((va + vb),wa)) by A8, A9, Def12

 .= ((f . (va,wa)) + (f . (vb,wa))) by BILINEAR: 26

 .= ((sc . (v1,w)) + (f . (vb,wa))) by A8, A6, Def12

 .= ((sc . (v1,w)) + (sc . (v2,w))) by A8, A7, Def12

 .= ((fg . v1) + (sc . (v2,w))) by BILINEAR: 9

 .= ((fg . v1) + (fg . v2)) by BILINEAR: 9;

 end;



 A10: sc is hermitan

 proof

 let v,w be Vector of vq;

 reconsider A = w as Vector of vr by Th56;

 consider wa be Vector of V such that

 A11: A = (wa + ( RKer (f *' ))) by VECTSP10: 22;



 A12: w = (wa + ( LKer f)) by A11, Th56;

 reconsider B = v as Vector of vr by Th56;

 consider va be Vector of V such that

 A13: v = (va + ( LKer f)) by VECTSP10: 22;



 A14: B = (va + ( RKer (f *' ))) by A13, Th56;



 thus (sc . (v,w)) = (f . (va,wa)) by A11, A13, Def12

 .= ((f . (wa,va)) *' ) by Def5

 .= ((sc . (w,v)) *' ) by A14, A12, Def12;

 end;

 sc is diagReR+0valued

 proof

 let v be Vector of vq;

 reconsider A = v as Vector of vr by Th56;

 consider va be Vector of V such that

 A15: v = (va + ( LKer f)) by VECTSP10: 22;

 A = (va + ( RKer (f *' ))) by A15, Th56;

 then (sc . (v,v)) = (f . (va,va)) by A15, Def12;

 hence thesis by Def7;

 end;

 hence thesis by A1, A5, A10;

 end;

 end

 theorem :: HERMITAN:65

 for V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V holds 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))

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 set vq = ( VectQuot (V,( LKer f))), vr = ( VectQuot (V,( RKer (f *' ))));

 let A,B be Vector of vq, v,w be Vector of V;

 reconsider W = B as Vector of vr by Th56;

 assume that

 A1: A = (v + ( LKer f)) and

 A2: B = (w + ( LKer f));

 W = (w + ( RKer (f *' ))) by A2, Th56;

 hence thesis by A1, Def12;

 end;

 theorem :: HERMITAN:66



 Th66: for V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V holds ( leftker ( ScalarForm f)) = ( leftker ( Q*Form f))

 proof

 let V be VectSp of F_Complex , f be diagReR+0valued hermitan-Form of V;

 set vq = ( VectQuot (V,( LKer f))), vr = ( VectQuot (V,( RKer (f *' )))), qf = ( Q*Form f), qhf = ( ScalarForm f), K = F_Complex ;

 thus ( leftker qhf) c= ( leftker qf)

 proof

 let x be object;

 assume x in ( leftker qhf);

 then

 consider A be Vector of vq such that

 A1: x = A and

 A2: for B be Vector of vq holds (qhf . (A,B)) = ( 0. K);

 now

 let B be Vector of vr;

 reconsider w = B as Vector of vq by Th56;



 thus (qf . (A,B)) = (qhf . (A,w))

 .= ( 0. K) by A2;

 end;

 hence thesis by A1;

 end;

 let x be object;

 assume x in ( leftker qf);

 then

 consider A be Vector of vq such that

 A3: x = A and

 A4: for B be Vector of vr holds (qf . (A,B)) = ( 0. K);

 now

 let B be Vector of vq;

 reconsider w = B as Vector of vr by Th56;



 thus (qhf . (A,B)) = (qf . (A,w))

 .= ( 0. K) by A4;

 end;

 hence thesis by A3;

 end;

 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)) by Th56;

 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;

 coherence

 proof

 set vq = ( VectQuot (V,( LKer f))), vr = ( VectQuot (V,( RKer (f *' )))), qh = ( ScalarForm f);



 A1: ( leftker qh) = ( leftker ( Q*Form f)) by Th66

 .= {( 0. vq)} by BILINEAR:def 23;

 ( rightker qh) = ( rightker ( Q*Form f)) by Th56

 .= {( 0. vr)} by BILINEAR:def 24

 .= {( 0. vq)} by Th56;

 hence

 A2: qh is non degenerated-on-left & qh is non degenerated-on-right by A1;

 let A be Vector of vq;

 assume A <> ( 0. vq);

 then ( Re (qh . (A,A))) <> 0 by A2, Th58;

 hence thesis by Def7;

 end;

 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;

 coherence ;

 end