:: CSSPACE semantic presentation

definition

func the_set_of_ComplexSequences -> non empty set means :Def1: :: CSSPACE:def 1
for b₁ being set holds
( b₁ in a₁ iff b₁ is Complex_Sequence );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :

definition

let c₁ be set ;
assume E2: c₁ in the_set_of_ComplexSequences ;
func seq_id c₁ -> Complex_Sequence equals :Def2: :: CSSPACE:def 2
a₁;
coherence by E2, Def1;

end;

:: deftheorem Def2 defines seq_id CSSPACE:def 2 :

definition

let c₁ be set ;
assume E3: c₁ in COMPLEX ;
func C_id c₁ -> Complex equals :Def3: :: CSSPACE:def 3
a₁;
coherence by E3;

end;

:: deftheorem Def3 defines C_id CSSPACE:def 3 :

theorem Th1: :: CSSPACE:1

ex b₁ being BinOp of the_set_of_ComplexSequences st
( ( for b₂, b₃ being Element of the_set_of_ComplexSequences holds b₁ . b₂,b₃ = (seq_id b₂) + (seq_id b₃) ) & b₁ is commutative & b₁ is associative )

proof end;

theorem Th2: :: CSSPACE:2

ex b₁ being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st
for b₂, b₃ being set st b₂ in COMPLEX & b₃ in the_set_of_ComplexSequences holds
b₁ . [b₂,b₃] = (C_id b₂) (#) (seq_id b₃)

proof end;

definition

func l_add -> BinOp of the_set_of_ComplexSequences means :Def4: :: CSSPACE:def 4
for b₁, b₂ being Element of the_set_of_ComplexSequences holds a₁ . b₁,b₂ = (seq_id b₁) + (seq_id b₂);
existence by Th1;
uniqueness

proof end;

end;

:: deftheorem Def4 defines l_add CSSPACE:def 4 :

definition

func l_mult -> Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences means :Def5: :: CSSPACE:def 5
for b₁, b₂ being set st b₁ in COMPLEX & b₂ in the_set_of_ComplexSequences holds
a₁ . [b₁,b₂] = (C_id b₁) (#) (seq_id b₂);
existence by Th2;
uniqueness

proof end;

end;

:: deftheorem Def5 defines l_mult CSSPACE:def 5 :

definition

func CZeroseq -> Element of the_set_of_ComplexSequences means :Def6: :: CSSPACE:def 6
for b₁ being Nat holds (seq_id a₁) . b₁ = 0c ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :

theorem Th3: :: CSSPACE:3

for b₁ being Complex_Sequence holds seq_id b₁ = b₁

proof end;

theorem Th4: :: CSSPACE:4

for b₁, b₂ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂)

proof end;

theorem Th5: :: CSSPACE:5

for b₁ being Complex
for b₂ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b₁ * b₂ = b₁ (#) (seq_id b₂)

proof end;

registration

cluster CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) -> Abelian ;
coherence

proof end;

end;

Lemma12: for b₁, b₂ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b₁ + b₂ = b₂ + b₁
;

theorem Th6: :: CSSPACE:6

for b₁, b₂, b₃ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th7: :: CSSPACE:7

for b₁ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b₁ + (0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)) = b₁

proof end;

theorem Th8: :: CSSPACE:8

for b₁ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) ex b₂ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) st b₁ + b₂ = 0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)

proof end;

theorem Th9: :: CSSPACE:9

for b₁ being Complex
for b₂, b₃ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof end;

theorem Th10: :: CSSPACE:10

for b₁, b₂ being Complex
for b₃ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃)

proof end;

theorem Th11: :: CSSPACE:11

for b₁, b₂ being Complex
for b₃ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof end;

theorem Th12: :: CSSPACE:12

for b₁ being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds 1r * b₁ = b₁

proof end;

definition end;

:: deftheorem Def7 defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :

definition

