environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, COMSEQ_1, FUNCT_2, TARSKI, RSSPACE, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, COMPLEX1, FUNCOP_1, RLVECT_1, CLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, RLSUB_1, REALSET1, SERIES_1, CARD_1, XXREAL_0, REAL_1, SQUARE_1, BHSP_1, PRE_TOPC, PROB_2, XCMPLX_0, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, CARD_3, SEQ_2, ORDINAL2, CSSPACE, CLOPBAN1, CFUNCDOM;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, RELAT_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_1, BINOP_1, REALSET1, XCMPLX_0, XXREAL_0, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, ZFMISC_1, NUMBERS, SQUARE_1, XREAL_0, COMPLEX1, COMSEQ_1, COMSEQ_2, SERIES_1, COMSEQ_3, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, CLVECT_1, CFUNCDOM;
definitions TARSKI, FUNCT_2, RLVECT_1, CLVECT_1, STRUCT_0, ALGSTR_0, VALUED_0;
theorems XBOOLE_0, RELAT_1, SQUARE_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SERIES_1, COMSEQ_3, FUNCT_1, FUNCT_2, RLVECT_1, XCMPLX_0, COMSEQ_1, CLVECT_1, COMPLEX1, COMSEQ_2, NORMSP_1, FUNCOP_1, XREAL_1, XXREAL_0, BHSP_1, ALGSTR_0, VALUED_1, ORDINAL1, CFUNCDOM;
schemes NAT_1, BINOP_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1, ALGSTR_0, VALUED_1, VALUED_0, VFUNCT_1, SERIES_1, XREAL_0, SQUARE_1, CFUNCDOM;
constructors HIDDEN, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3, REALSET1, BHSP_1, CLVECT_1, RELSET_1, VFUNCT_1, CFUNCDOM, FUNCSDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities CLVECT_1, STRUCT_0, REALSET1, SQUARE_1, BINOP_1, ALGSTR_0, CFUNCDOM, ORDINAL1;
expansions RLVECT_1, CLVECT_1, BINOP_1, VALUED_0;
Lm1:
|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable
deffunc H1( CUNITSTR ) -> Element of the carrier of $1 = 0. $1;
set V0 = the ComplexLinearSpace;
Lm2:
the carrier of ((0). the ComplexLinearSpace) = {(0. the ComplexLinearSpace)}
by CLVECT_1:def 9;
reconsider nilfunc = [: the carrier of ((0). the ComplexLinearSpace), the carrier of ((0). the ComplexLinearSpace):] --> 0c as Function of [: the carrier of ((0). the ComplexLinearSpace), the carrier of ((0). the ComplexLinearSpace):],COMPLEX ;
Lm3:
for x, y being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [x,y] = 0c
by FUNCOP_1:7;
0. the ComplexLinearSpace in the carrier of ((0). the ComplexLinearSpace)
by Lm2, TARSKI:def 1;
then Lm4:
nilfunc . [(0. the ComplexLinearSpace),(0. the ComplexLinearSpace)] = 0c
by Lm3;
Lm5:
for u being VECTOR of ((0). the ComplexLinearSpace) holds
( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 )
by COMPLEX1:4, FUNCOP_1:7;
Lm6:
for u, v being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [u,v] = (nilfunc . [v,u]) *'
Lm7:
for u, v, w being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm8:
for u, v being VECTOR of ((0). the ComplexLinearSpace)
for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
set X0 = CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #);
Lm9:
now for x, y, z being Point of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)
for a being Complex holds
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let x,
y,
z be
Point of
CUNITSTR(# the
carrier of
((0). the ComplexLinearSpace),
(0. ((0). the ComplexLinearSpace)), the
addF of
((0). the ComplexLinearSpace), the
Mult of
((0). the ComplexLinearSpace),
nilfunc #);
for a being Complex holds
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Complex;
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
H1(
CUNITSTR(# the
carrier of
((0). the ComplexLinearSpace),
(0. ((0). the ComplexLinearSpace)), the
addF of
((0). the ComplexLinearSpace), the
Mult of
((0). the ComplexLinearSpace),
nilfunc #))
= 0. the
ComplexLinearSpace
by CLVECT_1:30;
hence
(
x .|. x = 0c iff
x = H1(
CUNITSTR(# the
carrier of
((0). the ComplexLinearSpace),
(0. ((0). the ComplexLinearSpace)), the
addF of
((0). the ComplexLinearSpace), the
Mult of
((0). the ComplexLinearSpace),
nilfunc #)) )
by Lm2, Lm3, TARSKI:def 1;
( 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(
0 <= Re (x .|. x) &
0 = Im (x .|. x) )
by Lm5;
( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = (y .|. x) *'
by Lm6;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
(a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
verum
end;
Lm10:
for X being ComplexUnitarySpace
for p, q being Complex
for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y))
definition
existence
ex b1 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *'))
uniqueness
for b1, b2 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st ( for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) & ( for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b2 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) holds
b1 = b2
end;