:: CSSPACE semantic presentation

definition
func the_set_of_ComplexSequences -> non empty set means :Def1: :: CSSPACE:def 1
for b1 being set holds
( b1 in a1 iff b1 is Complex_Sequence );
existence
ex b1 being non empty set st
for b2 being set holds
( b2 in b1 iff b2 is Complex_Sequence )
proof end;
uniqueness
for b1, b2 being non empty set st ( for b3 being set holds
( b3 in b1 iff b3 is Complex_Sequence ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is Complex_Sequence ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :
for b1 being non empty set holds
( b1 = the_set_of_ComplexSequences iff for b2 being set holds
( b2 in b1 iff b2 is Complex_Sequence ) );

definition
let c1 be set ;
assume E2: c1 in the_set_of_ComplexSequences ;
func seq_id c1 -> Complex_Sequence equals :Def2: :: CSSPACE:def 2
a1;
coherence
c1 is Complex_Sequence
by E2, Def1;
end;

:: deftheorem Def2 defines seq_id CSSPACE:def 2 :
for b1 being set st b1 in the_set_of_ComplexSequences holds
seq_id b1 = b1;

definition
let c1 be set ;
assume E3: c1 in COMPLEX ;
func C_id c1 -> Complex equals :Def3: :: CSSPACE:def 3
a1;
coherence
c1 is Complex
by E3;
end;

:: deftheorem Def3 defines C_id CSSPACE:def 3 :
for b1 being set st b1 in COMPLEX holds
C_id b1 = b1;

theorem Th1: :: CSSPACE:1
ex b1 being BinOp of the_set_of_ComplexSequences st
( ( for b2, b3 being Element of the_set_of_ComplexSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3) ) & b1 is commutative & b1 is associative )
proof end;

theorem Th2: :: CSSPACE:2
ex b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st
for b2, b3 being set st b2 in COMPLEX & b3 in the_set_of_ComplexSequences holds
b1 . [b2,b3] = (C_id b2) (#) (seq_id b3)
proof end;

definition
func l_add -> BinOp of the_set_of_ComplexSequences means :Def4: :: CSSPACE:def 4
for b1, b2 being Element of the_set_of_ComplexSequences holds a1 . b1,b2 = (seq_id b1) + (seq_id b2);
existence
ex b1 being BinOp of the_set_of_ComplexSequences st
for b2, b3 being Element of the_set_of_ComplexSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3)
by Th1;
uniqueness
for b1, b2 being BinOp of the_set_of_ComplexSequences st ( for b3, b4 being Element of the_set_of_ComplexSequences holds b1 . b3,b4 = (seq_id b3) + (seq_id b4) ) & ( for b3, b4 being Element of the_set_of_ComplexSequences holds b2 . b3,b4 = (seq_id b3) + (seq_id b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines l_add CSSPACE:def 4 :
for b1 being BinOp of the_set_of_ComplexSequences holds
( b1 = l_add iff for b2, b3 being Element of the_set_of_ComplexSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3) );

definition
func l_mult -> Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences means :Def5: :: CSSPACE:def 5
for b1, b2 being set st b1 in COMPLEX & b2 in the_set_of_ComplexSequences holds
a1 . [b1,b2] = (C_id b1) (#) (seq_id b2);
existence
ex b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st
for b2, b3 being set st b2 in COMPLEX & b3 in the_set_of_ComplexSequences holds
b1 . [b2,b3] = (C_id b2) (#) (seq_id b3)
by Th2;
uniqueness
for b1, b2 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st ( for b3, b4 being set st b3 in COMPLEX & b4 in the_set_of_ComplexSequences holds
b1 . [b3,b4] = (C_id b3) (#) (seq_id b4) ) & ( for b3, b4 being set st b3 in COMPLEX & b4 in the_set_of_ComplexSequences holds
b2 . [b3,b4] = (C_id b3) (#) (seq_id b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines l_mult CSSPACE:def 5 :
for b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences holds
( b1 = l_mult iff for b2, b3 being set st b2 in COMPLEX & b3 in the_set_of_ComplexSequences holds
b1 . [b2,b3] = (C_id b2) (#) (seq_id b3) );

definition
func CZeroseq -> Element of the_set_of_ComplexSequences means :Def6: :: CSSPACE:def 6
for b1 being Nat holds (seq_id a1) . b1 = 0c ;
existence
ex b1 being Element of the_set_of_ComplexSequences st
for b2 being Nat holds (seq_id b1) . b2 = 0c
proof end;
uniqueness
for b1, b2 being Element of the_set_of_ComplexSequences st ( for b3 being Nat holds (seq_id b1) . b3 = 0c ) & ( for b3 being Nat holds (seq_id b2) . b3 = 0c ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :
for b1 being Element of the_set_of_ComplexSequences holds
( b1 = CZeroseq iff for b2 being Nat holds (seq_id b1) . b2 = 0c );

theorem Th3: :: CSSPACE:3
for b1 being Complex_Sequence holds seq_id b1 = b1
proof end;

theorem Th4: :: CSSPACE:4
for b1, b2 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 + b2 = (seq_id b1) + (seq_id b2)
proof end;

theorem Th5: :: CSSPACE:5
for b1 being Complex
for b2 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 * b2 = b1 (#) (seq_id b2)
proof end;

registration
cluster CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) -> Abelian ;
coherence
CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) is Abelian
proof end;
end;

Lemma12: for b1, b2 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 + b2 = b2 + b1
;

theorem Th6: :: CSSPACE:6
for b1, b2, b3 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b1 + b2) + b3 = b1 + (b2 + b3)
proof end;

theorem Th7: :: CSSPACE:7
for b1 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 + (0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)) = b1
proof end;

theorem Th8: :: CSSPACE:8
for b1 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) ex b2 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) st b1 + b2 = 0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)
proof end;

theorem Th9: :: CSSPACE:9
for b1 being Complex
for b2, b3 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3)
proof end;

theorem Th10: :: CSSPACE:10
for b1, b2 being Complex
for b3 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3)
proof end;

theorem Th11: :: CSSPACE:11
for b1, b2 being Complex
for b3 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b1 * b2) * b3 = b1 * (b2 * b3)
proof end;

theorem Th12: :: CSSPACE:12
for b1 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds 1r * b1 = b1
proof end;

definition
func Linear_Space_of_ComplexSequences -> ComplexLinearSpace equals :: CSSPACE:def 7
CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #);
correctness
coherence
CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) is ComplexLinearSpace
;
by Lemma12, Th6, Th7, Th8, Th9, Th10, Th11, Th12, CLVECT_1:1;
end;