let c₁ be ComplexLinearSpace;
let c₂ be Subset of c₁;
assume E20: ( c₂ is lineary-closed & not c₂ is empty ) ;
func Add_ c₂,c₁ -> BinOp of a₂ equals :Def8: :: CSSPACE:def 8
the add of a₁ || a₂;
correctness

proof end;

end;

:: deftheorem Def8 defines Add_ CSSPACE:def 8 :

definition

let c₁ be ComplexLinearSpace;
let c₂ be Subset of c₁;
assume E21: ( c₂ is lineary-closed & not c₂ is empty ) ;
func Mult_ c₂,c₁ -> Function of [:COMPLEX ,a₂:],a₂ equals :Def9: :: CSSPACE:def 9
the Mult of a₁ | [:COMPLEX ,a₂:];
correctness

proof end;

end;

:: deftheorem Def9 defines Mult_ CSSPACE:def 9 :

definition

let c₁ be ComplexLinearSpace;
let c₂ be Subset of c₁;
assume E22: ( c₂ is lineary-closed & not c₂ is empty ) ;
func Zero_ c₂,c₁ -> Element of a₂ equals :Def10: :: CSSPACE:def 10
0. a₁;
correctness

proof end;

end;

:: deftheorem Def10 defines Zero_ CSSPACE:def 10 :

