:: HERMITAN semantic presentation

Lemma1: 0 = [**0,0**]
;

theorem Th1: :: HERMITAN:1

for b₁ being complex number st b₁ = b₁ *' holds
Im b₁ = 0

proof end;

theorem Th2: :: HERMITAN:2

for b₁ being Element of COMPLEX st b₁ <> 0c holds
( |.[*((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)*].| = 1 & Re ([*((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)*] * b₁) = |.b₁.| & Im ([*((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)*] * b₁) = 0 )

proof end;

theorem Th3: :: HERMITAN:3

for b₁ being Element of COMPLEX ex b₂ being Element of COMPLEX st
( |.b₂.| = 1 & Re (b₂ * b₁) = |.b₁.| & Im (b₂ * b₁) = 0 )

proof end;

theorem Th4: :: HERMITAN:4

for b₁ being Element of COMPLEX holds b₁ * (b₁ *' ) = (|.b₁.| ^2 ) + (0 * )

proof end;

theorem Th5: :: HERMITAN:5

for b₁ being Element of F_Complex st b₁ = b₁ *' holds
Im b₁ = 0 by Th1;

i_FC *' = (Re i_FC ) - ((Im i_FC ) * ) by COMPLEX1:def 15
.= (Re ) - ((Im ) * )
.= 0 - (1 * ) by COMPLEX1:17 ;

then Lemma6: i_FC *' = "
;

theorem Th6: :: HERMITAN:6

canceled;

theorem Th7: :: HERMITAN:7

i_FC * (i_FC *' ) = 1. F_Complex

proof end;

theorem Th8: :: HERMITAN:8

for b₁ being Element of F_Complex st b₁ <> 0. F_Complex holds
( |.[**((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)**].| = 1 & Re ([**((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)**] * b₁) = |.b₁.| & Im ([**((Re b₁) / |.b₁.|),((- (Im b₁)) / |.b₁.|)**] * b₁) = 0 )

proof end;

E9: the unity of F_Complex = 1r by COMPLFLD:def 1
.= 1. F_Complex by COMPLFLD:10 ;

theorem Th9: :: HERMITAN:9

for b₁ being Element of F_Complex ex b₂ being Element of F_Complex st
( |.b₂.| = 1 & Re (b₂ * b₁) = |.b₁.| & Im (b₂ * b₁) = 0 )

proof end;

theorem Th10: :: HERMITAN:10

for b₁, b₂ being Element of F_Complex holds
( Re (b₁ - b₂) = (Re b₁) - (Re b₂) & Im (b₁ - b₂) = (Im b₁) - (Im b₂) )

proof end;

theorem Th11: :: HERMITAN:11

for b₁, b₂ being Element of F_Complex st Im b₁ = 0 holds
( Re (b₁ * b₂) = (Re b₁) * (Re b₂) & Im (b₁ * b₂) = (Re b₁) * (Im b₂) )

proof end;

theorem Th12: :: HERMITAN:12

for b₁, b₂ being Element of F_Complex st Im b₁ = 0 & Im b₂ = 0 holds
Im (b₁ * b₂) = 0

proof end;

Lemma13: for b₁ being Element of F_Complex holds Re b₁ = Re (b₁ *' )
by COMPLEX1:112;

theorem Th13: :: HERMITAN:13

canceled;

theorem Th14: :: HERMITAN:14

for b₁ being Element of F_Complex st Im b₁ = 0 holds
b₁ = b₁ *'

proof end;

theorem Th15: :: HERMITAN:15

for b₁, b₂ being Real holds [**b₁,0**] * [**b₂,0**] = [**(b₁ * b₂),0**] by COMPLFLD:6;

theorem Th16: :: HERMITAN:16

for b₁ being Element of F_Complex holds b₁ * (b₁ *' ) = [**(|.b₁.| ^2 ),0**]

proof end;

theorem Th17: :: HERMITAN:17

for b₁ being Element of F_Complex st 0 <= Re b₁ & Im b₁ = 0 holds
|.b₁.| = Re b₁

proof end;

theorem Th18: :: HERMITAN:18

for b₁ being Element of F_Complex holds (Re b₁) + (Re (b₁ *' )) = 2 * (Re b₁)

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
attr a₂ is cmplxhomogeneous means :Def1: :: HERMITAN:def 1
for b₁ being Vector of a₁
for b₂ being Scalar of holds a₂ . (b₂ * b₁) = (b₂ *' ) * (a₂ . b₁);

end;

:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def 1 :

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster 0Functional a₁ -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex ;
cluster cmplxhomogeneous -> 0-preserving Relation of the carrier of a₁,the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster additive 0-preserving cmplxhomogeneous Relation of the carrier of a₁,the carrier of F_Complex ;
existence

proof end;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
mode antilinear-Functional of a₁ is additive cmplxhomogeneous Functional of a₁;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂, c₃ be cmplxhomogeneous Functional of c₁;
cluster a₂ + a₃ -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be cmplxhomogeneous Functional of c₁;
cluster - a₂ -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Scalar of ;
let c₃ be cmplxhomogeneous Functional of c₁;
cluster a₂ * a₃ -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂, c₃ be cmplxhomogeneous Functional of c₁;
cluster a₂ - a₃ -> cmplxhomogeneous ;
coherence ;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
func c₂ *' -> Functional of a₁ means :Def2: :: HERMITAN:def 2
for b₁ being Vector of a₁ holds a₃ . b₁ = (a₂ . b₁) *' ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines *' HERMITAN:def 2 :

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be additive Functional of c₁;
cluster a₂ *' -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be homogeneous Functional of c₁;
cluster a₂ *' -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be cmplxhomogeneous Functional of c₁;
cluster a₂ *' -> homogeneous ;
coherence

proof end;

end;

registration

let c₁ be non trivial VectSp of F_Complex ;
let c₂ be non constant Functional of c₁;
cluster a₂ *' -> non constant ;
coherence

proof end;

end;

registration

let c₁ be non trivial VectSp of F_Complex ;
cluster non constant additive 0-preserving non trivial cmplxhomogeneous Relation of the carrier of a₁,the carrier of F_Complex ;
existence

proof end;

end;

theorem Th19: :: HERMITAN:19

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁ holds (b₂ *' ) *' = b₂

proof end;

theorem Th20: :: HERMITAN:20

for b₁ being non empty VectSpStr of F_Complex holds (0Functional b₁) *' = 0Functional b₁

proof end;

theorem Th21: :: HERMITAN:21

for b₁ being non empty VectSpStr of F_Complex
for b₂, b₃ being Functional of b₁ holds (b₂ + b₃) *' = (b₂ *' ) + (b₃ *' )

proof end;

theorem Th22: :: HERMITAN:22

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁ holds (- b₂) *' = - (b₂ *' )

proof end;

theorem Th23: :: HERMITAN:23

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁
for b₃ being Scalar of holds (b₃ * b₂) *' = (b₃ *' ) * (b₂ *' )

proof end;

theorem Th24: :: HERMITAN:24

for b₁ being non empty VectSpStr of F_Complex
for b₂, b₃ being Functional of b₁ holds (b₂ - b₃) *' = (b₂ *' ) - (b₃ *' )

proof end;

theorem Th25: :: HERMITAN:25

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁
for b₃ being Vector of b₁ holds
( b₂ . b₃ = 0. F_Complex iff (b₂ *' ) . b₃ = 0. F_Complex )

proof end;

theorem Th26: :: HERMITAN:26

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁ holds ker b₂ = ker (b₂ *' )

proof end;

theorem Th27: :: HERMITAN:27

for b₁ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex
for b₂ being antilinear-Functional of b₁ holds ker b₂ is lineary-closed

proof end;

theorem Th28: :: HERMITAN:28

for b₁ being VectSp of F_Complex
for b₂ being Subspace of b₁
for b₃ being antilinear-Functional of b₁ st the carrier of b₂ c= ker (b₃ *' ) holds
QFunctional b₃,b₂ is cmplxhomogeneous

proof end;

definition

let c₁ be VectSp of F_Complex ;
let c₂ be antilinear-Functional of c₁;
func QcFunctional c₂ -> antilinear-Functional of (VectQuot a₁,(Ker (a₂ *' ))) equals :: HERMITAN:def 3
QFunctional a₂,(Ker (a₂ *' ));
correctness

proof end;

end;

:: deftheorem Def3 defines QcFunctional HERMITAN:def 3 :

theorem Th29: :: HERMITAN:29

for b₁ being VectSp of F_Complex
for b₂ being antilinear-Functional of b₁
for b₃ being Vector of (VectQuot b₁,(Ker (b₂ *' )))
for b₄ being Vector of b₁ st b₃ = b₄ + (Ker (b₂ *' )) holds
(QcFunctional b₂) . b₃ = b₂ . b₄

proof end;

registration

let c₁ be non trivial VectSp of F_Complex ;
let c₂ be V72 antilinear-Functional of c₁;
cluster QcFunctional a₂ -> V72 0-preserving ;
coherence

proof end;

end;

registration

let c₁ be VectSp of F_Complex ;
let c₂ be antilinear-Functional of c₁;
cluster QcFunctional a₂ -> 0-preserving non degenerated ;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be Form of c₁,c₂;
attr a₃ is cmplxhomogeneousFAF means :Def4: :: HERMITAN:def 4
for b₁ being Vector of a₁ holds FunctionalFAF a₃,b₁ is cmplxhomogeneous;

end;

:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :

theorem Th30: :: HERMITAN:30

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃ being Vector of b₁
for b₄ being Vector of b₂
for b₅ being Element of F_Complex
for b₆ being Form of b₁,b₂ st b₆ is cmplxhomogeneousFAF holds
b₆ . [b₃,(b₅ * b₄)] = (b₅ *' ) * (b₆ . [b₃,b₄])

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Form of c₁,c₁;
attr a₂ is hermitan means :Def5: :: HERMITAN:def 5
for b₁, b₂ being Vector of a₁ holds a₂ . [b₁,b₂] = (a₂ . [b₂,b₁]) *' ;
attr a₂ is diagRvalued means :Def6: :: HERMITAN:def 6
for b₁ being Vector of a₁ holds Im (a₂ . [b₁,b₁]) = 0;
attr a₂ is diagReR+0valued means :Def7: :: HERMITAN:def 7
for b₁ being Vector of a₁ holds 0 <= Re (a₂ . [b₁,b₁]);

end;

:: deftheorem Def5 defines hermitan HERMITAN:def 5 :

:: deftheorem Def6 defines diagRvalued HERMITAN:def 6 :

:: deftheorem Def7 defines diagReR+0valued HERMITAN:def 7 :

E32: now

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
set c₃ = 0Functional c₁;
let c₄, c₅ be Vector of c₁;
thus (FormFunctional c₂,(0Functional c₁)) . [c₄,c₅] = (c₂ . c₄) * ((0Functional c₁) . c₅) by BILINEAR:def 11
.= (c₂ . c₄) * (0. F_Complex ) by HAHNBAN1:22
.= 0. F_Complex by VECTSP_1:39 ;

end;

Lemma33: for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁ holds FormFunctional b₂,(0Functional b₁) is hermitan

proof end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
cluster NulForm a₁,a₂ -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster NulForm a₁,a₁ -> cmplxhomogeneousFAF hermitan ;
coherence

proof end;

cluster NulForm a₁,a₁ -> cmplxhomogeneousFAF diagReR+0valued ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster hermitan -> diagRvalued Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
existence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
cluster additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Relation of [:the carrier of a₁,the carrier of a₂:],the carrier of F_Complex ;
existence

proof end;

end;

definition

let c₁, c₂ be non empty VectSpStr of F_Complex ;
mode sesquilinear-Form of a₁,a₂ is additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Form of a₁,a₂;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster additiveFAF hermitan -> additiveSAF Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster additiveSAF hermitan -> additiveFAF Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster homogeneousSAF hermitan -> cmplxhomogeneousFAF Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster cmplxhomogeneousFAF hermitan -> homogeneousSAF Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
mode hermitan-Form of a₁ is additiveSAF homogeneousSAF hermitan Form of a₁,a₁;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be Functional of c₁;
let c₄ be cmplxhomogeneous Functional of c₂;
cluster FormFunctional a₃,a₄ -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be cmplxhomogeneousFAF Form of c₁,c₂;
let c₄ be Vector of c₁;
cluster FunctionalFAF a₃,a₄ -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃, c₄ be cmplxhomogeneousFAF Form of c₁,c₂;
cluster a₃ + a₄ -> cmplxhomogeneousFAF ;
correctness

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be cmplxhomogeneousFAF Form of c₁,c₂;
let c₄ be Scalar of ;
cluster a₄ * a₃ -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be cmplxhomogeneousFAF Form of c₁,c₂;
cluster - a₃ -> cmplxhomogeneousFAF ;
coherence ;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃, c₄ be cmplxhomogeneousFAF Form of c₁,c₂;
cluster a₃ - a₄ -> cmplxhomogeneousFAF ;
coherence ;

end;

registration

let c₁, c₂ be non trivial VectSp of F_Complex ;
cluster non constant non trivial additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Relation of [:the carrier of a₁,the carrier of a₂:],the carrier of F_Complex ;
existence

proof end;

end;

definition

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be Form of c₁,c₂;
func c₃ *' -> Form of a₁,a₂ means :Def8: :: HERMITAN:def 8
for b₁ being Vector of a₁
for b₂ being Vector of a₂ holds a₄ . [b₁,b₂] = (a₃ . [b₁,b₂]) *' ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines *' HERMITAN:def 8 :

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be additiveFAF Form of c₁,c₂;
cluster a₃ *' -> additiveFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be additiveSAF Form of c₁,c₂;
cluster a₃ *' -> additiveSAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be homogeneousFAF Form of c₁,c₂;
cluster a₃ *' -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty VectSpStr of F_Complex ;
let c₃ be cmplxhomogeneousFAF Form of c₁,c₂;
cluster a₃ *' -> homogeneousFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be non trivial VectSp of F_Complex ;
let c₃ be non constant Form of c₁,c₂;
cluster a₃ *' -> non constant ;
coherence

proof end;

end;

theorem Th31: :: HERMITAN:31

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Functional of b₁
for b₃ being Vector of b₁ holds (FormFunctional b₂,(b₂ *' )) . [b₃,b₃] = [**(|.(b₂ . b₃).| ^2 ),0**]

proof end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
cluster FormFunctional a₂,(a₂ *' ) -> hermitan diagRvalued diagReR+0valued ;
coherence

proof end;

end;

registration

let c₁ be non trivial VectSp of F_Complex ;
cluster non constant non trivial additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
existence

proof end;

end;

theorem Th32: :: HERMITAN:32

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃ being Form of b₁,b₂ holds (b₃ *' ) *' = b₃

proof end;

theorem Th33: :: HERMITAN:33

for b₁, b₂ being non empty VectSpStr of F_Complex holds (NulForm b₁,b₂) *' = NulForm b₁,b₂

proof end;

theorem Th34: :: HERMITAN:34

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃, b₄ being Form of b₁,b₂ holds (b₃ + b₄) *' = (b₃ *' ) + (b₄ *' )

proof end;

theorem Th35: :: HERMITAN:35

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃ being Form of b₁,b₂ holds (- b₃) *' = - (b₃ *' )

proof end;

theorem Th36: :: HERMITAN:36

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃ being Form of b₁,b₂
for b₄ being Element of F_Complex holds (b₄ * b₃) *' = (b₄ *' ) * (b₃ *' )

proof end;

theorem Th37: :: HERMITAN:37

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃, b₄ being Form of b₁,b₂ holds (b₃ - b₄) *' = (b₃ *' ) - (b₄ *' )

proof end;

theorem Th38: :: HERMITAN:38

for b₁, b₂ being VectSp of F_Complex
for b₃ being Vector of b₁
for b₄, b₅ being Vector of b₂
for b₆ being additiveFAF cmplxhomogeneousFAF Form of b₁,b₂ holds b₆ . [b₃,(b₄ - b₅)] = (b₆ . [b₃,b₄]) - (b₆ . [b₃,b₅])

proof end;

theorem Th39: :: HERMITAN:39

for b₁, b₂ being VectSp of F_Complex
for b₃, b₄ being Vector of b₁
for b₅, b₆ being Vector of b₂
for b₇ being sesquilinear-Form of b₁,b₂ holds b₇ . [(b₃ - b₄),(b₅ - b₆)] = ((b₇ . [b₃,b₅]) - (b₇ . [b₃,b₆])) - ((b₇ . [b₄,b₅]) - (b₇ . [b₄,b₆]))

proof end;

theorem Th40: :: HERMITAN:40

for b₁, b₂ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex
for b₃, b₄ being Vector of b₁
for b₅, b₆ being Vector of b₂
for b₇, b₈ being Element of F_Complex
for b₉ being sesquilinear-Form of b₁,b₂ holds b₉ . [(b₃ + (b₇ * b₄)),(b₅ + (b₈ * b₆))] = ((b₉ . [b₃,b₅]) + ((b₈ *' ) * (b₉ . [b₃,b₆]))) + ((b₇ * (b₉ . [b₄,b₅])) + (b₇ * ((b₈ *' ) * (b₉ . [b₄,b₆]))))

proof end;

theorem Th41: :: HERMITAN:41

for b₁, b₂ being VectSp of F_Complex
for b₃, b₄ being Vector of b₁
for b₅, b₆ being Vector of b₂
for b₇, b₈ being Element of F_Complex
for b₉ being sesquilinear-Form of b₁,b₂ holds b₉ . [(b₃ - (b₇ * b₄)),(b₅ - (b₈ * b₆))] = ((b₉ . [b₃,b₅]) - ((b₈ *' ) * (b₉ . [b₃,b₆]))) - ((b₇ * (b₉ . [b₄,b₅])) - (b₇ * ((b₈ *' ) * (b₉ . [b₄,b₆]))))

proof end;

theorem Th42: :: HERMITAN:42

for b₁ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex
for b₂ being cmplxhomogeneousFAF Form of b₁,b₁
for b₃ being Vector of b₁ holds b₂ . [b₃,(0. b₁)] = 0. F_Complex

proof end;

theorem Th43: :: HERMITAN:43

for b₁ being VectSp of F_Complex
for b₂, b₃ being Vector of b₁
for b₄ being hermitan-Form of b₁ holds (((b₄ . [b₂,b₃]) + (b₄ . [b₂,b₃])) + (b₄ . [b₂,b₃])) + (b₄ . [b₂,b₃]) = (((b₄ . [(b₂ + b₃),(b₂ + b₃)]) - (b₄ . [(b₂ - b₃),(b₂ - b₃)])) + (i_FC * (b₄ . [(b₂ + (i_FC * b₃)),(b₂ + (i_FC * b₃))]))) - (i_FC * (b₄ . [(b₂ - (i_FC * b₃)),(b₂ - (i_FC * b₃))]))

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Form of c₁,c₁;
let c₃ be Vector of c₁;
func signnorm c₂,c₃ -> real number equals :: HERMITAN:def 9
Re (a₂ . [a₃,a₃]);
coherence ;

end;

:: deftheorem Def9 defines signnorm HERMITAN:def 9 :

theorem Th44: :: HERMITAN:44

for b₁ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex
for b₂ being diagRvalued diagReR+0valued Form of b₁,b₁
for b₃ being Vector of b₁ holds
( |.(b₂ . [b₃,b₃]).| = Re (b₂ . [b₃,b₃]) & signnorm b₂,b₃ = |.(b₂ . [b₃,b₃]).| )

proof end;

theorem Th45: :: HERMITAN:45

for b₁ being VectSp of F_Complex
for b₂, b₃ being Vector of b₁
for b₄ being sesquilinear-Form of b₁,b₁
for b₅ being Real
for b₆ being Element of F_Complex st |.b₆.| = 1 & Re (b₆ * (b₄ . [b₃,b₂])) = |.(b₄ . [b₃,b₂]).| & Im (b₆ * (b₄ . [b₃,b₂])) = 0 holds
b₄ . [(b₂ - (([**b₅,0**] * b₆) * b₃)),(b₂ - (([**b₅,0**] * b₆) * b₃))] = (((b₄ . [b₂,b₂]) - ([**b₅,0**] * (b₆ * (b₄ . [b₃,b₂])))) - ([**b₅,0**] * ((b₆ *' ) * (b₄ . [b₂,b₃])))) + ([**(b₅ ^2 ),0**] * (b₄ . [b₃,b₃]))

proof end;

theorem Th46: :: HERMITAN:46

for b₁ being VectSp of F_Complex
for b₂, b₃ being Vector of b₁
for b₄ being diagReR+0valued hermitan-Form of b₁
for b₅ being Real
for b₆ being Element of F_Complex st |.b₆.| = 1 & Re (b₆ * (b₄ . [b₃,b₂])) = |.(b₄ . [b₃,b₂]).| & Im (b₆ * (b₄ . [b₃,b₂])) = 0 holds
( Re (b₄ . [(b₂ - (([**b₅,0**] * b₆) * b₃)),(b₂ - (([**b₅,0**] * b₆) * b₃))]) = ((signnorm b₄,b₂) - ((2 * |.(b₄ . [b₃,b₂]).|) * b₅)) + ((signnorm b₄,b₃) * (b₅ ^2 )) & 0 <= ((signnorm b₄,b₂) - ((2 * |.(b₄ . [b₃,b₂]).|) * b₅)) + ((signnorm b₄,b₃) * (b₅ ^2 )) )

proof end;

theorem Th47: :: HERMITAN:47

for b₁ being VectSp of F_Complex
for b₂, b₃ being Vector of b₁
for b₄ being diagReR+0valued hermitan-Form of b₁ st signnorm b₄,b₃ = 0 holds
|.(b₄ . [b₃,b₂]).| = 0

proof end;

theorem Th48: :: HERMITAN:48

for b₁ being VectSp of F_Complex
for b₂, b₃ being Vector of b₁
for b₄ being diagReR+0valued hermitan-Form of b₁ holds |.(b₄ . [b₂,b₃]).| ^2 <= (signnorm b₄,b₂) * (signnorm b₄,b₃)

proof end;

theorem Th49: :: HERMITAN:49

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃, b₄ being Vector of b₁ holds |.(b₂ . [b₃,b₄]).| ^2 <= |.(b₂ . [b₃,b₃]).| * |.(b₂ . [b₄,b₄]).|

proof end;

theorem Th50: :: HERMITAN:50

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃, b₄ being Vector of b₁ holds signnorm b₂,(b₃ + b₄) <= ((sqrt (signnorm b₂,b₃)) + (sqrt (signnorm b₂,b₄))) ^2

proof end;

theorem Th51: :: HERMITAN:51

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃, b₄ being Vector of b₁ holds |.(b₂ . [(b₃ + b₄),(b₃ + b₄)]).| <= ((sqrt |.(b₂ . [b₃,b₃]).|) + (sqrt |.(b₂ . [b₄,b₄]).|)) ^2

proof end;

theorem Th52: :: HERMITAN:52

for b₁ being VectSp of F_Complex
for b₂ being hermitan-Form of b₁
for b₃, b₄ being Element of b₁ holds (signnorm b₂,(b₃ + b₄)) + (signnorm b₂,(b₃ - b₄)) = (2 * (signnorm b₂,b₃)) + (2 * (signnorm b₂,b₄))

proof end;

theorem Th53: :: HERMITAN:53

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃, b₄ being Element of b₁ holds |.(b₂ . [(b₃ + b₄),(b₃ + b₄)]).| + |.(b₂ . [(b₃ - b₄),(b₃ - b₄)]).| = (2 * |.(b₂ . [b₃,b₃]).|) + (2 * |.(b₂ . [b₄,b₄]).|)

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Form of c₁,c₁;
func quasinorm c₂ -> RFunctional of a₁ means :Def10: :: HERMITAN:def 10
for b₁ being Element of a₁ holds a₃ . b₁ = sqrt (signnorm a₂,b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :

definition

let c₁ be VectSp of F_Complex ;
let c₂ be diagReR+0valued hermitan-Form of c₁;
redefine func quasinorm as quasinorm c₂ -> Semi-Norm of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex ;
let c₂ be cmplxhomogeneousFAF Form of c₁,c₁;
cluster diagker a₂ -> non empty ;
coherence

proof end;

end;

theorem Th54: :: HERMITAN:54

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds diagker b₂ is lineary-closed

proof end;

theorem Th55: :: HERMITAN:55

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds diagker b₂ = leftker b₂

proof end;

theorem Th56: :: HERMITAN:56

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds diagker b₂ = rightker b₂

proof end;

theorem Th57: :: HERMITAN:57

for b₁ being non empty VectSpStr of F_Complex
for b₂ being Form of b₁,b₁ holds diagker b₂ = diagker (b₂ *' )

proof end;

theorem Th58: :: HERMITAN:58

for b₁, b₂ being non empty VectSpStr of F_Complex
for b₃ being Form of b₁,b₂ holds
( leftker b₃ = leftker (b₃ *' ) & rightker b₃ = rightker (b₃ *' ) )

proof end;

theorem Th59: :: HERMITAN:59

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds LKer b₂ = RKer (b₂ *' )

proof end;

theorem Th60: :: HERMITAN:60

for b₁ being VectSp of F_Complex
for b₂ being diagRvalued diagReR+0valued Form of b₁,b₁
for b₃ being Vector of b₁ st Re (b₂ . [b₃,b₃]) = 0 holds
b₂ . [b₃,b₃] = 0. F_Complex

proof end;

theorem Th61: :: HERMITAN:61

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃ being Vector of b₁ st Re (b₂ . [b₃,b₃]) = 0 & ( not b₂ is degenerated-on-left or not b₂ is degenerated-on-right ) holds
b₃ = 0. b₁

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be VectSp of F_Complex ;
let c₃ be additiveFAF cmplxhomogeneousFAF Form of c₁,c₂;
func RQ*Form c₃ -> additiveFAF cmplxhomogeneousFAF Form of a₁,(VectQuot a₂,(RKer (a₃ *' ))) equals :: HERMITAN:def 11
(RQForm (a₃ *' )) *' ;
correctness ;

end;

:: deftheorem Def11 defines RQ*Form HERMITAN:def 11 :

theorem Th62: :: HERMITAN:62

for b₁ being non empty VectSpStr of F_Complex
for b₂ being VectSp of F_Complex
for b₃ being additiveFAF cmplxhomogeneousFAF Form of b₁,b₂
for b₄ being Vector of b₁
for b₅ being Vector of b₂ holds (RQ*Form b₃) . [b₄,(b₅ + (RKer (b₃ *' )))] = b₃ . [b₄,b₅]

proof end;

registration

let c₁, c₂ be VectSp of F_Complex ;
let c₃ be sesquilinear-Form of c₁,c₂;
cluster LQForm a₃ -> additiveFAF cmplxhomogeneousFAF ;
coherence

proof end;

cluster RQ*Form a₃ -> additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF ;
coherence

proof end;

end;

definition

let c₁, c₂ be VectSp of F_Complex ;
let c₃ be sesquilinear-Form of c₁,c₂;
func Q*Form c₃ -> sesquilinear-Form of (VectQuot a₁,(LKer a₃)),(VectQuot a₂,(RKer (a₃ *' ))) means :Def12: :: HERMITAN:def 12
for b₁ being Vector of (VectQuot a₁,(LKer a₃))
for b₂ being Vector of (VectQuot a₂,(RKer (a₃ *' )))
for b₃ being Vector of a₁
for b₄ being Vector of a₂ st b₁ = b₃ + (LKer a₃) & b₂ = b₄ + (RKer (a₃ *' )) holds
a₄ . [b₁,b₂] = a₃ . [b₃,b₄];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Q*Form HERMITAN:def 12 :

registration

let c₁, c₂ be non trivial VectSp of F_Complex ;
let c₃ be non constant sesquilinear-Form of c₁,c₂;
cluster Q*Form a₃ -> non constant ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed VectSpStr of F_Complex ;
let c₂ be VectSp of F_Complex ;
let c₃ be additiveFAF cmplxhomogeneousFAF Form of c₁,c₂;
cluster RQ*Form a₃ -> additiveFAF non degenerated-on-right cmplxhomogeneousFAF ;
coherence

proof end;

end;

theorem Th63: :: HERMITAN:63

for b₁ being non empty VectSpStr of F_Complex
for b₂ being VectSp of F_Complex
for b₃ being additiveFAF cmplxhomogeneousFAF Form of b₁,b₂ holds leftker b₃ = leftker (RQ*Form b₃)

proof end;

theorem Th64: :: HERMITAN:64

for b₁, b₂ being VectSp of F_Complex
for b₃ being sesquilinear-Form of b₁,b₂ holds RKer (b₃ *' ) = RKer ((LQForm b₃) *' )

proof end;

theorem Th65: :: HERMITAN:65

for b₁, b₂ being VectSp of F_Complex
for b₃ being sesquilinear-Form of b₁,b₂ holds LKer b₃ = LKer (RQ*Form b₃)

proof end;

theorem Th66: :: HERMITAN:66

for b₁, b₂ being VectSp of F_Complex
for b₃ being sesquilinear-Form of b₁,b₂ holds
( Q*Form b₃ = RQ*Form (LQForm b₃) & Q*Form b₃ = LQForm (RQ*Form b₃) )

proof end;

theorem Th67: :: HERMITAN:67

for b₁, b₂ being VectSp of F_Complex
for b₃ being sesquilinear-Form of b₁,b₂ holds
( leftker (Q*Form b₃) = leftker (RQ*Form (LQForm b₃)) & rightker (Q*Form b₃) = rightker (RQ*Form (LQForm b₃)) & leftker (Q*Form b₃) = leftker (LQForm (RQ*Form b₃)) & rightker (Q*Form b₃) = rightker (LQForm (RQ*Form b₃)) )

proof end;

registration

let c₁, c₂ be VectSp of F_Complex ;
let c₃ be sesquilinear-Form of c₁,c₂;
cluster RQ*Form (LQForm a₃) -> additiveFAF additiveSAF homogeneousSAF non degenerated-on-left non degenerated-on-right cmplxhomogeneousFAF ;
coherence

proof end;

cluster LQForm (RQ*Form a₃) -> additiveFAF non degenerated-on-left non degenerated-on-right cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let c₁, c₂ be VectSp of F_Complex ;
let c₃ be sesquilinear-Form of c₁,c₂;
cluster Q*Form a₃ -> non degenerated-on-left non degenerated-on-right ;
coherence

proof end;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Form of c₁,c₁;
attr a₂ is positivediagvalued means :Def13: :: HERMITAN:def 13
for b₁ being Vector of a₁ st b₁ <> 0. a₁ holds
0 < Re (a₂ . [b₁,b₁]);

end;

:: deftheorem Def13 defines positivediagvalued HERMITAN:def 13 :

registration

let c₁ be non empty right_zeroed VectSpStr of F_Complex ;
cluster additiveSAF positivediagvalued -> diagReR+0valued Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed VectSpStr of F_Complex ;
cluster additiveFAF positivediagvalued -> diagReR+0valued Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of F_Complex ;
coherence

proof end;

end;

definition

let c₁ be VectSp of F_Complex ;
let c₂ be diagReR+0valued hermitan-Form of c₁;
func ScalarForm c₂ -> diagReR+0valued hermitan-Form of (VectQuot a₁,(LKer a₂)) equals :: HERMITAN:def 14
Q*Form a₂;
coherence

proof end;

end;

:: deftheorem Def14 defines ScalarForm HERMITAN:def 14 :

theorem Th68: :: HERMITAN:68

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁
for b₃, b₄ being Vector of (VectQuot b₁,(LKer b₂))
for b₅, b₆ being Vector of b₁ st b₃ = b₅ + (LKer b₂) & b₄ = b₆ + (LKer b₂) holds
(ScalarForm b₂) . [b₃,b₄] = b₂ . [b₅,b₆]

proof end;

theorem Th69: :: HERMITAN:69

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds leftker (ScalarForm b₂) = leftker (Q*Form b₂)

proof end;

theorem Th70: :: HERMITAN:70

for b₁ being VectSp of F_Complex
for b₂ being diagReR+0valued hermitan-Form of b₁ holds rightker (ScalarForm b₂) = rightker (Q*Form b₂) by Th59;

registration

let c₁ be VectSp of F_Complex ;
let c₂ be diagReR+0valued hermitan-Form of c₁;
cluster ScalarForm a₂ -> non degenerated-on-left non degenerated-on-right diagReR+0valued positivediagvalued ;
coherence

proof end;

end;

registration

let c₁ be non trivial VectSp of F_Complex ;
let c₂ be non constant diagReR+0valued hermitan-Form of c₁;
cluster ScalarForm a₂ -> non constant non degenerated-on-left non degenerated-on-right diagReR+0valued positivediagvalued ;
coherence ;

end;