:: deftheorem Def7 defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :
Linear_Space_of_ComplexSequences = CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #);

definition
let c1 be ComplexLinearSpace;
let c2 be Subset of c1;
assume E20: ( c2 is lineary-closed & not c2 is empty ) ;
func Add_ c2,c1 -> BinOp of a2 equals :Def8: :: CSSPACE:def 8
the add of a1 || a2;
correctness
coherence
the add of c1 || c2 is BinOp of c2
;
proof end;
end;

:: deftheorem Def8 defines Add_ CSSPACE:def 8 :
for b1 being ComplexLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Add_ b2,b1 = the add of b1 || b2;

definition
let c1 be ComplexLinearSpace;
let c2 be Subset of c1;
assume E21: ( c2 is lineary-closed & not c2 is empty ) ;
func Mult_ c2,c1 -> Function of [:COMPLEX ,a2:],a2 equals :Def9: :: CSSPACE:def 9
the Mult of a1 | [:COMPLEX ,a2:];
correctness
coherence
the Mult of c1 | [:COMPLEX ,c2:] is Function of [:COMPLEX ,c2:],c2
;
proof end;
end;

:: deftheorem Def9 defines Mult_ CSSPACE:def 9 :
for b1 being ComplexLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Mult_ b2,b1 = the Mult of b1 | [:COMPLEX ,b2:];

definition
let c1 be ComplexLinearSpace;
let c2 be Subset of c1;
assume E22: ( c2 is lineary-closed & not c2 is empty ) ;
func Zero_ c2,c1 -> Element of a2 equals :Def10: :: CSSPACE:def 10
0. a1;
correctness
coherence
0. c1 is Element of c2
;
proof end;
end;

:: deftheorem Def10 defines Zero_ CSSPACE:def 10 :
for b1 being ComplexLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Zero_ b2,b1 = 0. b1;