theorem Th13: :: CSSPACE:13

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ is lineary-closed & not b₂ is empty holds
CLSStruct(# b₂,(Zero_ b₂,b₁),(Add_ b₂,b₁),(Mult_ b₂,b₁) #) is Subspace of b₁

proof end;

definition

func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def11: :: CSSPACE:def 11
( not a₁ is empty & ( for b₁ being set holds
( b₁ in a₁ iff ( b₁ in the_set_of_ComplexSequences & |.(seq_id b₁).| (#) |.(seq_id b₁).| is summable ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :

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

theorem Th17: :: CSSPACE:17

( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( for b₁ being set holds
( b₁ is Element of Linear_Space_of_ComplexSequences iff b₁ is Complex_Sequence ) ) & ( for b₁ being set holds
( b₁ is VECTOR of Linear_Space_of_ComplexSequences iff b₁ is Complex_Sequence ) ) & ( for b₁ being VECTOR of Linear_Space_of_ComplexSequences holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of Linear_Space_of_ComplexSequences holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Complex
for b₂ being VECTOR of Linear_Space_of_ComplexSequences holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) ) by Def1, Def2, Th4, Th5;

definition

attr a₁ is strict;
struct CUNITSTR -> CLSStruct ;
aggr CUNITSTR(# carrier, Zero, add, Mult, scalar #) -> CUNITSTR ;
sel scalar c₁ -> Function of [:the carrier of a₁,the carrier of a₁:], COMPLEX ;

end;

registration

cluster non empty strict CUNITSTR ;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:COMPLEX ,c₁:],c₁;
let c₅ be Function of [:c₁,c₁:], COMPLEX ;
cluster CUNITSTR(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence

proof end;

end;

deffunc H₁( CUNITSTR ) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be non empty CUNITSTR ;
let c₂, c₃ be Point of c₁;
func c₂ .|. c₃ -> Complex equals :: CSSPACE:def 12
the scalar of a₁ . [a₂,a₃];
correctness ;

end;

:: deftheorem Def12 defines .|. CSSPACE:def 12 :

consider c₁ being ComplexLinearSpace;

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

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

Lemma28: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . [b₁,b₂] = 0c
by FUNCOP_1:13;

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

then Lemma29: c₂ . [(0. c₁),(0. c₁)] = 0c
by Lemma28;

Lemma30: for b₁ being VECTOR of ((0). c₁) holds
( 0 <= Re (c₂ . [b₁,b₁]) & Im (c₂ . [b₁,b₁]) = 0 )

proof end;

Lemma31: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . [b₁,b₂] = (c₂ . [b₂,b₁]) *'

proof end;

Lemma32: for b₁, b₂, b₃ being VECTOR of ((0). c₁) holds c₂ . [(b₁ + b₂),b₃] = (c₂ . [b₁,b₃]) + (c₂ . [b₂,b₃])

proof end;

Lemma33: for b₁, b₂ being VECTOR of ((0). c₁)
for b₃ being Complex holds c₂ . [(b₃ * b₁),b₂] = b₃ * (c₂ . [b₁,b₂])

proof end;

set c₃ = CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #);

E34: now

let c₄, c₅, c₆ be Point of CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #);
let c₇ be Complex;
thus ( c₄ .|. c₄ = 0c iff c₄ = H₁( CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) )

proof

H₁( CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) = the Zero of CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)
.= 0. ((0). c₁)
.= 0. c₁ by CLVECT_1:31 ;
hence ( c₄ .|. c₄ = 0c iff c₄ = H₁( CUNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) ) by Lemma27, Lemma29, TARSKI:def 1;

end;

thus ( 0 <= Re (c₄ .|. c₄) & 0 = Im (c₄ .|. c₄) ) by Lemma30;
thus c₄ .|. c₅ = (c₅ .|. c₄) *' by Lemma31;
thus (c₄ + c₅) .|. c₆ = (c₄ .|. c₆) + (c₅ .|. c₆)

proof

end;

thus (c₇ * c₄) .|. c₅ = c₇ * (c₄ .|. c₅)

proof

reconsider c₈ = c₄, c₉ = c₅ as VECTOR of ((0). c₁) ;
( (c₇ * c₄) .|. c₅ = c₂ . [(c₇ * c₈),c₉] & c₄ .|. c₅ = c₂ . [c₈,c₉] ) ;
hence (c₇ * c₄) .|. c₅ = c₇ * (c₄ .|. c₅) by Lemma33;

end;

definition

let c₄ be non empty CUNITSTR ;
attr a₁ is ComplexUnitarySpace-like means :Def13: :: CSSPACE:def 13
for b₁, b₂, b₃ being Point of a₁
for b₄ being Complex holds
( ( b₁ .|. b₁ = 0 implies b₁ = 0. a₁ ) & ( b₁ = 0. a₁ implies b₁ .|. b₁ = 0 ) & 0 <= Re (b₁ .|. b₁) & 0 = Im (b₁ .|. b₁) & b₁ .|. b₂ = (b₂ .|. b₁) *' & (b₁ + b₂) .|. b₃ = (b₁ .|. b₃) + (b₂ .|. b₃) & (b₄ * b₁) .|. b₂ = b₄ * (b₁ .|. b₂) );

end;

:: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def 13 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like strict ComplexUnitarySpace-like CUNITSTR ;
existence

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 b₁ being ComplexUnitarySpace holds (0. b₁) .|. (0. b₁) = 0 by Def13;

theorem Th19: :: CSSPACE:19

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds b₂ .|. (b₃ + b₄) = (b₂ .|. b₃) + (b₂ .|. b₄)

proof end;

theorem Th20: :: CSSPACE:20

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃, b₄ being Point of b₂ holds b₃ .|. (b₁ * b₄) = (b₁ *' ) * (b₃ .|. b₄)

proof end;

theorem Th21: :: CSSPACE:21

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃, b₄ being Point of b₂ holds (b₁ * b₃) .|. b₄ = b₃ .|. ((b₁ *' ) * b₄)

proof end;

theorem Th22: :: CSSPACE:22

for b₁, b₂ being Complex
for b₃ being ComplexUnitarySpace
for b₄, b₅, b₆ being Point of b₃ holds ((b₁ * b₄) + (b₂ * b₅)) .|. b₆ = (b₁ * (b₄ .|. b₆)) + (b₂ * (b₅ .|. b₆))

proof end;

theorem Th23: :: CSSPACE:23

for b₁, b₂ being Complex
for b₃ being ComplexUnitarySpace
for b₄, b₅, b₆ being Point of b₃ holds b₄ .|. ((b₁ * b₅) + (b₂ * b₆)) = ((b₁ *' ) * (b₄ .|. b₅)) + ((b₂ *' ) * (b₄ .|. b₆))

proof end;

theorem Th24: :: CSSPACE:24

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. b₃ = b₂ .|. (- b₃)

proof end;

theorem Th25: :: CSSPACE:25

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. b₃ = - (b₂ .|. b₃)

proof end;

theorem Th26: :: CSSPACE:26

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds b₂ .|. (- b₃) = - (b₂ .|. b₃)

proof end;

theorem Th27: :: CSSPACE:27

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. (- b₃) = b₂ .|. b₃

proof end;

theorem Th28: :: CSSPACE:28

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds (b₂ - b₃) .|. b₄ = (b₂ .|. b₄) - (b₃ .|. b₄)

proof end;

theorem Th29: :: CSSPACE:29

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds b₂ .|. (b₃ - b₄) = (b₂ .|. b₃) - (b₂ .|. b₄)

proof end;

theorem Th30: :: CSSPACE:30

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds (b₂ - b₃) .|. (b₄ - b₅) = (((b₂ .|. b₄) - (b₂ .|. b₅)) - (b₃ .|. b₄)) + (b₃ .|. b₅)

proof end;

theorem Th31: :: CSSPACE:31

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds (0. b₁) .|. b₂ = 0

proof end;

theorem Th32: :: CSSPACE:32

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds b₂ .|. (0. b₁) = 0

proof end;

theorem Th33: :: CSSPACE:33

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ + b₃) .|. (b₂ + b₃) = (((b₂ .|. b₂) + (b₂ .|. b₃)) + (b₃ .|. b₂)) + (b₃ .|. b₃)

proof end;

theorem Th34: :: CSSPACE:34

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ + b₃) .|. (b₂ - b₃) = (((b₂ .|. b₂) - (b₂ .|. b₃)) + (b₃ .|. b₂)) - (b₃ .|. b₃)

proof end;

theorem Th35: :: CSSPACE:35

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ - b₃) .|. (b₂ - b₃) = (((b₂ .|. b₂) - (b₂ .|. b₃)) - (b₃ .|. b₂)) + (b₃ .|. b₃)

proof end;

Lemma51: for b₁ being ComplexUnitarySpace
for b₂, b₃ being Complex
for b₄, b₅ being Point 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₃ *' )) * (b₅ .|. b₅))

proof end;

theorem Th36: :: CSSPACE:36

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds |.(b₂ .|. b₂).| = Re (b₂ .|. b₂)

proof end;

theorem Th37: :: CSSPACE:37

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds |.(b₂ .|. b₃).| <= (sqrt |.(b₂ .|. b₂).|) * (sqrt |.(b₃ .|. b₃).|)

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅, c₆ be Point of c₄;
pred c₂,c₃ are_orthogonal means :Def14: :: CSSPACE:def 14
a₂ .|. a₃ = 0;
symmetry by Def13, COMPLEX1:113;

end;

:: deftheorem Def14 defines are_orthogonal CSSPACE:def 14 :

theorem Th38: :: CSSPACE:38

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
b₂, - b₃ are_orthogonal

proof end;

theorem Th39: :: CSSPACE:39

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
- b₂,b₃ are_orthogonal

proof end;

theorem Th40: :: CSSPACE:40

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
- b₂, - b₃ are_orthogonal

proof end;

theorem Th41: :: CSSPACE:41

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds b₂, 0. b₁ are_orthogonal

proof end;

theorem Th42: :: CSSPACE:42

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
(b₂ + b₃) .|. (b₂ + b₃) = (b₂ .|. b₂) + (b₃ .|. b₃)

proof end;

theorem Th43: :: CSSPACE:43

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
(b₂ - b₃) .|. (b₂ - b₃) = (b₂ .|. b₂) + (b₃ .|. b₃)

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅ be Point of c₄;
func ||.c₂.|| -> Real equals :: CSSPACE:def 15
sqrt |.(a₂ .|. a₂).|;
correctness ;

end;

:: deftheorem Def15 defines ||. CSSPACE:def 15 :

theorem Th44: :: CSSPACE:44

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds
( ||.b₂.|| = 0 iff b₂ = 0. b₁ )

proof end;

theorem Th45: :: CSSPACE:45

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃ being Point of b₂ holds ||.(b₁ * b₃).|| = |.b₁.| * ||.b₃.||

proof end;

theorem Th46: :: CSSPACE:46

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds 0 <= ||.b₂.||

proof end;

theorem Th47: :: CSSPACE:47

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds |.(b₂ .|. b₃).| <= ||.b₂.|| * ||.b₃.|| by Th37;

theorem Th48: :: CSSPACE:48

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ + b₃).|| <= ||.b₂.|| + ||.b₃.||

proof end;

theorem Th49: :: CSSPACE:49

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds ||.(- b₂).|| = ||.b₂.||

proof end;

theorem Th50: :: CSSPACE:50

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds ||.b₂.|| - ||.b₃.|| <= ||.(b₂ - b₃).||

proof end;

theorem Th51: :: CSSPACE:51

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds abs (||.b₂.|| - ||.b₃.||) <= ||.(b₂ - b₃).||

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅, c₆ be Point of c₄;
func dist c₂,c₃ -> Real equals :: CSSPACE:def 16
||.(a₂ - a₃).||;
correctness ;

end;

:: deftheorem Def16 defines dist CSSPACE:def 16 :

theorem Th52: :: CSSPACE:52

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ = dist b₃,b₂

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅, c₆ be Point of c₄;
redefine func dist as dist c₂,c₃ -> Real;
commutativity by Th52;

end;

theorem Th53: :: CSSPACE:53

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁ holds dist b₂,b₂ = 0

proof end;

theorem Th54: :: CSSPACE:54

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist b₂,b₃ <= (dist b₂,b₄) + (dist b₄,b₃)

proof end;

theorem Th55: :: CSSPACE:55

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds
( b₂ <> b₃ iff dist b₂,b₃ <> 0 )

proof end;

theorem Th56: :: CSSPACE:56

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ >= 0 by Th46;

theorem Th57: :: CSSPACE:57

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds
( b₂ <> b₃ iff dist b₂,b₃ > 0 )

proof end;

theorem Th58: :: CSSPACE:58

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ = sqrt |.((b₂ - b₃) .|. (b₂ - b₃)).| ;

theorem Th59: :: CSSPACE:59

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds dist (b₂ + b₃),(b₄ + b₅) <= (dist b₂,b₄) + (dist b₃,b₅)

proof end;

theorem Th60: :: CSSPACE:60

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₅) <= (dist b₂,b₄) + (dist b₃,b₅)

proof end;

theorem Th61: :: CSSPACE:61

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₃) = dist b₂,b₄

proof end;

theorem Th62: :: CSSPACE:62

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₃) <= (dist b₃,b₂) + (dist b₃,b₄)

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅ be sequence of c₄;
func - c₂ -> sequence of a₁ means :Def17: :: CSSPACE:def 17
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines - CSSPACE:def 17 :

definition

let c₄ be ComplexUnitarySpace;
let c₅ be sequence of c₄;
let c₆ be Point of c₄;
func c₂ + c₃ -> sequence of a₁ means :Def18: :: CSSPACE:def 18
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines + CSSPACE:def 18 :

theorem Th63: :: CSSPACE:63

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

definition

let c₄ be ComplexUnitarySpace;
let c₅, c₆ be sequence of c₄;
redefine func + as c₂ + c₃ -> M6( NAT ,the carrier of a₁);
commutativity by Th63;

end;

theorem Th64: :: CSSPACE:64

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th65: :: CSSPACE:65

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is V67 & b₃ is V67 & b₄ = b₂ + b₃ holds
b₄ is V67

proof end;

theorem Th66: :: CSSPACE:66

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is V67 & b₃ is V67 & b₄ = b₂ - b₃ holds
b₄ is V67

proof end;

theorem Th67: :: CSSPACE:67

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃, b₄ being sequence of b₂ st b₃ is V67 & b₄ = b₁ * b₃ holds
b₄ is V67

proof end;

theorem Th68: :: CSSPACE:68

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V67 iff for b₃ being Nat holds b₂ . b₃ = b₂ . (b₃ + 1) )

proof end;

theorem Th69: :: CSSPACE:69

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V67 iff for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . (b₃ + b₄) )

proof end;

theorem Th70: :: CSSPACE:70

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V67 iff for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . b₄ )

