:: Complex Linear Space and Complex Normed Space
:: by Noboru Endou
::
:: Received January 26, 2004
:: Copyright (c) 2004 Association of Mizar Users
begin
definition
attr
c
1
is
strict
;
struct
CLSStruct
->
addLoopStr
;
aggr
CLSStruct
(#
carrier
,
ZeroF
,
addF
,
Mult
#)
->
CLSStruct
;
sel
Mult
c
1
->
Function
of
[:
COMPLEX
,the
carrier
of
c
1
:]
,the
carrier
of
c
1
;
end;
registration
cluster
non
empty
CLSStruct
;
existence
not for
b
1
being
CLSStruct
holds
b
1
is
empty
proof
end;
end;
definition
let
V
be
CLSStruct
;
mode
VECTOR of
V
is
Element
of ;
end;
definition
let
V
be non
empty
CLSStruct
;
let
v
be
VECTOR
of
V
;
let
z
be
Complex
;
func
z
*
v
->
Element
of
equals
:: CLVECT_1:def 1
the
Mult
of
V
.
[
z
,
v
]
;
coherence
the
Mult
of
V
.
[
z
,
v
]
is
Element
of
;
end;
::
deftheorem
defines
*
CLVECT_1:def 1 :
for
V
being non
empty
CLSStruct
for
v
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
v
=
the
Mult
of
V
.
[
z
,
v
]
;
registration
let
ZS
be non
empty
set
;
let
O
be
Element
of
ZS
;
let
F
be
BinOp
of
ZS
;
let
G
be
Function
of
[:
COMPLEX
,
ZS
:]
,
ZS
;
cluster
CLSStruct
(#
ZS
,
O
,
F
,
G
#)
->
non
empty
;
coherence
not
CLSStruct
(#
ZS
,
O
,
F
,
G
#) is
empty
;
end;
definition
let
IT
be non
empty
CLSStruct
;
attr
IT
is
ComplexLinearSpace-like
means
:
Def2
:
:: CLVECT_1:def 2
( ( for
z
being
Complex
for
v
,
w
being
VECTOR
of
IT
holds
z
*
(
v
+
w
)
=
(
z
*
v
)
+
(
z
*
w
)
) & ( for
z1
,
z2
being
Complex
for
v
being
VECTOR
of
IT
holds
(
z1
+
z2
)
*
v
=
(
z1
*
v
)
+
(
z2
*
v
)
) & ( for
z1
,
z2
being
Complex
for
v
being
VECTOR
of
IT
holds
(
z1
*
z2
)
*
v
=
z1
*
(
z2
*
v
)
) & ( for
v
being
VECTOR
of
IT
holds
1r
*
v
=
v
) );
end;
::
deftheorem
Def2
defines
ComplexLinearSpace-like
CLVECT_1:def 2 :
for
IT
being non
empty
CLSStruct
holds
(
IT
is
ComplexLinearSpace-like
iff ( ( for
z
being
Complex
for
v
,
w
being
VECTOR
of
IT
holds
z
*
(
v
+
w
)
=
(
z
*
v
)
+
(
z
*
w
)
) & ( for
z1
,
z2
being
Complex
for
v
being
VECTOR
of
IT
holds
(
z1
+
z2
)
*
v
=
(
z1
*
v
)
+
(
z2
*
v
)
) & ( for
z1
,
z2
being
Complex
for
v
being
VECTOR
of
IT
holds
(
z1
*
z2
)
*
v
=
z1
*
(
z2
*
v
)
) & ( for
v
being
VECTOR
of
IT
holds
1r
*
v
=
v
) ) );
definition
func
Trivial-CLSStruct
->
strict
CLSStruct
equals
:: CLVECT_1:def 3
CLSStruct
(# 1,
op0
,
op2
,
(
pr2
COMPLEX
,1
)
#);
coherence
CLSStruct
(# 1,
op0
,
op2
,
(
pr2
COMPLEX
,1
)
#) is
strict
CLSStruct
;
end;
::
deftheorem
defines
Trivial-CLSStruct
CLVECT_1:def 3 :
Trivial-CLSStruct
=
CLSStruct
(# 1,
op0
,
op2
,
(
pr2
COMPLEX
,1
)
#);
registration
cluster
Trivial-CLSStruct
->
non
empty
trivial
strict
;
coherence
(
Trivial-CLSStruct
is
trivial
& not
Trivial-CLSStruct
is
empty
)
by
CARD_1:87
;
end;
registration
cluster
non
empty
right_complementable
Abelian
add-associative
right_zeroed
strict
ComplexLinearSpace-like
CLSStruct
;
existence
ex
b
1
being non
empty
CLSStruct
st
(
b
1
is
strict
&
b
1
is
Abelian
&
b
1
is
add-associative
&
b
1
is
right_zeroed
&
b
1
is
right_complementable
&
b
1
is
ComplexLinearSpace-like
)
proof
end;
end;
definition
mode
ComplexLinearSpace
is
non
empty
right_complementable
Abelian
add-associative
right_zeroed
ComplexLinearSpace-like
CLSStruct
;
end;
theorem
:: CLVECT_1:1
canceled;
theorem
Th2
:
:: CLVECT_1:2
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
st (
z
=
0
or
v
=
0.
V
) holds
z
*
v
=
0.
V
proof
end;
theorem
Th3
:
:: CLVECT_1:3
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
holds
( not
z
*
v
=
0.
V
or
z
=
0
or
v
=
0.
V
)
proof
end;
theorem
Th4
:
:: CLVECT_1:4
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
-
v
=
(
-
1r
)
*
v
proof
end;
theorem
Th5
:
:: CLVECT_1:5
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
st
v
=
-
v
holds
v
=
0.
V
proof
end;
theorem
:: CLVECT_1:6
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
st
v
+
v
=
0.
V
holds
v
=
0.
V
proof
end;
theorem
Th7
:
:: CLVECT_1:7
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
(
-
v
)
=
(
-
z
)
*
v
proof
end;
theorem
Th8
:
:: CLVECT_1:8
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
(
-
v
)
=
-
(
z
*
v
)
proof
end;
theorem
:: CLVECT_1:9
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
holds
(
-
z
)
*
(
-
v
)
=
z
*
v
proof
end;
theorem
Th10
:
:: CLVECT_1:10
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
(
v
-
u
)
=
(
z
*
v
)
-
(
z
*
u
)
proof
end;
theorem
Th11
:
:: CLVECT_1:11
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z1
,
z2
being
Complex
holds
(
z1
-
z2
)
*
v
=
(
z1
*
v
)
-
(
z2
*
v
)
proof
end;
theorem
:: CLVECT_1:12
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
z
being
Complex
st
z
<>
0
&
z
*
v
=
z
*
u
holds
v
=
u
proof
end;
theorem
:: CLVECT_1:13
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z1
,
z2
being
Complex
st
v
<>
0.
V
&
z1
*
v
=
z2
*
v
holds
z1
=
z2
proof
end;
Lm1
: for
V
being non
empty
addLoopStr
holds
Sum
(
<*>
the
carrier
of
V
)
=
0.
V
proof
end;
Lm2
: for
V
being non
empty
addLoopStr
for
F
being
FinSequence
of the
carrier
of
V
st
len
F
=
0
holds
Sum
F
=
0.
V
proof
end;
theorem
:: CLVECT_1:14
for
V
being
ComplexLinearSpace
for
z
being
Complex
for
F
,
G
being
FinSequence
of the
carrier
of
V
st
len
F
=
len
G
& ( for
k
being
Element
of
NAT
for
v
being
VECTOR
of
V
st
k
in
dom
F
&
v
=
G
.
k
holds
F
.
k
=
z
*
v
) holds
Sum
F
=
z
*
(
Sum
G
)
proof
end;
theorem
:: CLVECT_1:15
for
V
being
ComplexLinearSpace
for
z
being
Complex
holds
z
*
(
Sum
(
<*>
the
carrier
of
V
)
)
=
0.
V
by
Lm1
,
Th2
;
theorem
:: CLVECT_1:16
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
(
Sum
<*
v
,
u
*>
)
=
(
z
*
v
)
+
(
z
*
u
)
proof
end;
theorem
:: CLVECT_1:17
for
V
being
ComplexLinearSpace
for
u
,
v1
,
v2
being
VECTOR
of
V
for
z
being
Complex
holds
z
*
(
Sum
<*
u
,
v1
,
v2
*>
)
=
(
(
z
*
u
)
+
(
z
*
v1
)
)
+
(
z
*
v2
)
proof
end;
theorem
Th18
:
:: CLVECT_1:18
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
Sum
<*
v
,
v
*>
=
(
1r
+
1r
)
*
v
proof
end;
theorem
:: CLVECT_1:19
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
Sum
<*
(
-
v
)
,
(
-
v
)
*>
=
(
-
(
1r
+
1r
)
)
*
v
proof
end;
theorem
:: CLVECT_1:20
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
Sum
<*
v
,
v
,
v
*>
=
(
(
1r
+
1r
)
+
1r
)
*
v
proof
end;
begin
definition
let
V
be
ComplexLinearSpace
;
let
V1
be
Subset
of ;
attr
V1
is
linearly-closed
means
:
Def4
:
:: CLVECT_1:def 4
( ( for
v
,
u
being
VECTOR
of
V
st
v
in
V1
&
u
in
V1
holds
v
+
u
in
V1
) & ( for
z
being
Complex
for
v
being
VECTOR
of
V
st
v
in
V1
holds
z
*
v
in
V1
) );
end;
::
deftheorem
Def4
defines
linearly-closed
CLVECT_1:def 4 :
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of holds
(
V1
is
linearly-closed
iff ( ( for
v
,
u
being
VECTOR
of
V
st
v
in
V1
&
u
in
V1
holds
v
+
u
in
V1
) & ( for
z
being
Complex
for
v
being
VECTOR
of
V
st
v
in
V1
holds
z
*
v
in
V1
) ) );
theorem
Th21
:
:: CLVECT_1:21
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
<>
{}
&
V1
is
linearly-closed
holds
0.
V
in
V1
proof
end;
theorem
Th22
:
:: CLVECT_1:22
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
is
linearly-closed
holds
for
v
being
VECTOR
of
V
st
v
in
V1
holds
-
v
in
V1
proof
end;
theorem
:: CLVECT_1:23
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
is
linearly-closed
holds
for
v
,
u
being
VECTOR
of
V
st
v
in
V1
&
u
in
V1
holds
v
-
u
in
V1
proof
end;
theorem
Th24
:
:: CLVECT_1:24
for
V
being
ComplexLinearSpace
holds
{
(
0.
V
)
}
is
linearly-closed
proof
end;
theorem
:: CLVECT_1:25
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st the
carrier
of
V
=
V1
holds
V1
is
linearly-closed
proof
end;
theorem
:: CLVECT_1:26
for
V
being
ComplexLinearSpace
for
V1
,
V2
,
V3
being
Subset
of st
V1
is
linearly-closed
&
V2
is
linearly-closed
&
V3
=
{
(
v
+
u
)
where
v
,
u
is
VECTOR
of
V
: (
v
in
V1
&
u
in
V2
)
}
holds
V3
is
linearly-closed
proof
end;
theorem
:: CLVECT_1:27
for
V
being
ComplexLinearSpace
for
V1
,
V2
being
Subset
of st
V1
is
linearly-closed
&
V2
is
linearly-closed
holds
V1
/\
V2
is
linearly-closed
proof
end;
definition
let
V
be
ComplexLinearSpace
;
mode
Subspace
of
V
->
ComplexLinearSpace
means
:
Def5
:
:: CLVECT_1:def 5
( the
carrier
of
it
c=
the
carrier
of
V
&
0.
it
=
0.
V
& the
addF
of
it
=
the
addF
of
V
||
the
carrier
of
it
& the
Mult
of
it
=
the
Mult
of
V
|
[:
COMPLEX
,the
carrier
of
it
:]
);
existence
ex
b
1
being
ComplexLinearSpace
st
( the
carrier
of
b
1
c=
the
carrier
of
V
&
0.
b
1
=
0.
V
& the
addF
of
b
1
=
the
addF
of
V
||
the
carrier
of
b
1
& the
Mult
of
b
1
=
the
Mult
of
V
|
[:
COMPLEX
,the
carrier
of
b
1
:]
)
proof
end;
end;
::
deftheorem
Def5
defines
Subspace
CLVECT_1:def 5 :
for
V
,
b
2
being
ComplexLinearSpace
holds
(
b
2
is
Subspace
of
V
iff ( the
carrier
of
b
2
c=
the
carrier
of
V
&
0.
b
2
=
0.
V
& the
addF
of
b
2
=
the
addF
of
V
||
the
carrier
of
b
2
& the
Mult
of
b
2
=
the
Mult
of
V
|
[:
COMPLEX
,the
carrier
of
b
2
:]
) );
theorem
:: CLVECT_1:28
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
for
x
being
set
st
x
in
W1
&
W1
is
Subspace
of
W2
holds
x
in
W2
proof
end;
theorem
Th29
:
:: CLVECT_1:29
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
for
x
being
set
st
x
in
W
holds
x
in
V
proof
end;
theorem
Th30
:
:: CLVECT_1:30
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
for
w
being
VECTOR
of
W
holds
w
is
VECTOR
of
V
proof
end;
theorem
:: CLVECT_1:31
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
0.
W
=
0.
V
by
Def5
;
theorem
:: CLVECT_1:32
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
0.
W1
=
0.
W2
proof
end;
theorem
Th33
:
:: CLVECT_1:33
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
w1
,
w2
being
VECTOR
of
W
st
w1
=
v
&
w2
=
u
holds
w1
+
w2
=
v
+
u
proof
end;
theorem
Th34
:
:: CLVECT_1:34
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
for
w
being
VECTOR
of
W
st
w
=
v
holds
z
*
w
=
z
*
v
proof
end;
theorem
Th35
:
:: CLVECT_1:35
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
w
being
VECTOR
of
W
st
w
=
v
holds
-
v
=
-
w
proof
end;
theorem
Th36
:
:: CLVECT_1:36
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
w1
,
w2
being
VECTOR
of
W
st
w1
=
v
&
w2
=
u
holds
w1
-
w2
=
v
-
u
proof
end;
Lm3
: for
V
being
ComplexLinearSpace
for
V1
being
Subset
of
for
W
being
Subspace
of
V
st the
carrier
of
W
=
V1
holds
V1
is
linearly-closed
proof
end;
theorem
Th37
:
:: CLVECT_1:37
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
0.
V
in
W
proof
end;
theorem
:: CLVECT_1:38
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
0.
W1
in
W2
proof
end;
theorem
:: CLVECT_1:39
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
0.
W
in
V
by
Th29
,
RLVECT_1:3
;
theorem
Th40
:
:: CLVECT_1:40
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
u
in
W
&
v
in
W
holds
u
+
v
in
W
proof
end;
theorem
Th41
:
:: CLVECT_1:41
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
st
v
in
W
holds
z
*
v
in
W
proof
end;
theorem
Th42
:
:: CLVECT_1:42
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
v
in
W
holds
-
v
in
W
proof
end;
theorem
Th43
:
:: CLVECT_1:43
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
u
in
W
&
v
in
W
holds
u
-
v
in
W
proof
end;
theorem
Th44
:
:: CLVECT_1:44
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of
for
D
being non
empty
set
for
d1
being
Element
of
D
for
A
being
BinOp
of
D
for
M
being
Function
of
[:
COMPLEX
,
D
:]
,
D
st
V1
=
D
&
d1
=
0.
V
&
A
=
the
addF
of
V
||
V1
&
M
=
the
Mult
of
V
|
[:
COMPLEX
,
V1
:]
holds
CLSStruct
(#
D
,
d1
,
A
,
M
#) is
Subspace
of
V
proof
end;
theorem
Th45
:
:: CLVECT_1:45
for
V
being
ComplexLinearSpace
holds
V
is
Subspace
of
V
proof
end;
theorem
Th46
:
:: CLVECT_1:46
for
V
,
X
being
strict
ComplexLinearSpace
st
V
is
Subspace
of
X
&
X
is
Subspace
of
V
holds
V
=
X
proof
end;
theorem
Th47
:
:: CLVECT_1:47
for
V
,
X
,
Y
being
ComplexLinearSpace
st
V
is
Subspace
of
X
&
X
is
Subspace
of
Y
holds
V
is
Subspace
of
Y
proof
end;
theorem
Th48
:
:: CLVECT_1:48
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
st the
carrier
of
W1
c=
the
carrier
of
W2
holds
W1
is
Subspace
of
W2
proof
end;
theorem
:: CLVECT_1:49
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
st ( for
v
being
VECTOR
of
V
st
v
in
W1
holds
v
in
W2
) holds
W1
is
Subspace
of
W2
proof
end;
registration
let
V
be
ComplexLinearSpace
;
cluster
strict
Subspace
of
V
;
existence
ex
b
1
being
Subspace
of
V
st
b
1
is
strict
proof
end;
end;
theorem
Th50
:
:: CLVECT_1:50
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
strict
Subspace
of
V
st the
carrier
of
W1
=
the
carrier
of
W2
holds
W1
=
W2
proof
end;
theorem
Th51
:
:: CLVECT_1:51
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
strict
Subspace
of
V
st ( for
v
being
VECTOR
of
V
holds
(
v
in
W1
iff
v
in
W2
) ) holds
W1
=
W2
proof
end;
theorem
:: CLVECT_1:52
for
V
being
strict
ComplexLinearSpace
for
W
being
strict
Subspace
of
V
st the
carrier
of
W
=
the
carrier
of
V
holds
W
=
V
proof
end;
theorem
:: CLVECT_1:53
for
V
being
strict
ComplexLinearSpace
for
W
being
strict
Subspace
of
V
st ( for
v
being
VECTOR
of
V
holds
(
v
in
W
iff
v
in
V
) ) holds
W
=
V
proof
end;
theorem
:: CLVECT_1:54
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of
for
W
being
Subspace
of
V
st the
carrier
of
W
=
V1
holds
V1
is
linearly-closed
by
Lm3
;
theorem
Th55
:
:: CLVECT_1:55
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
<>
{}
&
V1
is
linearly-closed
holds
ex
W
being
strict
Subspace
of
V
st
V1
=
the
carrier
of
W
proof
end;
definition
let
V
be
ComplexLinearSpace
;
func
(0).
V
->
strict
Subspace
of
V
means
:
Def6
:
:: CLVECT_1:def 6
the
carrier
of
it
=
{
(
0.
V
)
}
;
correctness
existence
ex
b
1
being
strict
Subspace
of
V
st the
carrier
of
b
1
=
{
(
0.
V
)
}
;
uniqueness
for
b
1
,
b
2
being
strict
Subspace
of
V
st the
carrier
of
b
1
=
{
(
0.
V
)
}
& the
carrier
of
b
2
=
{
(
0.
V
)
}
holds
b
1
=
b
2
;
by
Th24
,
Th50
,
Th55
;
end;
::
deftheorem
Def6
defines
(0).
CLVECT_1:def 6 :
for
V
being
ComplexLinearSpace
for
b
2
being
strict
Subspace
of
V
holds
(
b
2
=
(0).
V
iff the
carrier
of
b
2
=
{
(
0.
V
)
}
);
definition
let
V
be
ComplexLinearSpace
;
func
(Omega).
V
->
strict
Subspace
of
V
equals
:: CLVECT_1:def 7
CLSStruct
(# the
carrier
of
V
,the
ZeroF
of
V
,the
addF
of
V
,the
Mult
of
V
#);
coherence
CLSStruct
(# the
carrier
of
V
,the
ZeroF
of
V
,the
addF
of
V
,the
Mult
of
V
#) is
strict
Subspace
of
V
proof
end;
end;
::
deftheorem
defines
(Omega).
CLVECT_1:def 7 :
for
V
being
ComplexLinearSpace
holds
(Omega).
V
=
CLSStruct
(# the
carrier
of
V
,the
ZeroF
of
V
,the
addF
of
V
,the
Mult
of
V
#);
theorem
Th56
:
:: CLVECT_1:56
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
(0).
W
=
(0).
V
proof
end;
theorem
Th57
:
:: CLVECT_1:57
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
(0).
W1
=
(0).
W2
proof
end;
theorem
:: CLVECT_1:58
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
(0).
W
is
Subspace
of
V
by
Th47
;
theorem
:: CLVECT_1:59
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
(0).
V
is
Subspace
of
W
proof
end;
theorem
:: CLVECT_1:60
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
(0).
W1
is
Subspace
of
W2
proof
end;
theorem
:: CLVECT_1:61
for
V
being
strict
ComplexLinearSpace
holds
V
is
Subspace
of
(Omega).
V
;
definition
let
V
be
ComplexLinearSpace
;
let
v
be
VECTOR
of
V
;
let
W
be
Subspace
of
V
;
func
v
+
W
->
Subset
of
equals
:: CLVECT_1:def 8
{
(
v
+
u
)
where
u
is
VECTOR
of
V
:
u
in
W
}
;
coherence
{
(
v
+
u
)
where
u
is
VECTOR
of
V
:
u
in
W
}
is
Subset
of
proof
end;
end;
::
deftheorem
defines
+
CLVECT_1:def 8 :
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
v
+
W
=
{
(
v
+
u
)
where
u
is
VECTOR
of
V
:
u
in
W
}
;
Lm4
: for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
(
0.
V
)
+
W
=
the
carrier
of
W
proof
end;
definition
let
V
be
ComplexLinearSpace
;
let
W
be
Subspace
of
V
;
mode
Coset
of
W
->
Subset
of
means
:
Def9
:
:: CLVECT_1:def 9
ex
v
being
VECTOR
of
V
st
it
=
v
+
W
;
existence
ex
b
1
being
Subset
of ex
v
being
VECTOR
of
V
st
b
1
=
v
+
W
proof
end;
end;
::
deftheorem
Def9
defines
Coset
CLVECT_1:def 9 :
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
for
b
3
being
Subset
of holds
(
b
3
is
Coset
of
W
iff ex
v
being
VECTOR
of
V
st
b
3
=
v
+
W
);
theorem
Th62
:
:: CLVECT_1:62
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
0.
V
in
v
+
W
iff
v
in
W
)
proof
end;
theorem
Th63
:
:: CLVECT_1:63
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
v
in
v
+
W
proof
end;
theorem
:: CLVECT_1:64
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds
(
0.
V
)
+
W
=
the
carrier
of
W
by
Lm4
;
theorem
Th65
:
:: CLVECT_1:65
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
v
+
(
(0).
V
)
=
{
v
}
proof
end;
Lm5
: for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
in
W
iff
v
+
W
=
the
carrier
of
W
)
proof
end;
theorem
Th66
:
:: CLVECT_1:66
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
v
+
(
(Omega).
V
)
=
the
carrier
of
V
proof
end;
theorem
Th67
:
:: CLVECT_1:67
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
0.
V
in
v
+
W
iff
v
+
W
=
the
carrier
of
W
)
proof
end;
theorem
:: CLVECT_1:68
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
in
W
iff
v
+
W
=
the
carrier
of
W
)
by
Lm5
;
theorem
Th69
:
:: CLVECT_1:69
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
st
v
in
W
holds
(
z
*
v
)
+
W
=
the
carrier
of
W
proof
end;
theorem
Th70
:
:: CLVECT_1:70
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
st
z
<>
0
&
(
z
*
v
)
+
W
=
the
carrier
of
W
holds
v
in
W
proof
end;
theorem
Th71
:
:: CLVECT_1:71
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
in
W
iff
(
-
v
)
+
W
=
the
carrier
of
W
)
proof
end;
theorem
Th72
:
:: CLVECT_1:72
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
u
in
W
iff
v
+
W
=
(
v
+
u
)
+
W
)
proof
end;
theorem
:: CLVECT_1:73
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
u
in
W
iff
v
+
W
=
(
v
-
u
)
+
W
)
proof
end;
theorem
Th74
:
:: CLVECT_1:74
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
in
u
+
W
iff
u
+
W
=
v
+
W
)
proof
end;
theorem
Th75
:
:: CLVECT_1:75
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
+
W
=
(
-
v
)
+
W
iff
v
in
W
)
proof
end;
theorem
Th76
:
:: CLVECT_1:76
for
V
being
ComplexLinearSpace
for
u
,
v1
,
v2
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
u
in
v1
+
W
&
u
in
v2
+
W
holds
v1
+
W
=
v2
+
W
proof
end;
theorem
:: CLVECT_1:77
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
u
in
v
+
W
&
u
in
(
-
v
)
+
W
holds
v
in
W
proof
end;
theorem
Th78
:
:: CLVECT_1:78
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
st
z
<>
1r
&
z
*
v
in
v
+
W
holds
v
in
W
proof
end;
theorem
Th79
:
:: CLVECT_1:79
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
z
being
Complex
for
W
being
Subspace
of
V
st
v
in
W
holds
z
*
v
in
v
+
W
proof
end;
theorem
:: CLVECT_1:80
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
-
v
in
v
+
W
iff
v
in
W
)
proof
end;
theorem
Th81
:
:: CLVECT_1:81
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
u
+
v
in
v
+
W
iff
u
in
W
)
proof
end;
theorem
:: CLVECT_1:82
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
v
-
u
in
v
+
W
iff
u
in
W
)
proof
end;
theorem
Th83
:
:: CLVECT_1:83
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
u
in
v
+
W
iff ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
u
=
v
+
v1
) )
proof
end;
theorem
:: CLVECT_1:84
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
(
u
in
v
+
W
iff ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
u
=
v
-
v1
) )
proof
end;
theorem
Th85
:
:: CLVECT_1:85
for
V
being
ComplexLinearSpace
for
v1
,
v2
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
( ex
v
being
VECTOR
of
V
st
(
v1
in
v
+
W
&
v2
in
v
+
W
) iff
v1
-
v2
in
W
)
proof
end;
theorem
Th86
:
:: CLVECT_1:86
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
v
+
W
=
u
+
W
holds
ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
v
+
v1
=
u
)
proof
end;
theorem
Th87
:
:: CLVECT_1:87
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
st
v
+
W
=
u
+
W
holds
ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
v
-
v1
=
u
)
proof
end;
theorem
Th88
:
:: CLVECT_1:88
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
for
W1
,
W2
being
strict
Subspace
of
V
holds
(
v
+
W1
=
v
+
W2
iff
W1
=
W2
)
proof
end;
theorem
Th89
:
:: CLVECT_1:89
for
V
being
ComplexLinearSpace
for
v
,
u
being
VECTOR
of
V
for
W1
,
W2
being
strict
Subspace
of
V
st
v
+
W1
=
u
+
W2
holds
W1
=
W2
proof
end;
theorem
:: CLVECT_1:90
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
for
C
being
Coset
of
W
holds
(
C
is
linearly-closed
iff
C
=
the
carrier
of
W
)
proof
end;
theorem
:: CLVECT_1:91
for
V
being
ComplexLinearSpace
for
W1
,
W2
being
strict
Subspace
of
V
for
C1
being
Coset
of
W1
for
C2
being
Coset
of
W2
st
C1
=
C2
holds
W1
=
W2
proof
end;
theorem
:: CLVECT_1:92
for
V
being
ComplexLinearSpace
for
v
being
VECTOR
of
V
holds
{
v
}
is
Coset
of
(0).
V
proof
end;
theorem
:: CLVECT_1:93
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
is
Coset
of
(0).
V
holds
ex
v
being
VECTOR
of
V
st
V1
=
{
v
}
proof
end;
theorem
:: CLVECT_1:94
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
holds the
carrier
of
W
is
Coset
of
W
proof
end;
theorem
:: CLVECT_1:95
for
V
being
ComplexLinearSpace
holds the
carrier
of
V
is
Coset
of
(Omega).
V
proof
end;
theorem
:: CLVECT_1:96
for
V
being
ComplexLinearSpace
for
V1
being
Subset
of st
V1
is
Coset
of
(Omega).
V
holds
V1
=
the
carrier
of
V
proof
end;
theorem
:: CLVECT_1:97
for
V
being
ComplexLinearSpace
for
W
being
Subspace
of
V
for
C
being
Coset
of
W
holds
(
0.
V
in
C
iff
C
=
the
carrier
of
W
)
proof
end;
theorem
Th98
:
:: CLVECT_1:98
for
V
being
ComplexLinearSpace
for
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
C
being
Coset
of
W
holds
(
u
in
C
iff
C
=
u
+
W
)
proof
end;
theorem
:: CLVECT_1:99
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
C
being
Coset
of
W
st
u
in
C
&
v
in
C
holds
ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
u
+
v1
=
v
)
proof
end;
theorem
:: CLVECT_1:100
for
V
being
ComplexLinearSpace
for
u
,
v
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
C
being
Coset
of
W
st
u
in
C
&
v
in
C
holds
ex
v1
being
VECTOR
of
V
st
(
v1
in
W
&
u
-
v1
=
v
)
proof
end;
theorem
:: CLVECT_1:101
for
V
being
ComplexLinearSpace
for
v1
,
v2
being
VECTOR
of
V
for
W
being
Subspace
of
V
holds
( ex
C
being
Coset
of
W
st
(
v1
in
C
&
v2
in
C
) iff
v1
-
v2
in
W
)
proof
end;
theorem
:: CLVECT_1:102
for
V
being
ComplexLinearSpace
for
u
being
VECTOR
of
V
for
W
being
Subspace
of
V
for
B
,
C
being
Coset
of
W
st
u
in
B
&
u
in
C
holds
B
=
C
proof
end;
begin
definition
attr
c
1
is
strict
;
struct
CNORMSTR
->
CLSStruct
;
aggr
CNORMSTR
(#
carrier
,
ZeroF
,
addF
,
Mult
,
norm
#)
->
CNORMSTR
;
sel
norm
c
1
->
Function
of the
carrier
of
c
1
,
REAL
;
end;
registration
cluster
non
empty
CNORMSTR
;
existence
not for
b
1
being
CNORMSTR
holds
b
1
is
empty
proof
end;
end;
deffunc
H
1
(
CNORMSTR
)
->
Element
of the
carrier
of $1 =
0.
$1;
definition
let
X
be non
empty
CNORMSTR
;
let
x
be
Point
of ;
func
||.
x
.||
->
Real
equals
:: CLVECT_1:def 10
the
norm
of
X
.
x
;
coherence
the
norm
of
X
.
x
is
Real
;
end;
::
deftheorem
defines
||.
CLVECT_1:def 10 :
for
X
being non
empty
CNORMSTR
for
x
being
Point
of holds
||.
x
.||
=
the
norm
of
X
.
x
;
consider
V
being
ComplexLinearSpace
;
Lm6
: the
carrier
of
(
(0).
V
)
=
{
(
0.
V
)
}
by
Def6
;
reconsider
niltonil
= the
carrier
of
(
(0).
V
)
-->
0
as
Function
of the
carrier
of
(
(0).
V
)
,
REAL
by
FUNCOP_1:57
;
0.
V
is
VECTOR
of
(
(0).
V
)
by
Lm6
,
TARSKI:def 1
;
then
Lm7
:
niltonil
.
(
0.
V
)
=
0
by
FUNCOP_1:13
;
Lm8
: for
u
being
VECTOR
of
(
(0).
V
)
for
z
being
Complex
holds
niltonil
.
(
z
*
u
)
=
|.
z
.|
*
(
niltonil
.
u
)
proof
end;
Lm9
: for
u
,
v
being
VECTOR
of
(
(0).
V
)
holds
niltonil
.
(
u
+
v
)
<=
(
niltonil
.
u
)
+
(
niltonil
.
v
)
proof
end;
reconsider
X
=
CNORMSTR
(# the
carrier
of
(
(0).
V
)
,
(
0.
(
(0).
V
)
)
,the
addF
of
(
(0).
V
)
,the
Mult
of
(
(0).
V
)
,
niltonil
#) as non
empty
CNORMSTR
;
Lm10
:
now
let
x
,
y
be
Point
of ;
:: thesis:
for
z
being
Complex
holds
( (
||.
x
.||
=
0
implies
x
=
H
1
(
X
) ) & (
x
=
H
1
(
X
) implies
||.
x
.||
=
0
) &
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
&
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
)
let
z
be
Complex
;
:: thesis:
( (
||.
x
.||
=
0
implies
x
=
H
1
(
X
) ) & (
x
=
H
1
(
X
) implies
||.
x
.||
=
0
) &
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
&
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
)
reconsider
u
=
x
,
w
=
y
as
VECTOR
of
(
(0).
V
)
;
H
1
(
X
)
=
0.
V
by
Def5
;
hence
(
||.
x
.||
=
0
iff
x
=
H
1
(
X
) )
by
Lm6
,
FUNCOP_1:13
,
TARSKI:def 1
;
:: thesis:
(
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
&
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
)
z
*
x
=
z
*
u
;
hence
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
by
Lm8
;
:: thesis:
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
x
+
y
=
u
+
w
;
hence
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
by
Lm9
;
:: thesis:
verum
end;
definition
let
IT
be non
empty
CNORMSTR
;
attr
IT
is
ComplexNormSpace-like
means
:
Def11
:
:: CLVECT_1:def 11
for
x
,
y
being
Point
of
for
z
being
Complex
holds
( (
||.
x
.||
=
0
implies
x
=
0.
IT
) & (
x
=
0.
IT
implies
||.
x
.||
=
0
) &
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
&
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
);
end;
::
deftheorem
Def11
defines
ComplexNormSpace-like
CLVECT_1:def 11 :
for
IT
being non
empty
CNORMSTR
holds
(
IT
is
ComplexNormSpace-like
iff for
x
,
y
being
Point
of
for
z
being
Complex
holds
( (
||.
x
.||
=
0
implies
x
=
0.
IT
) & (
x
=
0.
IT
implies
||.
x
.||
=
0
) &
||.
(
z
*
x
)
.||
=
|.
z
.|
*
||.
x
.||
&
||.
(
x
+
y
)
.||
<=
||.
x
.||
+
||.
y
.||
) );
registration
cluster
non
empty
right_complementable
Abelian
add-associative
right_zeroed
ComplexLinearSpace-like
strict
ComplexNormSpace-like
CNORMSTR
;
existence
ex
b
1
being non
empty
CNORMSTR
st
(
b
1
is
ComplexNormSpace-like
&
b
1
is
ComplexLinearSpace-like
&
b
1
is
Abelian
&
b
1
is
add-associative
&
b
1
is
right_zeroed
&
b
1
is
right_complementable
&
b
1
is
strict
)
proof
end;
end;
definition
mode
ComplexNormSpace
is
non
empty
right_complementable
Abelian
add-associative
right_zeroed
ComplexLinearSpace-like
ComplexNormSpace-like
CNORMSTR
;
end;
theorem
:: CLVECT_1:103
for
CNS
being
ComplexNormSpace
holds
||.
(
0.
CNS
)
.||
=
0
by
Def11
;
theorem
Th104
:
:: CLVECT_1:104
for
CNS
being
ComplexNormSpace
for
x
being
Point
of holds
||.
(
-
x
)
.||
=
||.
x
.||
proof
end;
theorem
Th105
:
:: CLVECT_1:105
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
||.
(
x
-
y
)
.||
<=
||.
x
.||
+
||.
y
.||
proof
end;
theorem
Th106
:
:: CLVECT_1:106
for
CNS
being
ComplexNormSpace
for
x
being
Point
of holds
0
<=
||.
x
.||
proof
end;
theorem
:: CLVECT_1:107
for
z1
,
z2
being
Complex
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
||.
(
(
z1
*
x
)
+
(
z2
*
y
)
)
.||
<=
(
|.
z1
.|
*
||.
x
.||
)
+
(
|.
z2
.|
*
||.
y
.||
)
proof
end;
theorem
Th108
:
:: CLVECT_1:108
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
(
||.
(
x
-
y
)
.||
=
0
iff
x
=
y
)
proof
end;
theorem
Th109
:
:: CLVECT_1:109
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
||.
(
x
-
y
)
.||
=
||.
(
y
-
x
)
.||
proof
end;
theorem
Th110
:
:: CLVECT_1:110
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
||.
x
.||
-
||.
y
.||
<=
||.
(
x
-
y
)
.||
proof
end;
theorem
Th111
:
:: CLVECT_1:111
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of holds
abs
(
||.
x
.||
-
||.
y
.||
)
<=
||.
(
x
-
y
)
.||
proof
end;
theorem
Th112
:
:: CLVECT_1:112
for
CNS
being
ComplexNormSpace
for
x
,
w
,
y
being
Point
of holds
||.
(
x
-
w
)
.||
<=
||.
(
x
-
y
)
.||
+
||.
(
y
-
w
)
.||
proof
end;
theorem
:: CLVECT_1:113
for
CNS
being
ComplexNormSpace
for
x
,
y
being
Point
of st
x
<>
y
holds
||.
(
x
-
y
)
.||
<>
0
by
Th108
;
definition
canceled;
canceled;
canceled;
end;
::
deftheorem
CLVECT_1:def 12 :
canceled;
::
deftheorem
CLVECT_1:def 13 :
canceled;
::
deftheorem
CLVECT_1:def 14 :
canceled;
definition
let
CNS
be
ComplexLinearSpace
;
let
S
be
sequence
of
CNS
;
let
z
be
Complex
;
func
z
*
S
->
sequence
of
CNS
means
:
Def15
:
:: CLVECT_1:def 15
for
n
being
Element
of
NAT
holds
it
.
n
=
z
*
(
S
.
n
)
;
existence
ex
b
1
being
sequence
of
CNS
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
z
*
(
S
.
n
)
proof
end;
uniqueness
for
b
1
,
b
2
being
sequence
of
CNS
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
z
*
(
S
.
n
)
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
z
*
(
S
.
n
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def15
defines
*
CLVECT_1:def 15 :
for
CNS
being
ComplexLinearSpace
for
S
being
sequence
of
CNS
for
z
being
Complex
for
b
4
being
sequence
of
CNS
holds
(
b
4
=
z
*
S
iff for
n
being
Element
of
NAT
holds
b
4
.
n
=
z
*
(
S
.
n
)
);
definition
let
CNS
be
ComplexNormSpace
;
let
S
be
sequence
of
CNS
;
attr
S
is
convergent
means
:
Def16
:
:: CLVECT_1:def 16
ex
g
being
Point
of st
for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
g
)
.||
<
r
;
end;
::
deftheorem
Def16
defines
convergent
CLVECT_1:def 16 :
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
holds
(
S
is
convergent
iff ex
g
being
Point
of st
for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
g
)
.||
<
r
);
theorem
:: CLVECT_1:114
canceled;
theorem
Th115
:
:: CLVECT_1:115
for
CNS
being
ComplexNormSpace
for
S1
,
S2
being
sequence
of
CNS
st
S1
is
convergent
&
S2
is
convergent
holds
S1
+
S2
is
convergent
proof
end;
theorem
Th116
:
:: CLVECT_1:116
for
CNS
being
ComplexNormSpace
for
S1
,
S2
being
sequence
of
CNS
st
S1
is
convergent
&
S2
is
convergent
holds
S1
-
S2
is
convergent
proof
end;
theorem
Th117
:
:: CLVECT_1:117
for
CNS
being
ComplexNormSpace
for
x
being
Point
of
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
S
-
x
is
convergent
proof
end;
theorem
Th118
:
:: CLVECT_1:118
for
z
being
Complex
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
z
*
S
is
convergent
proof
end;
definition
let
CNS
be
ComplexNormSpace
;
let
S
be
sequence
of
CNS
;
func
||.
S
.||
->
Real_Sequence
means
:
Def17
:
:: CLVECT_1:def 17
for
n
being
Element
of
NAT
holds
it
.
n
=
||.
(
S
.
n
)
.||
;
existence
ex
b
1
being
Real_Sequence
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
||.
(
S
.
n
)
.||
proof
end;
uniqueness
for
b
1
,
b
2
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
||.
(
S
.
n
)
.||
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
||.
(
S
.
n
)
.||
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def17
defines
||.
CLVECT_1:def 17 :
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
for
b
3
being
Real_Sequence
holds
(
b
3
=
||.
S
.||
iff for
n
being
Element
of
NAT
holds
b
3
.
n
=
||.
(
S
.
n
)
.||
);
theorem
Th119
:
:: CLVECT_1:119
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
||.
S
.||
is
convergent
proof
end;
definition
let
CNS
be
ComplexNormSpace
;
let
S
be
sequence
of
CNS
;
assume
A1
:
S
is
convergent
;
func
lim
S
->
Point
of
means
:
Def18
:
:: CLVECT_1:def 18
for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
it
)
.||
<
r
;
existence
ex
b
1
being
Point
of st
for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
b
1
)
.||
<
r
by
A1
,
Def16
;
uniqueness
for
b
1
,
b
2
being
Point
of st ( for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
b
1
)
.||
<
r
) & ( for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
b
2
)
.||
<
r
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def18
defines
lim
CLVECT_1:def 18 :
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
for
b
3
being
Point
of holds
(
b
3
=
lim
S
iff for
r
being
Real
st
0
<
r
holds
ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
m
<=
n
holds
||.
(
(
S
.
n
)
-
b
3
)
.||
<
r
);
theorem
:: CLVECT_1:120
for
CNS
being
ComplexNormSpace
for
g
being
Point
of
for
S
being
sequence
of
CNS
st
S
is
convergent
&
lim
S
=
g
holds
(
||.
(
S
-
g
)
.||
is
convergent
&
lim
||.
(
S
-
g
)
.||
=
0
)
proof
end;
theorem
:: CLVECT_1:121
for
CNS
being
ComplexNormSpace
for
S1
,
S2
being
sequence
of
CNS
st
S1
is
convergent
&
S2
is
convergent
holds
lim
(
S1
+
S2
)
=
(
lim
S1
)
+
(
lim
S2
)
proof
end;
theorem
:: CLVECT_1:122
for
CNS
being
ComplexNormSpace
for
S1
,
S2
being
sequence
of
CNS
st
S1
is
convergent
&
S2
is
convergent
holds
lim
(
S1
-
S2
)
=
(
lim
S1
)
-
(
lim
S2
)
proof
end;
theorem
:: CLVECT_1:123
for
CNS
being
ComplexNormSpace
for
x
being
Point
of
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
lim
(
S
-
x
)
=
(
lim
S
)
-
x
proof
end;
theorem
:: CLVECT_1:124
for
z
being
Complex
for
CNS
being
ComplexNormSpace
for
S
being
sequence
of
CNS
st
S
is
convergent
holds
lim
(
z
*
S
)
=
z
*
(
lim
S
)
proof
end;