theorem Th13: :: CSSPACE:13
for b1 being ComplexLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
CLSStruct(# b2,(Zero_ b2,b1),(Add_ b2,b1),(Mult_ b2,b1) #) is Subspace of b1
proof end;

definition
func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def11: :: CSSPACE:def 11
( not a1 is empty & ( for b1 being set holds
( b1 in a1 iff ( b1 in the_set_of_ComplexSequences & |.(seq_id b1).| (#) |.(seq_id b1).| is summable ) ) ) );
existence
ex b1 being Subset of Linear_Space_of_ComplexSequences st
( not b1 is empty & ( for b2 being set holds
( b2 in b1 iff ( b2 in the_set_of_ComplexSequences & |.(seq_id b2).| (#) |.(seq_id b2).| is summable ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_ComplexSequences st not b1 is empty & ( for b3 being set holds
( b3 in b1 iff ( b3 in the_set_of_ComplexSequences & |.(seq_id b3).| (#) |.(seq_id b3).| is summable ) ) ) & not b2 is empty & ( for b3 being set holds
( b3 in b2 iff ( b3 in the_set_of_ComplexSequences & |.(seq_id b3).| (#) |.(seq_id b3).| is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_l2ComplexSequences iff ( not b1 is empty & ( for b2 being set holds
( b2 in b1 iff ( b2 in the_set_of_ComplexSequences & |.(seq_id b2).| (#) |.(seq_id b2).| is summable ) ) ) ) );

theorem Th14: :: CSSPACE:14
( the_set_of_l2ComplexSequences is lineary-closed & not the_set_of_l2ComplexSequences is empty )
proof end;

theorem Th15: :: CSSPACE:15
CLSStruct(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Subspace of Linear_Space_of_ComplexSequences by Th13, Th14;

theorem Th16: :: CSSPACE:16
CLSStruct(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is ComplexLinearSpace by Th13, Th14;

theorem Th17: :: CSSPACE:17
( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( for b1 being set holds
( b1 is Element of Linear_Space_of_ComplexSequences iff b1 is Complex_Sequence ) ) & ( for b1 being set holds
( b1 is VECTOR of Linear_Space_of_ComplexSequences iff b1 is Complex_Sequence ) ) & ( for b1 being VECTOR of Linear_Space_of_ComplexSequences holds b1 = seq_id b1 ) & ( for b1, b2 being VECTOR of Linear_Space_of_ComplexSequences holds b1 + b2 = (seq_id b1) + (seq_id b2) ) & ( for b1 being Complex
for b2 being VECTOR of Linear_Space_of_ComplexSequences holds b1 * b2 = b1 (#) (seq_id b2) ) ) by Def1, Def2, Th4, Th5;

definition
attr a1 is strict;
struct CUNITSTR -> CLSStruct ;
aggr CUNITSTR(# carrier, Zero, add, Mult, scalar #) -> CUNITSTR ;
sel scalar c1 -> Function of [:the carrier of a1,the carrier of a1:], COMPLEX ;
end;

registration
cluster non empty strict CUNITSTR ;
existence
ex b1 being CUNITSTR st
( not b1 is empty & b1 is strict )
proof end;
end;

registration
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
let c4 be Function of [:COMPLEX ,c1:],c1;
let c5 be Function of [:c1,c1:], COMPLEX ;
cluster CUNITSTR(# a1,a2,a3,a4,a5 #) -> non empty ;
coherence
not CUNITSTR(# c1,c2,c3,c4,c5 #) is empty
proof end;
end;

deffunc H1( CUNITSTR ) -> Element of the carrier of a1 = 0. a1;

definition
let c1 be non empty CUNITSTR ;
let c2, c3 be Point of c1;
func c2 .|. c3 -> Complex equals :: CSSPACE:def 12
the scalar of a1 . [a2,a3];
correctness
coherence
the scalar of c1 . [c2,c3] is Complex
;
;
end;

:: deftheorem Def12 defines .|. CSSPACE:def 12 :
for b1 being non empty CUNITSTR
for b2, b3 being Point of b1 holds b2 .|. b3 = the scalar of b1 . [b2,b3];

consider c1 being ComplexLinearSpace;

Lemma27: the carrier of ((0). c1) = {(0. c1)}
by CLVECT_1:def 5;

reconsider c2 = [:the carrier of ((0). c1),the carrier of ((0). c1):] --> 0c as Function of [:the carrier of ((0). c1),the carrier of ((0). c1):], COMPLEX by FUNCOP_1:57;

Lemma28: for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = 0c
by FUNCOP_1:13;

0. c1 in the carrier of ((0). c1)
by Lemma27, TARSKI:def 1;

then Lemma29: c2 . [(0. c1),(0. c1)] = 0c
by Lemma28;

Lemma30: for b1 being VECTOR of ((0). c1) holds
( 0 <= Re (c2 . [b1,b1]) & Im (c2 . [b1,b1]) = 0 )
proof end;

Lemma31: for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = (c2 . [b2,b1]) *'
proof end;

Lemma32: for b1, b2, b3 being VECTOR of ((0). c1) holds c2 . [(b1 + b2),b3] = (c2 . [b1,b3]) + (c2 . [b2,b3])
proof end;

Lemma33: for b1, b2 being VECTOR of ((0). c1)
for b3 being Complex holds c2 . [(b3 * b1),b2] = b3 * (c2 . [b1,b2])
proof end;

set c3 = CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);

E34: now
let c4, c5, c6 be Point of CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
let c7 be Complex;
thus ( c4 .|. c4 = 0c iff c4 = H1( CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) )
proof
H1( CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) = the Zero of CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)
.= 0. ((0). c1)
.= 0. c1 by CLVECT_1:31 ;
hence ( c4 .|. c4 = 0c iff c4 = H1( CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) ) by Lemma27, Lemma29, TARSKI:def 1;
end;
thus ( 0 <= Re (c4 .|. c4) & 0 = Im (c4 .|. c4) ) by Lemma30;
thus c4 .|. c5 = (c5 .|. c4) *' by Lemma31;
thus (c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6)
proof
reconsider c8 = c4, c9 = c5, c10 = c6 as VECTOR of ((0). c1) ;
( (c4 + c5) .|. c6 = c2 . [(c8 + c9),c10] & c4 .|. c6 = c2 . [c8,c10] & c5 .|. c6 = c2 . [c9,c10] ) ;
hence (c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6) by Lemma32;
end;
thus (c7 * c4) .|. c5 = c7 * (c4 .|. c5)
proof
reconsider c8 = c4, c9 = c5 as VECTOR of ((0). c1) ;
( (c7 * c4) .|. c5 = c2 . [(c7 * c8),c9] & c4 .|. c5 = c2 . [c8,c9] ) ;
hence (c7 * c4) .|. c5 = c7 * (c4 .|. c5) by Lemma33;
end;
end;

definition
let c4 be non empty CUNITSTR ;
attr a1 is ComplexUnitarySpace-like means :Def13: :: CSSPACE:def 13
for b1, b2, b3 being Point of a1
for b4 being Complex holds
( ( b1 .|. b1 = 0 implies b1 = 0. a1 ) & ( b1 = 0. a1 implies b1 .|. b1 = 0 ) & 0 <= Re (b1 .|. b1) & 0 = Im (b1 .|. b1) & b1 .|. b2 = (b2 .|. b1) *' & (b1 + b2) .|. b3 = (b1 .|. b3) + (b2 .|. b3) & (b4 * b1) .|. b2 = b4 * (b1 .|. b2) );
end;

:: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def 13 :
for b1 being non empty CUNITSTR holds
( b1 is ComplexUnitarySpace-like iff for b2, b3, b4 being Point of b1
for b5 being Complex holds
( ( b2 .|. b2 = 0 implies b2 = 0. b1 ) & ( b2 = 0. b1 implies b2 .|. b2 = 0 ) & 0 <= Re (b2 .|. b2) & 0 = Im (b2 .|. b2) & b2 .|. b3 = (b3 .|. b2) *' & (b2 + b3) .|. b4 = (b2 .|. b4) + (b3 .|. b4) & (b5 * b2) .|. b3 = b5 * (b2 .|. b3) ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like strict ComplexUnitarySpace-like CUNITSTR ;
existence
ex b1 being non empty CUNITSTR st
( b1 is ComplexUnitarySpace-like & b1 is ComplexLinearSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
mode ComplexUnitarySpace is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexUnitarySpace-like CUNITSTR ;
end;

theorem Th18: :: CSSPACE:18
for b1 being ComplexUnitarySpace holds (0. b1) .|. (0. b1) = 0 by Def13;

theorem Th19: :: CSSPACE:19
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds b2 .|. (b3 + b4) = (b2 .|. b3) + (b2 .|. b4)
proof end;

theorem Th20: :: CSSPACE:20
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3, b4 being Point of b2 holds b3 .|. (b1 * b4) = (b1 *' ) * (b3 .|. b4)
proof end;

theorem Th21: :: CSSPACE:21
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3, b4 being Point of b2 holds (b1 * b3) .|. b4 = b3 .|. ((b1 *' ) * b4)
proof end;

theorem Th22: :: CSSPACE:22
for b1, b2 being Complex
for b3 being ComplexUnitarySpace
for b4, b5, b6 being Point of b3 holds ((b1 * b4) + (b2 * b5)) .|. b6 = (b1 * (b4 .|. b6)) + (b2 * (b5 .|. b6))
proof end;

theorem Th23: :: CSSPACE:23
for b1, b2 being Complex
for b3 being ComplexUnitarySpace
for b4, b5, b6 being Point of b3 holds b4 .|. ((b1 * b5) + (b2 * b6)) = ((b1 *' ) * (b4 .|. b5)) + ((b2 *' ) * (b4 .|. b6))
proof end;

theorem Th24: :: CSSPACE:24
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. b3 = b2 .|. (- b3)
proof end;

theorem Th25: :: CSSPACE:25
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. b3 = - (b2 .|. b3)
proof end;

theorem Th26: :: CSSPACE:26
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds b2 .|. (- b3) = - (b2 .|. b3)
proof end;

theorem Th27: :: CSSPACE:27
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. (- b3) = b2 .|. b3
proof end;

theorem Th28: :: CSSPACE:28
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds (b2 - b3) .|. b4 = (b2 .|. b4) - (b3 .|. b4)
proof end;

theorem Th29: :: CSSPACE:29
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds b2 .|. (b3 - b4) = (b2 .|. b3) - (b2 .|. b4)
proof end;

theorem Th30: :: CSSPACE:30
for b1 being ComplexUnitarySpace
for b2, b3, b4, b5 being Point of b1 holds (b2 - b3) .|. (b4 - b5) = (((b2 .|. b4) - (b2 .|. b5)) - (b3 .|. b4)) + (b3 .|. b5)
proof end;

theorem Th31: :: CSSPACE:31
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds (0. b1) .|. b2 = 0
proof end;

theorem Th32: :: CSSPACE:32
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds b2 .|. (0. b1) = 0
proof end;

theorem Th33: :: CSSPACE:33
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (b2 + b3) .|. (b2 + b3) = (((b2 .|. b2) + (b2 .|. b3)) + (b3 .|. b2)) + (b3 .|. b3)
proof end;

theorem Th34: :: CSSPACE:34
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (b2 + b3) .|. (b2 - b3) = (((b2 .|. b2) - (b2 .|. b3)) + (b3 .|. b2)) - (b3 .|. b3)
proof end;

theorem Th35: :: CSSPACE:35
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds (b2 - b3) .|. (b2 - b3) = (((b2 .|. b2) - (b2 .|. b3)) - (b3 .|. b2)) + (b3 .|. b3)
proof end;

Lemma51: for b1 being ComplexUnitarySpace
for b2, b3 being Complex
for b4, b5 being Point of b1 holds ((b2 * b4) + (b3 * b5)) .|. ((b2 * b4) + (b3 * b5)) = ((((b2 * (b2 *' )) * (b4 .|. b4)) + ((b2 * (b3 *' )) * (b4 .|. b5))) + (((b2 *' ) * b3) * (b5 .|. b4))) + ((b3 * (b3 *' )) * (b5 .|. b5))
proof end;

theorem Th36: :: CSSPACE:36
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds |.(b2 .|. b2).| = Re (b2 .|. b2)
proof end;

theorem Th37: :: CSSPACE:37
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds |.(b2 .|. b3).| <= (sqrt |.(b2 .|. b2).|) * (sqrt |.(b3 .|. b3).|)
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5, c6 be Point of c4;
pred c2,c3 are_orthogonal means :Def14: :: CSSPACE:def 14
a2 .|. a3 = 0;
symmetry
for b1, b2 being Point of c4 st b1 .|. b2 = 0 holds
b2 .|. b1 = 0
by Def13, COMPLEX1:113;
end;

:: deftheorem Def14 defines are_orthogonal CSSPACE:def 14 :
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds
( b2,b3 are_orthogonal iff b2 .|. b3 = 0 );

theorem Th38: :: CSSPACE:38
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 st b2,b3 are_orthogonal holds
b2, - b3 are_orthogonal
proof end;

theorem Th39: :: CSSPACE:39
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 st b2,b3 are_orthogonal holds
- b2,b3 are_orthogonal
proof end;

theorem Th40: :: CSSPACE:40
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 st b2,b3 are_orthogonal holds
- b2, - b3 are_orthogonal
proof end;

theorem Th41: :: CSSPACE:41
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds b2, 0. b1 are_orthogonal
proof end;

theorem Th42: :: CSSPACE:42
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 st b2,b3 are_orthogonal holds
(b2 + b3) .|. (b2 + b3) = (b2 .|. b2) + (b3 .|. b3)
proof end;

theorem Th43: :: CSSPACE:43
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 st b2,b3 are_orthogonal holds
(b2 - b3) .|. (b2 - b3) = (b2 .|. b2) + (b3 .|. b3)
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5 be Point of c4;
func ||.c2.|| -> Real equals :: CSSPACE:def 15
sqrt |.(a2 .|. a2).|;
correctness
coherence
sqrt |.(c5 .|. c5).| is Real
;
;
end;

:: deftheorem Def15 defines ||. CSSPACE:def 15 :
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds ||.b2.|| = sqrt |.(b2 .|. b2).|;

theorem Th44: :: CSSPACE:44
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds
( ||.b2.|| = 0 iff b2 = 0. b1 )
proof end;

theorem Th45: :: CSSPACE:45
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3 being Point of b2 holds ||.(b1 * b3).|| = |.b1.| * ||.b3.||
proof end;

theorem Th46: :: CSSPACE:46
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds 0 <= ||.b2.||
proof end;

theorem Th47: :: CSSPACE:47
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds |.(b2 .|. b3).| <= ||.b2.|| * ||.b3.|| by Th37;

theorem Th48: :: CSSPACE:48
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds ||.(b2 + b3).|| <= ||.b2.|| + ||.b3.||
proof end;

theorem Th49: :: CSSPACE:49
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds ||.(- b2).|| = ||.b2.||
proof end;

theorem Th50: :: CSSPACE:50
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds ||.b2.|| - ||.b3.|| <= ||.(b2 - b3).||
proof end;

theorem Th51: :: CSSPACE:51
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds abs (||.b2.|| - ||.b3.||) <= ||.(b2 - b3).||
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5, c6 be Point of c4;
func dist c2,c3 -> Real equals :: CSSPACE:def 16
||.(a2 - a3).||;
correctness
coherence
||.(c5 - c6).|| is Real
;
;
end;

:: deftheorem Def16 defines dist CSSPACE:def 16 :
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds dist b2,b3 = ||.(b2 - b3).||;

theorem Th52: :: CSSPACE:52
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds dist b2,b3 = dist b3,b2
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5, c6 be Point of c4;
redefine func dist as dist c2,c3 -> Real;
commutativity
for b1, b2 being Point of c4 holds dist b1,b2 = dist b2,b1
by Th52;
end;

theorem Th53: :: CSSPACE:53
for b1 being ComplexUnitarySpace
for b2 being Point of b1 holds dist b2,b2 = 0
proof end;

theorem Th54: :: CSSPACE:54
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds dist b2,b3 <= (dist b2,b4) + (dist b4,b3)
proof end;

theorem Th55: :: CSSPACE:55
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds
( b2 <> b3 iff dist b2,b3 <> 0 )
proof end;

theorem Th56: :: CSSPACE:56
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds dist b2,b3 >= 0 by Th46;

theorem Th57: :: CSSPACE:57
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds
( b2 <> b3 iff dist b2,b3 > 0 )
proof end;

theorem Th58: :: CSSPACE:58
for b1 being ComplexUnitarySpace
for b2, b3 being Point of b1 holds dist b2,b3 = sqrt |.((b2 - b3) .|. (b2 - b3)).| ;

theorem Th59: :: CSSPACE:59
for b1 being ComplexUnitarySpace
for b2, b3, b4, b5 being Point of b1 holds dist (b2 + b3),(b4 + b5) <= (dist b2,b4) + (dist b3,b5)
proof end;

theorem Th60: :: CSSPACE:60
for b1 being ComplexUnitarySpace
for b2, b3, b4, b5 being Point of b1 holds dist (b2 - b3),(b4 - b5) <= (dist b2,b4) + (dist b3,b5)
proof end;

theorem Th61: :: CSSPACE:61
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds dist (b2 - b3),(b4 - b3) = dist b2,b4
proof end;

theorem Th62: :: CSSPACE:62
for b1 being ComplexUnitarySpace
for b2, b3, b4 being Point of b1 holds dist (b2 - b3),(b4 - b3) <= (dist b3,b2) + (dist b3,b4)
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5 be sequence of c4;
func - c2 -> sequence of a1 means :Def17: :: CSSPACE:def 17
for b1 being Nat holds a3 . b1 = - (a2 . b1);
existence
ex b1 being sequence of c4 st
for b2 being Nat holds b1 . b2 = - (c5 . b2)
proof end;
uniqueness
for b1, b2 being sequence of c4 st ( for b3 being Nat holds b1 . b3 = - (c5 . b3) ) & ( for b3 being Nat holds b2 . b3 = - (c5 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines - CSSPACE:def 17 :
for b1 being ComplexUnitarySpace
for b2, b3 being sequence of b1 holds
( b3 = - b2 iff for b4 being Nat holds b3 . b4 = - (b2 . b4) );

definition
let c4 be ComplexUnitarySpace;
let c5 be sequence of c4;
let c6 be Point of c4;
func c2 + c3 -> sequence of a1 means :Def18: :: CSSPACE:def 18
for b1 being Nat holds a4 . b1 = (a2 . b1) + a3;
existence
ex b1 being sequence of c4 st
for b2 being Nat holds b1 . b2 = (c5 . b2) + c6
proof end;
uniqueness
for b1, b2 being sequence of c4 st ( for b3 being Nat holds b1 . b3 = (c5 . b3) + c6 ) & ( for b3 being Nat holds b2 . b3 = (c5 . b3) + c6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines + CSSPACE:def 18 :
for b1 being ComplexUnitarySpace
for b2 being sequence of b1
for b3 being Point of b1
for b4 being sequence of b1 holds
( b4 = b2 + b3 iff for b5 being Nat holds b4 . b5 = (b2 . b5) + b3 );

theorem Th63: :: CSSPACE:63
for b1 being ComplexUnitarySpace
for b2, b3 being sequence of b1 holds b2 + b3 = b3 + b2
proof end;

definition
let c4 be ComplexUnitarySpace;
let c5, c6 be sequence of c4;
redefine func + as c2 + c3 -> M6( NAT ,the carrier of a1);
commutativity
for b1, b2 being sequence of c4 holds b1 + b2 = b2 + b1
by Th63;
end;

theorem Th64: :: CSSPACE:64
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 holds b2 + (b3 + b4) = (b2 + b3) + b4
proof end;

theorem Th65: :: CSSPACE:65
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 st b2 is V67 & b3 is V67 & b4 = b2 + b3 holds
b4 is V67
proof end;

theorem Th66: :: CSSPACE:66
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 st b2 is V67 & b3 is V67 & b4 = b2 - b3 holds
b4 is V67
proof end;

theorem Th67: :: CSSPACE:67
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3, b4 being sequence of b2 st b3 is V67 & b4 = b1 * b3 holds
b4 is V67
proof end;

theorem Th68: :: CSSPACE:68
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds
( b2 is V67 iff for b3 being Nat holds b2 . b3 = b2 . (b3 + 1) )
proof end;

theorem Th69: :: CSSPACE:69
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds
( b2 is V67 iff for b3, b4 being Nat holds b2 . b3 = b2 . (b3 + b4) )
proof end;

theorem Th70: :: CSSPACE:70
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds
( b2 is V67 iff for b3, b4 being Nat holds b2 . b3 = b2 . b4 )
proof end;

theorem Th71: :: CSSPACE:71
for b1 being ComplexUnitarySpace
for b2, b3 being sequence of b1 holds b2 - b3 = b2 + (- b3)
proof end;

theorem Th72: :: CSSPACE:72
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds b2 = b2 + (0. b1)
proof end;

theorem Th73: :: CSSPACE:73
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3, b4 being sequence of b2 holds b1 * (b3 + b4) = (b1 * b3) + (b1 * b4)
proof end;

theorem Th74: :: CSSPACE:74
for b1, b2 being Complex
for b3 being ComplexUnitarySpace
for b4 being sequence of b3 holds (b1 + b2) * b4 = (b1 * b4) + (b2 * b4)
proof end;

theorem Th75: :: CSSPACE:75
for b1, b2 being Complex
for b3 being ComplexUnitarySpace
for b4 being sequence of b3 holds (b1 * b2) * b4 = b1 * (b2 * b4)
proof end;

theorem Th76: :: CSSPACE:76
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds 1r * b2 = b2
proof end;

theorem Th77: :: CSSPACE:77
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds (- 1r ) * b2 = - b2
proof end;

theorem Th78: :: CSSPACE:78
for b1 being ComplexUnitarySpace
for b2 being Point of b1
for b3 being sequence of b1 holds b3 - b2 = b3 + (- b2)
proof end;

theorem Th79: :: CSSPACE:79
for b1 being ComplexUnitarySpace
for b2, b3 being sequence of b1 holds b2 - b3 = - (b3 - b2)
proof end;

theorem Th80: :: CSSPACE:80
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds b2 = b2 - (0. b1)
proof end;

theorem Th81: :: CSSPACE:81
for b1 being ComplexUnitarySpace
for b2 being sequence of b1 holds b2 = - (- b2)
proof end;

theorem Th82: :: CSSPACE:82
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 holds b2 - (b3 + b4) = (b2 - b3) - b4
proof end;

theorem Th83: :: CSSPACE:83
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 holds (b2 + b3) - b4 = b2 + (b3 - b4)
proof end;

theorem Th84: :: CSSPACE:84
for b1 being ComplexUnitarySpace
for b2, b3, b4 being sequence of b1 holds b2 - (b3 - b4) = (b2 - b3) + b4
proof end;

theorem Th85: :: CSSPACE:85
for b1 being Complex
for b2 being ComplexUnitarySpace
for b3, b4 being sequence of b2 holds b1 * (b3 - b4) = (b1 * b3) - (b1 * b4)
proof end;

theorem Th86: :: CSSPACE:86
ex b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st
for b2, b3 being set st b2 in the_set_of_l2ComplexSequences & b3 in the_set_of_l2ComplexSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) ((seq_id b3) *' ))
proof end;

definition
func cl_scalar -> Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX means :: CSSPACE:def 19
for b1, b2 being set st b1 in the_set_of_l2ComplexSequences & b2 in the_set_of_l2ComplexSequences holds
a1 . [b1,b2] = Sum ((seq_id b1) (#) ((seq_id b2) *' ));
existence
ex b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st
for b2, b3 being set st b2 in the_set_of_l2ComplexSequences & b3 in the_set_of_l2ComplexSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) ((seq_id b3) *' ))
by Th86;
uniqueness
for b1, b2 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st ( for b3, b4 being set st b3 in the_set_of_l2ComplexSequences & b4 in the_set_of_l2ComplexSequences holds
b1 . [b3,b4] = Sum ((seq_id b3) (#) ((seq_id b4) *' )) ) & ( for b3, b4 being set st b3 in the_set_of_l2ComplexSequences & b4 in the_set_of_l2ComplexSequences holds
b2 . [b3,b4] = Sum ((seq_id b3) (#) ((seq_id b4) *' )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines cl_scalar CSSPACE:def 19 :
for b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX holds
( b1 = cl_scalar iff for b2, b3 being set st b2 in the_set_of_l2ComplexSequences & b3 in the_set_of_l2ComplexSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) ((seq_id b3) *' )) );

registration
cluster CUNITSTR(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_scalar #) -> non empty ;
coherence
not CUNITSTR(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_scalar #) is empty
proof end;
end;

definition
func Complex_l2_Space -> non empty CUNITSTR equals :: CSSPACE:def 20
CUNITSTR(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_scalar #);
correctness
coherence
CUNITSTR(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_scalar #) is non empty CUNITSTR
;
;
end;

:: deftheorem Def20 defines Complex_l2_Space CSSPACE:def 20 :
Complex_l2_Space = CUNITSTR(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_scalar #);

theorem Th87: :: CSSPACE:87
for b1 being CUNITSTR st CLSStruct(# the carrier of b1,the Zero of b1,the add of b1,the Mult of b1 #) is ComplexLinearSpace holds
b1 is ComplexLinearSpace
proof end;

theorem Th88: :: CSSPACE:88
for b1 being Complex_Sequence st ( for b2 being Nat holds b1 . b2 = 0c ) holds
( b1 is summable & Sum b1 = 0c )
proof end;

registration
cluster Complex_l2_Space -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( Complex_l2_Space is Abelian & Complex_l2_Space is add-associative & Complex_l2_Space is right_zeroed & Complex_l2_Space is right_complementable & Complex_l2_Space is ComplexLinearSpace-like )
by Th16, Th87;
end;