proof end;

theorem Th71: :: CSSPACE:71

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th72: :: CSSPACE:72

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ = b₂ + (0. b₁)

proof end;

theorem Th73: :: CSSPACE:73

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃, b₄ being sequence of b₂ holds b₁ * (b₃ + b₄) = (b₁ * b₃) + (b₁ * b₄)

proof end;

theorem Th74: :: CSSPACE:74

for b₁, b₂ being Complex
for b₃ being ComplexUnitarySpace
for b₄ being sequence of b₃ holds (b₁ + b₂) * b₄ = (b₁ * b₄) + (b₂ * b₄)

proof end;

theorem Th75: :: CSSPACE:75

for b₁, b₂ being Complex
for b₃ being ComplexUnitarySpace
for b₄ being sequence of b₃ holds (b₁ * b₂) * b₄ = b₁ * (b₂ * b₄)

proof end;

theorem Th76: :: CSSPACE:76

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds 1r * b₂ = b₂

proof end;

theorem Th77: :: CSSPACE:77

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds (- 1r ) * b₂ = - b₂

proof end;

theorem Th78: :: CSSPACE:78

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ holds b₃ - b₂ = b₃ + (- b₂)

proof end;

theorem Th79: :: CSSPACE:79

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = - (b₃ - b₂)

