begin
definition
existence
ex b1 being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st
for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds
b1 . (z,x) = (C_id z) (#) (seq_id x)
uniqueness
for b1, b2 being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds
b1 . (z,x) = (C_id z) (#) (seq_id x) ) & ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds
b2 . (z,x) = (C_id z) (#) (seq_id x) ) holds
b1 = b2
end;
begin
deffunc H1( CUNITSTR ) -> Element of the carrier of $1 = 0. $1;
set V0 = the ComplexLinearSpace;
Lm1:
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 ;
Lm2:
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 Lm1, TARSKI:def 1;
then Lm3:
nilfunc . [(0. the ComplexLinearSpace),(0. the ComplexLinearSpace)] = 0c
by Lm2;
Lm4:
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;
Lm5:
for u, v being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [u,v] = (nilfunc . [v,u]) *'
Lm6:
for u, v, w being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm7:
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 #);
Lm8:
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 Lm1, Lm2, 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 Lm4;
( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = (y .|. x) *'
by Lm5;
( (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;
Lm9:
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))
begin
definition
existence
ex b1 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st
for x, y being set 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 set 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 set 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;