proof end;

theorem Th80: :: CSSPACE:80

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ = b₂ - (0. b₁)

proof end;

theorem Th81: :: CSSPACE:81

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ = - (- b₂)

proof end;

theorem Th82: :: CSSPACE:82

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

theorem Th83: :: CSSPACE:83

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds (b₂ + b₃) - b₄ = b₂ + (b₃ - b₄)

proof end;

theorem Th84: :: CSSPACE:84

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th85: :: CSSPACE:85

for b₁ being Complex
for b₂ being ComplexUnitarySpace
for b₃, b₄ being sequence of b₂ holds b₁ * (b₃ - b₄) = (b₁ * b₃) - (b₁ * b₄)

proof end;

theorem Th86: :: CSSPACE:86

ex b₁ being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st
for b₂, b₃ being set st b₂ in the_set_of_l2ComplexSequences & b₃ in the_set_of_l2ComplexSequences holds
b₁ . [b₂,b₃] = Sum ((seq_id b₂) (#) ((seq_id b₃) *' ))

proof end;

definition

func cl_scalar -> Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX means :: CSSPACE:def 19
for b₁, b₂ being set st b₁ in the_set_of_l2ComplexSequences & b₂ in the_set_of_l2ComplexSequences holds
a₁ . [b₁,b₂] = Sum ((seq_id b₁) (#) ((seq_id b₂) *' ));
existence by Th86;
uniqueness

proof end;

end;

:: deftheorem Def19 defines cl_scalar CSSPACE:def 19 :

registration end;

definition end;

:: deftheorem Def20 defines Complex_l2_Space CSSPACE:def 20 :

theorem Th87: :: CSSPACE:87

for b₁ being CUNITSTR st CLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) is ComplexLinearSpace holds
b₁ is ComplexLinearSpace

proof end;

theorem Th88: :: CSSPACE:88

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
( b₁ is summable & Sum b₁ = 0c )

proof end;

registration end;