:: Complex Linear Space and Complex Normed Space
:: by Noboru Endou
::
:: Received January 26, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, RLVECT_1,
FUNCT_1, ZFMISC_1, XBOOLE_0, FUNCT_7, RELAT_1, ARYTM_3, COMPLEX1,
FUNCT_5, MCART_1, CARD_1, SUPINF_2, ARYTM_1, CARD_3, FINSEQ_1, XXREAL_0,
TARSKI, XCMPLX_0, RLSUB_1, REALSET1, NORMSP_1, PRE_TOPC, REAL_1,
FUNCOP_1, NAT_1, SEQ_2, ORDINAL2, CLVECT_1, NORMSP_0, METRIC_1, RELAT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, COMPLEX1, REAL_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1, FINSEQ_1, NAT_1,
FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1,
SEQ_2, NORMSP_0, NORMSP_1;
constructors BINOP_1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, REALSET1, NORMSP_1,
FUNCT_3, FUNCT_5, RELSET_1, FINSEQ_4, COMSEQ_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REALSET1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, NORMSP_0, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions STRUCT_0, RLVECT_1, TARSKI, XBOOLE_0, ALGSTR_0;
equalities STRUCT_0, XBOOLE_0, BINOP_1, REALSET1, ALGSTR_0, COMPLEX1,
NORMSP_0;
expansions STRUCT_0, RLVECT_1, TARSKI, XBOOLE_0, NORMSP_0;
theorems STRUCT_0, TARSKI, RLVECT_1, COMPLEX1, XCMPLX_0, FINSEQ_1, NAT_1,
FUNCT_1, XBOOLE_0, FUNCT_2, RELAT_1, XBOOLE_1, ZFMISC_1, RELSET_1,
ABSVALUE, SEQ_2, FUNCOP_1, XREAL_1, XXREAL_0, NORMSP_1, ALGSTR_0,
NORMSP_0, ORDINAL1;
schemes FUNCT_2, NAT_1, XBOOLE_0;
begin :: Complex Linear Space
definition
struct (addLoopStr) CLSStruct (# carrier -> set, ZeroF -> Element of the
carrier, addF -> BinOp of the carrier, Mult -> Function of [:COMPLEX, the
carrier:], the carrier #);
end;
registration
cluster non empty for CLSStruct;
existence
proof
set ZS = the non empty set,O = the Element of ZS,F = the BinOp of ZS,G =the
Function of [:COMPLEX,ZS:],ZS;
take CLSStruct(#ZS,O,F,G#);
thus the carrier of CLSStruct(#ZS,O,F,G#) is non empty;
end;
end;
definition
let V be CLSStruct;
mode VECTOR of V is Element of V;
end;
definition
let V be non empty CLSStruct, v be VECTOR of V, z be Complex;
func z * v -> Element of V equals
(the Mult of V).[z,v];
coherence
proof
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
(the Mult of V).[z,v] is Element of V;
hence thesis;
end;
end;
registration
let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function
of [:COMPLEX,ZS:],ZS;
cluster CLSStruct (# ZS,O,F,G #) -> non empty;
coherence;
end;
reserve a,b for Complex;
definition
let IT be non empty CLSStruct;
attr IT is vector-distributive means
:Def2: for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w;
attr IT is scalar-distributive means
:Def3: for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v;
attr IT is scalar-associative means
:Def4: for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attr IT is scalar-unital means
:Def5: for v being VECTOR of IT holds 1r * v = v;
end;
definition
func Trivial-CLSStruct -> strict CLSStruct equals
CLSStruct(#{0},op0,op2,pr2(COMPLEX,{0})#);
coherence;
end;
registration
cluster Trivial-CLSStruct -> 1-element;
coherence;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
for non empty CLSStruct;
existence
proof
take S = Trivial-CLSStruct;
thus S is strict;
thus S is Abelian
by STRUCT_0:def 10;
thus S is add-associative
by STRUCT_0:def 10;
thus S is right_zeroed
by STRUCT_0:def 10;
thus S is right_complementable
proof
let x be Element of S;
take x;
thus thesis by STRUCT_0:def 10;
end;
thus for a for v,w being VECTOR of S holds a * (v + w) = a * v + a * w by
STRUCT_0:def 10;
thus for a,b for v being VECTOR of S holds (a + b) * v = a * v + b * v by
STRUCT_0:def 10;
thus for a,b for v being VECTOR of S holds (a * b) * v = a * (b * v) by
STRUCT_0:def 10;
thus for v being VECTOR of S holds 1r * v = v by STRUCT_0:def 10;
end;
end;
definition
mode ComplexLinearSpace is Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty CLSStruct;
end;
::
:: Axioms of complex linear space.
::
reserve V,X,Y for ComplexLinearSpace;
reserve u,u1,u2,v,v1,v2 for VECTOR of V;
reserve z,z1,z2 for Complex;
theorem Th1:
z = 0 or v = 0.V implies z * v = 0.V
proof
assume
A1: z = 0 or v = 0.V;
now
per cases by A1;
suppose
A2: z = 0c;
v + 0c * v = 1r * v + 0c * v by Def5
.= (1r + 0c) * v by Def3
.= v by Def5
.= v + 0.V by RLVECT_1:4;
hence thesis by A2,RLVECT_1:8;
end;
suppose
A3: v = 0.V;
z * 0.V + z * 0.V = z * (0.V + 0.V) by Def2
.= z * 0.V by RLVECT_1:4
.= z * 0.V + 0.V by RLVECT_1:4;
hence thesis by A3,RLVECT_1:8;
end;
end;
hence thesis;
end;
theorem Th2:
z * v = 0.V implies z = 0 or v = 0.V
proof
assume that
A1: z * v = 0.V and
A2: z <> 0;
thus v = 1r * v by Def5
.= (z" * z) * v by A2,XCMPLX_0:def 7
.= z" * 0.V by A1,Def4
.= 0.V by Th1;
end;
theorem Th3:
- v = (- 1r) * v
proof
v + (- 1r) * v = 1r * v + (- 1r) * v by Def5
.= (1r + (- 1r)) * v by Def3
.= 0.V by Th1;
hence (- v) = (- v) + (v + (- 1r) * v) by RLVECT_1:4
.= ((- v) + v) + (- 1r) * v by RLVECT_1:def 3
.= 0.V + (- 1r) * v by RLVECT_1:5
.= (- 1r) * v by RLVECT_1:4;
end;
theorem Th4:
v = - v implies v = 0.V
proof
assume v = - v;
then 0.V = v - (- v) by RLVECT_1:15
.= v + v by RLVECT_1:17
.= 1r * v + v by Def5
.= 1r * v + 1r * v by Def5
.= (1r + 1r) * v by Def3;
hence thesis by Th2;
end;
theorem
v + v = 0.V implies v = 0.V
proof
assume v + v = 0.V;
then v = - v by RLVECT_1:def 10;
hence thesis by Th4;
end;
theorem Th6:
z * (- v) = (- z) * v
proof
thus z * (- v) = z * ((- 1r) * v) by Th3
.= (z *(- 1r)) * v by Def4
.= (- z) * v;
end;
theorem Th7:
z * (- v) = - (z * v)
proof
thus z * (- v) = (- (1r * z)) * v by Th6
.= ((- 1r) * z) * v
.= (- 1r) * (z * v) by Def4
.= - (z * v) by Th3;
end;
theorem
(- z) * (- v) = z * v
proof
thus (- z) * (- v) = (- (- z)) * v by Th6
.= z * v;
end;
theorem Th9:
z * (v - u) = z * v - z * u
proof
thus z * (v - u) = z * v + z * (- u) by Def2
.= z * v - z * u by Th7;
end;
theorem Th10:
(z1 - z2) * v = z1 * v - z2 * v
proof
thus (z1 - z2) * v = (z1 + (- z2)) * v .= z1 * v + (- z2) * v by Def3
.= z1 * v + z2 * (- v) by Th6
.= z1 * v - z2 * v by Th7;
end;
theorem
z <> 0 & z * v = z * u implies v = u
proof
assume that
A1: z <> 0 and
A2: z * v = z * u;
0.V = z * v - z * u by A2,RLVECT_1:15
.= z * (v - u) by Th9;
then v - u = 0.V by A1,Th2;
hence thesis by RLVECT_1:21;
end;
theorem
v <> 0.V & z1 * v = z2 * v implies z1 = z2
proof
assume that
A1: v <> 0.V and
A2: z1 * v = z2 * v;
0.V = z1 * v - z2 * v by A2,RLVECT_1:15
.= (z1 - z2) * v by Th10;
then (- z2) + z1 = 0 by A1,Th2;
hence thesis;
end;
Lm1: for V being non empty addLoopStr holds Sum(<*>(the carrier of V)) = 0.V
proof
let V be non empty addLoopStr;
set S = <*>(the carrier of V);
ex f being sequence of the carrier of V st Sum(S) = f.(len S) & f.0
= 0.V & for j being Nat, v being Element of V st j < len S & v = S.(
j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
hence thesis;
end;
Lm2: for V being non empty addLoopStr, F being FinSequence of the carrier of V
holds len F = 0 implies Sum(F) = 0.V
proof
let V be non empty addLoopStr;
let F be FinSequence of the carrier of V;
assume len F = 0;
then F = <*>(the carrier of V);
hence thesis by Lm1;
end;
theorem
for F,G being FinSequence of the carrier of V st len F = len G & (for
k being Nat,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
let F,G be FinSequence of the carrier of V;
defpred P[set] means for H,I being FinSequence of the carrier of V st len H
= len I & len H = $1 & (for k being Nat, v being VECTOR of V st k in
Seg len H & v = I.k holds H.k = z * v) holds Sum(H) = z * Sum(I);
A1: dom F = Seg len F by FINSEQ_1:def 3;
now
let n be Nat;
assume
A2: for H,I being FinSequence of the carrier of V st len H = len I &
len H = n & for k being Nat, v being VECTOR of V st k in Seg len H &
v = I.k holds H.k = z * v holds Sum(H) = z * Sum(I);
let H,I be FinSequence of the carrier of V;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Nat, v being VECTOR of V st k in Seg len H
& v = I.k holds H.k = z * v;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of the carrier
of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: len q = n by A3,A4,FINSEQ_1:17;
A8: len p = n by A4,A6,FINSEQ_1:17;
A9: now
len p <= len H by A4,A6,FINSEQ_1:17;
then
A10: Seg len p c= Seg len H by FINSEQ_1:5;
A11: dom p = Seg n by A4,A6,FINSEQ_1:17;
let k be Nat;
let v be VECTOR of V;
assume that
A12: k in Seg len p and
A13: v = q.k;
dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
then I.k = q.k by A8,A12,FUNCT_1:47;
then H.k = z * v by A5,A12,A13,A10;
hence p.k = z * v by A8,A12,A11,FUNCT_1:47;
end;
n + 1 in Seg(n + 1) by FINSEQ_1:4;
then n +1 in dom H & n +1 in dom I by A3,A4,FINSEQ_1:def 3;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as VECTOR of V by FUNCT_1:102
;
A14: v1 = z * v2 by A4,A5,FINSEQ_1:4;
A15: dom q = Seg len q by FINSEQ_1:def 3;
dom p = Seg len p by FINSEQ_1:def 3;
hence Sum(H) = Sum(p) + v1 by A4,A8,RLVECT_1:38
.= z * Sum(q) + z * v2 by A2,A8,A7,A9,A14
.= z * (Sum(q) + v2) by Def2
.= z * Sum(I) by A3,A4,A7,A15,RLVECT_1:38;
end;
then
A16: for n being Nat st P[n] holds P[n+1];
now
let H,I be FinSequence of the carrier of V;
assume that
A17: len H = len I and
A18: len H = 0 and
for k being Nat,v being VECTOR of V st k in Seg len H & v =
I.k holds H.k = z * v;
Sum(H) = 0.V by A18,Lm2;
hence Sum(H) = z * Sum(I) by A17,A18,Lm2,Th1;
end;
then
A19: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A19,A16);
hence thesis by A1;
end;
theorem
z * Sum(<*>(the carrier of V)) = 0.V by Lm1,Th1;
theorem
z * Sum<* v,u *> = z * v + z * u
proof
thus z * Sum<* v,u *> = z * (v + u) by RLVECT_1:45
.= z * v + z * u by Def2;
end;
theorem
z * Sum<* u,v1,v2 *> = z * u + z * v1 + z * v2
proof
thus z * Sum<* u,v1,v2 *> = z * (u + v1 + v2) by RLVECT_1:46
.= z * (u + v1) + z * v2 by Def2
.= z * u + z * v1 + z * v2 by Def2;
end;
theorem Th17:
Sum<* v,v *> = (1r+1r) * v
proof
thus Sum<* v,v *> = v + v by RLVECT_1:45
.= 1r * v + v by Def5
.= 1r * v + 1r * v by Def5
.= (1r+1r) * v by Def3;
end;
theorem
Sum<* - v,- v *> = (-(1r+1r)) * v
proof
reconsider 2r = 2+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum<* - v,- v *> = - (v + v) by RLVECT_1:60
.= - Sum<* v,v *> by RLVECT_1:45
.= - ((1r+1r) * v) by Th17
.= (- 1r) * (2r * v) by Th3
.= ((- 1r) * 2r) * v by Def4
.= (-(1r+1r)) * v;
end;
theorem
Sum<* v,v,v *> = (1r+1r+1r) * v
proof
reconsider 2r = 2+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum<* v,v,v *> = Sum<* v,v *> + v by RLVECT_1:66
.= (1r+1r) * v + v by Th17
.= (1r+1r) * v + 1r * v by Def5
.= (1r+1r+1r) * v by Def3;
end;
begin :: Subspace and Cosets of Subspaces in Complex Linear Space
reserve V1,V2,V3 for Subset of V;
definition
let V, V1;
attr V1 is linearly-closed means
(for v,u being VECTOR of V st v in V1 & u in V1 holds v + u in V1) &
for z being Complex, v being VECTOR of V st v in V1 holds z * v in V1;
end;
theorem Th20:
V1 <> {} & V1 is linearly-closed implies 0.V in V1
proof
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
set x = the Element of V1;
reconsider x as Element of V by A1,TARSKI:def 3;
0c * x in V1 by A1,A2;
hence thesis by Th1;
end;
theorem Th21:
V1 is linearly-closed implies for v being VECTOR of V st v in V1
holds - v in V1
proof
assume
A1: V1 is linearly-closed;
let v be VECTOR of V;
assume v in V1;
then (- 1r) * v in V1 by A1;
hence thesis by Th3;
end;
theorem
V1 is linearly-closed implies for v,u being VECTOR of V st v in V1 & u
in V1 holds v - u in V1
proof
assume
A1: V1 is linearly-closed;
let v,u be VECTOR of V;
assume that
A2: v in V1 and
A3: u in V1;
- u in V1 by A1,A3,Th21;
hence thesis by A1,A2;
end;
theorem Th23:
{0.V} is linearly-closed
proof
thus for v,u being VECTOR of V st v in {0.V} & u in {0.V} holds v + u in {0.
V}
proof
let v,u be VECTOR of V;
assume v in {0.V} & u in {0.V};
then v = 0.V & u = 0.V by TARSKI:def 1;
then v + u = 0.V by RLVECT_1:4;
hence thesis by TARSKI:def 1;
end;
let z;
let v be VECTOR of V;
assume
A1: v in {0.V};
then v = 0.V by TARSKI:def 1;
hence thesis by A1,Th1;
end;
theorem
the carrier of V = V1 implies V1 is linearly-closed;
theorem
V1 is linearly-closed & V2 is linearly-closed & V3 = {v + u : v in V1
& u in V2} implies V3 is linearly-closed
proof
assume that
A1: V1 is linearly-closed & V2 is linearly-closed and
A2: V3 = {v + u: v in V1 & u in V2};
thus for v,u being VECTOR of V st v in V3 & u in V3 holds v + u in V3
proof
let v,u be VECTOR of V;
assume that
A3: v in V3 and
A4: u in V3;
consider v2,v1 be VECTOR of V such that
A5: v = v1 + v2 and
A6: v1 in V1 & v2 in V2 by A2,A3;
consider u2,u1 be VECTOR of V such that
A7: u = u1 + u2 and
A8: u1 in V1 & u2 in V2 by A2,A4;
A9: v + u = ((v1 + v2) + u1) + u2 by A5,A7,RLVECT_1:def 3
.= ((v1 + u1) + v2) + u2 by RLVECT_1:def 3
.= (v1 + u1) + (v2 + u2) by RLVECT_1:def 3;
v1 + u1 in V1 & v2 + u2 in V2 by A1,A6,A8;
hence thesis by A2,A9;
end;
let z be Complex, v be VECTOR of V;
assume v in V3;
then consider v2,v1 be VECTOR of V such that
A10: v = v1 + v2 and
A11: v1 in V1 & v2 in V2 by A2;
A12: z * v = z * v1 + z * v2 by A10,Def2;
z * v1 in V1 & z * v2 in V2 by A1,A11;
hence thesis by A2,A12;
end;
theorem
V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is
linearly-closed
proof
assume that
A1: V1 is linearly-closed and
A2: V2 is linearly-closed;
thus for v,u being VECTOR of V st v in V1 /\ V2 & u in V1 /\ V2 holds v + u
in V1 /\ V2
proof
let v,u be VECTOR of V;
assume
A3: v in V1 /\ V2 & u in V1 /\ V2;
then v in V2 & u in V2 by XBOOLE_0:def 4;
then
A4: v + u in V2 by A2;
v in V1 & u in V1 by A3,XBOOLE_0:def 4;
then v + u in V1 by A1;
hence thesis by A4,XBOOLE_0:def 4;
end;
let z be Complex, v be VECTOR of V;
assume
A5: v in V1 /\ V2;
then v in V2 by XBOOLE_0:def 4;
then
A6: z * v in V2 by A2;
v in V1 by A5,XBOOLE_0:def 4;
then z * v in V1 by A1;
hence thesis by A6,XBOOLE_0:def 4;
end;
definition
let V;
mode Subspace of V -> ComplexLinearSpace means
:Def8:
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
proof
the addF of V = (the addF of V)||the carrier of V & the Mult of V = (
the Mult of V) | [:COMPLEX, the carrier of V:] by RELSET_1:19;
hence thesis;
end;
end;
:: Axioms of the subspaces of real linear spaces.
reserve W,W1,W2 for Subspace of V;
reserve x for set;
reserve w,w1,w2 for VECTOR of W;
theorem
x in W1 & W1 is Subspace of W2 implies x in W2
proof
assume x in W1 & W1 is Subspace of W2;
then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def8;
hence thesis;
end;
theorem Th28:
for x being object holds x in W implies x in V
proof let x be object;
assume x in W;
then
A1: x in the carrier of W;
the carrier of W c= the carrier of V by Def8;
hence thesis by A1;
end;
theorem Th29:
w is VECTOR of V
proof
w in V by Th28,RLVECT_1:1;
hence thesis;
end;
theorem
0.W = 0.V by Def8;
theorem
0.W1 = 0.W2
proof
thus 0.W1 = 0.V by Def8
.= 0.W2 by Def8;
end;
theorem Th32:
w1 = v & w2 = u implies w1 + w2 = v + u
proof
assume
A1: v = w1 & u = w2;
w1 + w2 = ((the addF of V)||the carrier of W).[w1,w2] by Def8;
hence thesis by A1,FUNCT_1:49;
end;
theorem Th33:
w = v implies z * w = z * v
proof
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
z * w = ((the Mult of V) | [:COMPLEX, the carrier of W:]).[z,w] by Def8;
hence thesis by FUNCT_1:49;
end;
theorem Th34:
w = v implies - v = - w
proof
assume
A1: w = v;
- v = (- 1r) * v & - w = (- 1r) * w by Th3;
hence thesis by A1,Th33;
end;
theorem Th35:
w1 = v & w2 = u implies w1 - w2 = v - u
proof
assume that
A1: w1 = v and
A2: w2 = u;
- w2 = - u by A2,Th34;
hence thesis by A1,Th32;
end;
Lm3: the carrier of W = V1 implies V1 is linearly-closed
proof
set VW = the carrier of W;
reconsider WW = W as ComplexLinearSpace;
assume
A1: the carrier of W = V1;
thus for v,u st v in V1 & u in V1 holds v + u in V1
proof
let v,u;
assume v in V1 & u in V1;
then reconsider vv = v, uu = u as VECTOR of WW by A1;
reconsider vw = vv + uu as Element of VW;
vw in V1 by A1;
hence thesis by Th32;
end;
let z,v;
assume v in V1;
then reconsider vv = v as VECTOR of WW by A1;
reconsider vw = z * vv as Element of VW;
vw in V1 by A1;
hence thesis by Th33;
end;
theorem Th36:
0.V in W
proof
0.W in W;
hence thesis by Def8;
end;
theorem
0.W1 in W2
proof
0.W1 = 0.V by Def8;
hence thesis by Th36;
end;
theorem
0.W in V by Th28,RLVECT_1:1;
theorem Th39:
u in W & v in W implies u + v in W
proof
reconsider VW = the carrier of W as Subset of V by Def8;
assume u in W & v in W;
then
A1: u in the carrier of W & v in the carrier of W;
VW is linearly-closed by Lm3;
then u + v in the carrier of W by A1;
hence thesis;
end;
theorem Th40:
v in W implies z * v in W
proof
reconsider VW = the carrier of W as Subset of V by Def8;
assume v in W;
then
A1: v in the carrier of W;
VW is linearly-closed by Lm3;
then z * v in the carrier of W by A1;
hence thesis;
end;
theorem Th41:
v in W implies - v in W
proof
assume v in W;
then (- 1r) * v in W by Th40;
hence thesis by Th3;
end;
theorem Th42:
u in W & v in W implies u - v in W
proof
assume
A1: u in W;
assume v in W;
then - v in W by Th41;
hence thesis by A1,Th39;
end;
reserve D for non empty set;
reserve d1 for Element of D;
reserve A for BinOp of D;
reserve M for Function of [:COMPLEX,D:],D;
Lm4: now
let V,V1,D,d1,A,M,z;
let w be VECTOR of CLSStruct (# D,d1,A,M #);
let v be Element of V;
assume that
A1: V1 = D and
A2: M = (the Mult of V) | [:COMPLEX,V1:] and
A3: w = v;
z in COMPLEX by XCMPLX_0:def 2;
then [z,w] in [:COMPLEX,V1:] by A1,ZFMISC_1:def 2;
hence z*w = z*v by A3,A2,FUNCT_1:49;
end;
theorem Th43:
V1 = D & d1 = 0.V & A = (the addF of V)||V1 &
M = (the Mult of V) | [:COMPLEX,V1:] implies
CLSStruct (# D,d1,A,M #) is Subspace of V
proof
assume that
A1: V1 = D and
A2: d1 = 0.V and
A3: A = (the addF of V)||V1 and
A4: M = (the Mult of V) | [:COMPLEX,V1:];
set W = CLSStruct (# D,d1,A,M #);
A5: for x,y being VECTOR of W holds x + y = (the addF of V).[x,y] by A1,A3,
FUNCT_1:49;
A6: W is Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
proof
set MV = the Mult of V;
set AV = the addF of V;
thus for x,y being VECTOR of W holds x + y = y + x
proof
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
thus x + y = x1 + y1 by A5
.= y1 + x1
.= y + x by A5;
end;
thus for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1,TARSKI:def 3;
thus (x + y) + z = AV.[x + y,z1] by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= AV.[x1,y + z] by A5
.= x + (y + z) by A5;
end;
thus for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
thus x + 0.W = y + 0.V by A2,A5
.= x by RLVECT_1:4;
end;
thus W is right_complementable
proof
let x be VECTOR of W;
reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3;
consider v such that
A7: x1 + v = 0.V by ALGSTR_0:def 11;
reconsider mj=-1r as Element of COMPLEX by XCMPLX_0:def 2;
v = - x1 by A7,RLVECT_1:def 10
.= (- 1r) * x1 by Th3
.= MV.[mj,x]
.= (- 1r) * x by A1,A4,FUNCT_1:49;
then reconsider y = v as VECTOR of W;
take y;
thus thesis by A2,A5,A7;
end;
thus for z for x,y being VECTOR of W holds z * (x + y) = z * x + z * y
proof
let z;
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
A8: z*x1 = z*x & z*y1 = z*y by A1,A4,Lm4;
thus z * (x + y) = z * (x1 + y1) by A1,A4,A5,Lm4
.= z * x1 + z * y1 by Def2
.= z * x + z * y by A5,A8;
end;
thus for z1,z2 for x being VECTOR of W holds (z1 + z2) * x = z1*x + z2*x
proof
let z1,z2;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
A9: z1*y = z1*x & z2*y = z2*x by A1,A4,Lm4;
thus (z1 + z2) * x = (z1 + z2) * y by A1,A4,Lm4
.= z1 * y + z2 * y by Def3
.= z1 * x + z2 * x by A5,A9;
end;
thus for z1,z2 for x being VECTOR of W holds (z1 * z2) * x = z1 * (z2 * x)
proof
let z1,z2;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
A10: z2*y = z2*x by A1,A4,Lm4;
thus (z1 * z2) * x = (z1 * z2) * y by A1,A4,Lm4
.= z1 * (z2 * y) by Def4
.= z1 * (z2 * x) by A1,A4,A10,Lm4;
end;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
thus 1r * x = 1r * y by A1,A4,Lm4
.= x by Def5;
end;
0.W = 0.V by A2;
hence thesis by A1,A3,A4,A6,Def8;
end;
theorem Th44:
V is Subspace of V
proof
thus the carrier of V c= the carrier of V & 0.V = 0.V;
thus thesis by RELSET_1:19;
end;
theorem Th45:
for V,X being strict ComplexLinearSpace holds V is Subspace of X
& X is Subspace of V implies V = X
proof
let V,X be strict ComplexLinearSpace;
assume that
A1: V is Subspace of X and
A2: X is Subspace of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX & VX c= VV by A1,A2,Def8;
then
A3: VV = VX;
set AX = the addF of X;
set AV = the addF of V;
AV = AX||VV & AX = AV||VX by A1,A2,Def8;
then
A4: AV = AX by A3,RELAT_1:72;
set MX = the Mult of X;
set MV = the Mult of V;
A5: MX = MV | [:COMPLEX,VX:] by A2,Def8;
0.V = 0.X & MV = MX | [:COMPLEX,VV:] by A1,Def8;
hence thesis by A3,A4,A5,RELAT_1:72;
end;
theorem Th46:
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y
proof
assume that
A1: V is Subspace of X and
A2: X is Subspace of Y;
the carrier of V c= the carrier of X & the carrier of X c= the carrier
of Y by A1,A2,Def8;
hence the carrier of V c= the carrier of Y;
0.V = 0.X by A1,Def8;
hence 0.V = 0.Y by A2,Def8;
thus the addF of V = (the addF of Y)||the carrier of V
proof
set AY = the addF of Y;
set VX = the carrier of X;
set AX = the addF of X;
set VV = the carrier of V;
set AV = the addF of V;
VV c= VX by A1,Def8;
then
A3: [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:96;
AV = AX||VV by A1,Def8;
then AV = AY||VX||VV by A2,Def8;
hence thesis by A3,FUNCT_1:51;
end;
set MY = the Mult of Y;
set MX = the Mult of X;
set MV = the Mult of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX by A1,Def8;
then
A4: [:COMPLEX,VV:] c= [:COMPLEX,VX:] by ZFMISC_1:95;
MV = MX | [:COMPLEX,VV:] by A1,Def8;
then MV = (MY | [:COMPLEX,VX:]) | [:COMPLEX,VV:] by A2,Def8;
hence thesis by A4,FUNCT_1:51;
end;
theorem Th47:
the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2
proof
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
set AV = the addF of V;
set MV = the Mult of V;
assume
A1: the carrier of W1 c= the carrier of W2;
then
A2: [:VW1,VW1:] c= [:VW2,VW2:] by ZFMISC_1:96;
0.W1 = 0.V by Def8;
hence the carrier of W1 c= the carrier of W2 & 0.W1 = 0.W2 by A1,Def8;
the addF of W1 = AV||VW1 & the addF of W2 = AV||VW2 by Def8;
hence the addF of W1 = (the addF of W2)||the carrier of W1 by A2,FUNCT_1:51;
A3: [:COMPLEX,VW1:] c= [:COMPLEX,VW2:] by A1,ZFMISC_1:95;
the Mult of W1 = MV | [:COMPLEX,VW1:] & the Mult of W2 = MV | [:COMPLEX,
VW2 :] by Def8;
hence thesis by A3,FUNCT_1:51;
end;
theorem
(for v st v in W1 holds v in W2) implies W1 is Subspace of W2
proof
assume
A1: for v st v in W1 holds v in W2;
the carrier of W1 c= the carrier of W2
proof
let x be object;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2;
then v in W2 by A1;
hence thesis;
end;
hence thesis by Th47;
end;
registration
let V;
cluster strict for Subspace of V;
existence
proof
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider V1 = the carrier of V as Subset of V;
the addF of V = (the addF of V)||V1 & the Mult of V = (the Mult of V)
| [: COMPLEX,V1:] by RELSET_1:19;
then CLSStruct(#the carrier of V,0.V,the addF of V,the Mult of V #) is
Subspace of V by Th43;
hence thesis;
end;
end;
theorem Th49:
for W1,W2 being strict Subspace of V holds the carrier of W1 =
the carrier of W2 implies W1 = W2
proof
let W1,W2 be strict Subspace of V;
assume the carrier of W1 = the carrier of W2;
then W1 is Subspace of W2 & W2 is Subspace of W1 by Th47;
hence thesis by Th45;
end;
theorem Th50:
for W1,W2 being strict Subspace of V holds (for v holds v in W1
iff v in W2) implies W1 = W2
proof
let W1,W2 be strict Subspace of V;
assume
A1: for v holds v in W1 iff v in W2;
for x being object holds x in the carrier of W1 iff x in the carrier of W2
proof let x be object;
thus x in the carrier of W1 implies x in the carrier of W2
proof
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2;
then v in W2 by A1;
hence thesis;
end;
assume
A3: x in the carrier of W2;
the carrier of W2 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A3;
v in W2 by A3;
then v in W1 by A1;
hence thesis;
end;
then the carrier of W1 = the carrier of W2 by TARSKI:2;
hence thesis by Th49;
end;
theorem
for V being strict ComplexLinearSpace, W being strict Subspace of V
holds the carrier of W = the carrier of V implies W = V
proof
let V be strict ComplexLinearSpace, W be strict Subspace of V;
assume
A1: the carrier of W = the carrier of V;
V is Subspace of V by Th44;
hence thesis by A1,Th49;
end;
theorem
for V being strict ComplexLinearSpace, W being strict Subspace of V
holds (for v being VECTOR of V holds v in W iff v in V) implies W = V
proof
let V be strict ComplexLinearSpace, W be strict Subspace of V;
assume
A1: for v being VECTOR of V holds v in W iff v in V;
V is Subspace of V by Th44;
hence thesis by A1,Th50;
end;
theorem
the carrier of W = V1 implies V1 is linearly-closed by Lm3;
theorem Th54:
V1 <> {} & V1 is linearly-closed implies ex W being strict
Subspace of V st V1 = the carrier of W
proof
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
reconsider D = V1 as non empty set by A1;
set M = (the Mult of V) | [:COMPLEX,V1:];
set VV = the carrier of V;
dom(the Mult of V) = [:COMPLEX,VV:] by FUNCT_2:def 1;
then
A3: dom M = [:COMPLEX,VV:] /\ [:COMPLEX,V1:] by RELAT_1:61;
[:COMPLEX,V1:] c= [:COMPLEX ,VV:] by ZFMISC_1:95;
then
A4: dom M = [:COMPLEX,D:] by A3,XBOOLE_1:28;
now
let y be object;
thus y in D implies ex x being object st x in dom M & y = M.x
proof
assume
A5: y in D;
then reconsider v1 = y as Element of VV;
A6: [1r,y] in [:COMPLEX,D:] by A5,ZFMISC_1:87;
then M.[1r,y] = 1r * v1 by FUNCT_1:49
.= y by Def5;
hence thesis by A4,A6;
end;
given x being object such that
A7: x in dom M and
A8: y = M.x;
consider x1,x2 being object such that
A9: x1 in COMPLEX and
A10: x2 in D and
A11: x = [x1,x2] by A4,A7,ZFMISC_1:def 2;
reconsider xx1 = x1 as Element of COMPLEX by A9;
reconsider v2 = x2 as Element of VV by A10;
[x1,x2] in [:COMPLEX,V1:] by A9,A10,ZFMISC_1:87;
then y = xx1 * v2 by A8,A11,FUNCT_1:49;
hence y in D by A2,A10;
end;
then D = rng M by FUNCT_1:def 3;
then reconsider M as Function of [:COMPLEX,D:],D by A4,FUNCT_2:def 1
,RELSET_1:4;
set A = (the addF of V)||V1;
reconsider d1 = 0.V as Element of D by A2,Th20;
dom(the addF of V) = [:VV,VV:] by FUNCT_2:def 1;
then dom A = [:VV,VV:] /\ [:V1,V1:] by RELAT_1:61;
then
A12: dom A = [:D,D:] by XBOOLE_1:28,ZFMISC_1:96;
now
let y be object;
thus y in D implies ex x being object st x in dom A & y = A.x
proof
assume
A13: y in D;
then reconsider v1 = y, v0 = d1 as Element of VV;
A14: [d1,y] in [:D,D:] by A13,ZFMISC_1:87;
then A.[d1,y] = v0 + v1 by FUNCT_1:49
.= y by RLVECT_1:4;
hence thesis by A12,A14;
end;
given x being object such that
A15: x in dom A and
A16: y = A.x;
consider x1,x2 being object such that
A17: x1 in D & x2 in D and
A18: x = [x1,x2] by A12,A15,ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Element of VV by A17;
[x1,x2] in [:V1,V1:] by A17,ZFMISC_1:87;
then y = v1 + v2 by A16,A18,FUNCT_1:49;
hence y in D by A2,A17;
end;
then D = rng A by FUNCT_1:def 3;
then reconsider A as Function of [:D,D:],D by A12,FUNCT_2:def 1,RELSET_1:4;
set W = CLSStruct (# D,d1,A,M #);
W is Subspace of V by Th43;
hence thesis;
end;
:: Definition of zero subspace and improper subspace of complex linear space.
definition
let V;
func (0).V -> strict Subspace of V means
:Def9:
the carrier of it = {0.V};
correctness by Th23,Th49,Th54;
end;
definition
let V;
func (Omega).V -> strict Subspace of V equals
the CLSStruct of V;
coherence
proof
set W = the CLSStruct of V;
A1: for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of W;
reconsider u9=u,v9=v,w9=w as VECTOR of V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
A2: for v being VECTOR of W holds v + 0.W = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus v + 0.W = v9 + 0.V .= v by RLVECT_1:4;
end;
A3: W is right_complementable
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
consider w9 being VECTOR of V such that
A4: v9 + w9 = 0.V by ALGSTR_0:def 11;
reconsider w=w9 as VECTOR of W;
take w;
thus thesis by A4;
end;
A5: for z1,z2 for v being VECTOR of W holds (z1 * z2) * v = z1 * (z2 * v )
proof
let z1,z2;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (z1 * z2) * v = (z1 * z2) * v9 .= z1 * (z2 * v9) by Def4
.= z1 * (z2 * v);
end;
A6: for z1,z2 for v being VECTOR of W holds (z1+z2) * v = z1* v + z2* v
proof
let z1,z2;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (z1 + z2) * v = (z1 + z2) * v9 .= z1 * v9 + z2 * v9 by Def3
.= z1 * v + z2 * v;
end;
A7: for z for v,w being VECTOR of W holds z * (v + w) = z * v + z * w
proof
let z;
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
thus z * (v + w) = z * (v9 + w9) .= z * v9 + z * w9 by Def2
.= z * v + z * w;
end;
A8: for z for v,w be VECTOR of W, v9,w9 be VECTOR of V st v=v9 & w=w9
holds v+w = v9+w9 & z*v = z*v9;
A9: for v,w being VECTOR of W holds v + w = w + v
proof
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
thus v + w = w9 + v9 by A8
.= w + v;
end;
for v being VECTOR of W holds 1r * v = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus 1r * v = 1r * v9 .= v by Def5;
end;
then reconsider W as ComplexLinearSpace
by A9,A1,A2,A3,A7,A6,A5,Def2,Def3,Def4,Def5,RLVECT_1:def 2,def 3,def 4;
A10: the Mult of W = (the Mult of V) | [:COMPLEX, the carrier of W:] by
RELSET_1:19;
0.W = 0.V & the addF of W = (the addF of V)||the carrier of W by
RELSET_1:19;
hence thesis by A10,Def8;
end;
end;
:: Definitional theorems of zero subspace and improper subspace.
theorem Th55:
(0).W = (0).V
proof
the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def9;
then
A1: the carrier of (0).W = the carrier of (0).V by Def8;
(0).W is Subspace of V by Th46;
hence thesis by A1,Th49;
end;
theorem Th56:
(0).W1 = (0).W2
proof
(0).W1 = (0).V by Th55;
hence thesis by Th55;
end;
theorem
(0).W is Subspace of V by Th46;
theorem
(0).V is Subspace of W
proof
the carrier of (0).V = {0.V} by Def9
.= {0.W} by Def8;
hence thesis by Th47;
end;
theorem
(0).W1 is Subspace of W2
proof
(0).W1 = (0).W2 by Th56;
hence thesis;
end;
theorem
for V being strict ComplexLinearSpace holds V is Subspace of (Omega).V;
:: Introduction of the cosets of subspace.
definition
let V;
let v,W;
func v + W -> Subset of V equals
{v + u : u in W};
coherence
proof
set Y = {v + u : u in W};
defpred P[object] means ex u st $1 = v + u & u in W;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of V & P[x] from
XBOOLE_0:sch 1;
X c= the carrier of V
by A1;
then reconsider X as Subset of V;
A2: Y c= X
proof
let x be object;
assume x in Y;
then ex u st x = v + u & u in W;
hence thesis by A1;
end;
X c= Y
proof
let x be object;
assume x in X;
then ex u st x = v + u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
Lm5: 0.V + W = the carrier of W
proof
set A = {0.V + u : u in W};
A1: the carrier of W c= A
proof
let x be object;
assume x in the carrier of W;
then
A2: x in W;
then x in V by Th28;
then reconsider y = x as Element of V;
0.V + y = x by RLVECT_1:4;
hence thesis by A2;
end;
A c= the carrier of W
proof
let x be object;
assume x in A;
then consider u such that
A3: x = 0.V + u and
A4: u in W;
x = u by A3,RLVECT_1:4;
hence thesis by A4;
end;
hence thesis by A1;
end;
definition
let V;
let W;
mode Coset of W -> Subset of V means
:Def12:
ex v st it = v + W;
existence
proof
reconsider VW = the carrier of W as Subset of V by Def8;
take VW;
take 0.V;
thus thesis by Lm5;
end;
end;
reserve B,C for Coset of W;
:: Definitional theorems of the cosets.
theorem Th61:
0.V in v + W iff v in W
proof
thus 0.V in v + W implies v in W
proof
assume 0.V in v + W;
then consider u such that
A1: 0.V = v + u and
A2: u in W;
v = - u by A1,RLVECT_1:def 10;
hence thesis by A2,Th41;
end;
assume v in W;
then
A3: - v in W by Th41;
0.V = v - v by RLVECT_1:15
.= v + (- v);
hence thesis by A3;
end;
theorem Th62:
v in v + W
proof
v + 0.V = v & 0.V in W by Th36,RLVECT_1:4;
hence thesis;
end;
theorem
0.V + W = the carrier of W by Lm5;
theorem Th64:
v + (0).V = {v}
proof
thus v + (0).V c= {v}
proof
let x be object;
assume x in v + (0).V;
then consider u such that
A1: x = v + u and
A2: u in (0).V;
A3: the carrier of (0).V = {0.V} by Def9;
u in the carrier of (0).V by A2;
then u = 0.V by A3,TARSKI:def 1;
then x = v by A1,RLVECT_1:4;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {v};
then
A4: x = v by TARSKI:def 1;
0.V in (0).V & v = v + 0.V by Th36,RLVECT_1:4;
hence thesis by A4;
end;
Lm6: v in W iff v + W = the carrier of W
proof
0.V in W & v + 0.V = v by Th36,RLVECT_1:4;
then
A1: v in {v + u : u in W};
thus v in W implies v + W = the carrier of W
proof
assume
A2: v in W;
thus v + W c= the carrier of W
proof
let x be object;
assume x in v + W;
then consider u such that
A3: x = v + u and
A4: u in W;
v + u in W by A2,A4,Th39;
hence thesis by A3;
end;
let x be object;
assume x in the carrier of W;
then reconsider y = x, z = v as Element of W by A2;
reconsider y1 = y, z1 = z as VECTOR of V by Th29;
A5: z + (y - z) = (y + z) - z by RLVECT_1:def 3
.= y + (z - z) by RLVECT_1:def 3
.= y + 0.W by RLVECT_1:15
.= x by RLVECT_1:4;
y - z in W;
then
A6: y1 - z1 in W by Th35;
y - z = y1 - z1 by Th35;
then z1 + (y1 - z1) = x by A5,Th32;
hence thesis by A6;
end;
assume
A7: v + W = the carrier of W;
assume not v in W;
hence thesis by A7,A1;
end;
theorem Th65:
v + (Omega).V = the carrier of V
by STRUCT_0:def 5,Lm6;
theorem Th66:
0.V in v + W iff v + W = the carrier of W
by Th61,Lm6;
theorem
v in W iff v + W = the carrier of W by Lm6;
theorem Th68:
v in W implies (z * v) + W = the carrier of W
proof
assume
A1: v in W;
thus (z * v) + W c= the carrier of W
proof
let x be object;
assume x in (z * v) + W;
then consider u such that
A2: x = z * v + u and
A3: u in W;
z * v in W by A1,Th40;
then z * v + u in W by A3,Th39;
hence thesis by A2;
end;
let x be object;
assume
A4: x in the carrier of W;
then
A5: x in W;
the carrier of W c= the carrier of V by Def8;
then reconsider y = x as Element of V by A4;
A6: z * v + (y - z * v) = (y + z * v) - z * v by RLVECT_1:def 3
.= y + (z * v - z * v) by RLVECT_1:def 3
.= y + 0.V by RLVECT_1:15
.= x by RLVECT_1:4;
z * v in W by A1,Th40;
then y - z * v in W by A5,Th42;
hence thesis by A6;
end;
theorem Th69:
z <> 0 & (z * v) + W = the carrier of W implies v in W
proof
assume that
A1: z <> 0 and
A2: (z * v) + W = the carrier of W;
assume not v in W;
then not 1r * v in W by Def5;
then not (z" * z) * v in W by A1,XCMPLX_0:def 7;
then not z" * (z * v) in W by Def4;
then
A3: not z * v in W by Th40;
0.V in W & z * v + 0.V = z * v by Th36,RLVECT_1:4;
then z * v in {z * v + u : u in W};
hence contradiction by A2,A3;
end;
theorem Th70:
v in W iff - v + W = the carrier of W
proof
v in W iff ((- 1r) * v) + W = the carrier of W by Th68,Th69;
hence thesis by Th3;
end;
theorem Th71:
u in W iff v + W = (v + u) + W
proof
thus u in W implies v + W = (v + u) + W
proof
assume
A1: u in W;
thus v + W c= (v + u) + W
proof
let x be object;
assume x in v + W;
then consider v1 such that
A2: x = v + v1 and
A3: v1 in W;
A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def 3
.= v + ((v1 + u) - u) by RLVECT_1:def 3
.= v + (v1 + (u - u)) by RLVECT_1:def 3
.= v + (v1 + 0.V) by RLVECT_1:15
.= x by A2,RLVECT_1:4;
v1 - u in W by A1,A3,Th42;
hence thesis by A4;
end;
let x be object;
assume x in (v + u) + W;
then consider v2 such that
A5: x = (v + u) + v2 and
A6: v2 in W;
A7: x = v + (u + v2) by A5,RLVECT_1:def 3;
u + v2 in W by A1,A6,Th39;
hence thesis by A7;
end;
assume
A8: v + W = (v + u) + W;
0.V in W & v + 0.V = v by Th36,RLVECT_1:4;
then v in (v + u) + W by A8;
then consider u1 such that
A9: v = (v + u) + u1 and
A10: u1 in W;
v = v + 0.V & v = v + (u + u1) by A9,RLVECT_1:4,def 3;
then u + u1 = 0.V by RLVECT_1:8;
then u = - u1 by RLVECT_1:def 10;
hence thesis by A10,Th41;
end;
theorem
u in W iff v + W = (v - u) + W
proof
A1: - u in W implies u in W
proof
assume - u in W;
then - (- u) in W by Th41;
hence thesis by RLVECT_1:17;
end;
-u in W iff v+W = (v+(-u))+W by Th71;
hence thesis by A1,Th41;
end;
theorem Th73:
v in u + W iff u + W = v + W
proof
thus v in u + W implies u + W = v + W
proof
assume v in u + W;
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W;
thus u + W c= v + W
proof
let x be object;
assume x in u + W;
then consider v1 such that
A3: x = u + v1 and
A4: v1 in W;
v - z = u + (z - z) by A1,RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
then
A5: x = v + (v1 + (- z)) by A3,RLVECT_1:def 3
.= v + (v1 - z);
v1 - z in W by A2,A4,Th42;
hence thesis by A5;
end;
let x be object;
assume x in v + W;
then consider v2 such that
A6: x = v + v2 & v2 in W;
z + v2 in W & x = u + (z + v2) by A1,A2,A6,Th39,RLVECT_1:def 3;
hence thesis;
end;
thus thesis by Th62;
end;
theorem Th74:
v + W = (- v) + W iff v in W
proof
thus v + W = (- v) + W implies v in W
proof
assume v + W = (- v) + W;
then v in (- v) + W by Th62;
then consider u such that
A1: v = - v + u and
A2: u in W;
0.V = v - (- v + u) by A1,RLVECT_1:15
.= (v - (- v)) - u by RLVECT_1:27
.= (v + v) - u by RLVECT_1:17
.= (1r * v + v) - u by Def5
.= (1r * v + 1r * v) - u by Def5
.= (1r+1r) * v - u by Def3;
then (1r+1r)" * ((1r+1r) * v) = (1r+1r)" * u by RLVECT_1:21;
then ((1r+1r)" * (1r+1r)) * v = (1r+1r)" * u by Def4;
then v = (1r+1r)" * u by Def5;
hence thesis by A2,Th40;
end;
assume
A3: v in W;
then v + W = the carrier of W by Lm6;
hence thesis by A3,Th70;
end;
theorem Th75:
u in v1 + W & u in v2 + W implies v1 + W = v2 + W
proof
assume that
A1: u in v1 + W and
A2: u in v2 + W;
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus v1 + W c= v2 + W
proof
let x be object;
assume x in v1 + W;
then consider u1 such that
A7: x = v1 + u1 and
A8: u1 in W;
x2 - x1 in W by A4,A6,Th42;
then
A9: (x2 - x1) + u1 in W by A8,Th39;
u - x1 = v1 + (x1 - x1) by A3,RLVECT_1:def 3
.= v1 + 0.V by RLVECT_1:15
.= v1 by RLVECT_1:4;
then x = (v2 + (x2 - x1)) + u1 by A5,A7,RLVECT_1:def 3
.= v2 + ((x2 - x1) + u1) by RLVECT_1:def 3;
hence thesis by A9;
end;
let x be object;
assume x in v2 + W;
then consider u1 such that
A10: x = v2 + u1 and
A11: u1 in W;
x1 - x2 in W by A4,A6,Th42;
then
A12: (x1 - x2) + u1 in W by A11,Th39;
u - x2 = v2 + (x2 - x2) by A5,RLVECT_1:def 3
.= v2 + 0.V by RLVECT_1:15
.= v2 by RLVECT_1:4;
then x = (v1 + (x1 - x2)) + u1 by A3,A10,RLVECT_1:def 3
.= v1 + ((x1 - x2) + u1) by RLVECT_1:def 3;
hence thesis by A12;
end;
theorem
u in v + W & u in (- v) + W implies v in W
by Th75,Th74;
theorem Th77:
z <> 1r & z * v in v + W implies v in W
proof
assume that
A1: z <> 1r and
A2: z * v in v + W;
A3: z - 1r <> 0 by A1;
consider u such that
A4: z * v = v + u and
A5: u in W by A2;
u = u + 0.V by RLVECT_1:4
.= u + (v - v) by RLVECT_1:15
.= z * v - v by A4,RLVECT_1:def 3
.= z * v - 1r * v by Def5
.= (z - 1r) * v by Th10;
then (z - 1r)" * u = ((z - 1r)" * (z - 1r)) * v by Def4;
then 1r * v = (z - 1r)" * u by A3,XCMPLX_0:def 7;
then v = (z - 1r)" * u by Def5;
hence thesis by A5,Th40;
end;
theorem Th78:
v in W implies z * v in v + W
proof
assume v in W;
then
A1: (z - 1r) * v in W by Th40;
z * v = ((z - 1r) + 1r) * v .= (z - 1r) * v + 1r * v by Def3
.= v + (z - 1r) * v by Def5;
hence thesis by A1;
end;
theorem
- v in v + W iff v in W
proof
(- 1r) * v = - v by Th3;
hence thesis by Th77,Th78;
end;
theorem Th80:
u + v in v + W iff u in W
proof
thus u + v in v + W implies u in W
proof
assume u + v in v + W;
then ex v1 st u + v = v + v1 & v1 in W;
hence thesis by RLVECT_1:8;
end;
assume u in W;
hence thesis;
end;
theorem
v - u in v + W iff u in W
proof
A1: v - u = (- u) + v;
A2: - u in W implies - (- u) in W by Th41;
u in W implies - u in W by Th41;
hence thesis by A1,A2,Th80,RLVECT_1:17;
end;
theorem Th82:
u in v + W iff ex v1 st v1 in W & u = v + v1
proof
thus u in v + W implies ex v1 st v1 in W & u = v + v1
proof
assume u in v + W;
then ex v1 st u = v + v1 & v1 in W;
hence thesis;
end;
given v1 such that
A1: v1 in W & u = v + v1;
thus thesis by A1;
end;
theorem
u in v + W iff ex v1 st v1 in W & u = v - v1
proof
thus u in v + W implies ex v1 st v1 in W & u = v - v1
proof
assume u in v + W;
then consider v1 such that
A1: u = v + v1 and
A2: v1 in W;
take x = - v1;
thus x in W by A2,Th41;
thus thesis by A1,RLVECT_1:17;
end;
given v1 such that
A3: v1 in W and
A4: u = v - v1;
- v1 in W by A3,Th41;
hence thesis by A4;
end;
theorem Th84:
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W
proof
thus (ex v st v1 in v + W & v2 in v + W) implies v1 - v2 in W
proof
given v such that
A1: v1 in v + W and
A2: v2 in v + W;
consider u2 such that
A3: u2 in W and
A4: v2 = v + u2 by A2,Th82;
consider u1 such that
A5: u1 in W and
A6: v1 = v + u1 by A1,Th82;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6,A4,RLVECT_1:30
.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3
.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3
.= (u1 + 0.V) - u2 by RLVECT_1:5
.= u1 - u2 by RLVECT_1:4;
hence thesis by A5,A3,Th42;
end;
assume v1 - v2 in W;
then
A7: - (v1 - v2) in W by Th41;
take v1;
thus v1 in v1 + W by Th62;
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33
.= (v1 + (- v1)) + v2 by RLVECT_1:def 3
.= 0.V + v2 by RLVECT_1:5
.= v2 by RLVECT_1:4;
hence thesis by A7;
end;
theorem Th85:
v + W = u + W implies ex v1 st v1 in W & v + v1 = u
proof
assume v + W = u + W;
then v in u + W by Th62;
then consider u1 such that
A1: v = u + u1 and
A2: u1 in W;
take v1 = u - v;
0.V = (u + u1) - v by A1,RLVECT_1:15
.= u1 + (u - v) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,Th41;
thus v + v1 = (u + v) - v by RLVECT_1:def 3
.= u + (v - v) by RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem Th86:
v + W = u + W implies ex v1 st v1 in W & v - v1 = u
proof
assume v + W = u + W;
then u in v + W by Th62;
then consider u1 such that
A1: u = v + u1 and
A2: u1 in W;
take v1 = v - u;
0.V = (v + u1) - u by A1,RLVECT_1:15
.= u1 + (v - u) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,Th41;
thus v - v1 = (v - v) + u by RLVECT_1:29
.= 0.V + u by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem Th87:
for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2
proof
let W1,W2 be strict Subspace of V;
thus v + W1 = v + W2 implies W1 = W2
proof
assume
A1: v + W1 = v + W2;
the carrier of W1 = the carrier of W2
proof
A2: the carrier of W1 c= the carrier of V by Def8;
thus the carrier of W1 c= the carrier of W2
proof
let x be object;
assume
A3: x in the carrier of W1;
then reconsider y = x as Element of V by A2;
set z = v + y;
x in W1 by A3;
then z in v + W2 by A1;
then consider u such that
A4: z = v + u and
A5: u in W2;
y = u by A4,RLVECT_1:8;
hence thesis by A5;
end;
let x be object;
assume
A6: x in the carrier of W2;
the carrier of W2 c= the carrier of V by Def8;
then reconsider y = x as Element of V by A6;
set z = v + y;
x in W2 by A6;
then z in v + W1 by A1;
then consider u such that
A7: z = v + u and
A8: u in W1;
y = u by A7,RLVECT_1:8;
hence thesis by A8;
end;
hence thesis by Th49;
end;
thus thesis;
end;
theorem Th88:
for W1,W2 being strict Subspace of V holds v + W1 = u + W2 implies W1 = W2
proof
let W1,W2 be strict Subspace of V;
assume
A1: v + W1 = u + W2;
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume
A2: W1 <> W2;
A3: now
set x = the Element of V1 \ V2;
assume V1 \ V2 <> {};
then x in V1 by XBOOLE_0:def 5;
then
A4: x in W1;
then x in V by Th28;
then reconsider x as Element of V;
set z = v + x;
z in u + W2 by A1,A4;
then consider u1 such that
A5: z = u + u1 and
A6: u1 in W2;
x = 0.V + x by RLVECT_1:4
.= v - v + x by RLVECT_1:15
.= - v + (u + u1) by A5,RLVECT_1:def 3;
then
A7: (v + (- v + (u + u1))) + W1 = v + W1 by A4,Th71;
v + (- v + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def 3
.= 0.V + (u + u1) by RLVECT_1:15
.= u + u1 by RLVECT_1:4;
then (u + u1) + W2 = (u + u1) + W1 by A1,A6,A7,Th71;
hence thesis by A2,Th87;
end;
A8: now
set x = the Element of V2 \ V1;
assume V2 \ V1 <> {};
then x in V2 by XBOOLE_0:def 5;
then
A9: x in W2;
then x in V by Th28;
then reconsider x as Element of V;
set z = u + x;
z in v + W1 by A1,A9;
then consider u1 such that
A10: z = v + u1 and
A11: u1 in W1;
x = 0.V + x by RLVECT_1:4
.= u - u + x by RLVECT_1:15
.= - u + (v + u1) by A10,RLVECT_1:def 3;
then
A12: (u + (- u + (v + u1))) + W2 = u + W2 by A9,Th71;
u + (- u + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def 3
.= 0.V + (v + u1) by RLVECT_1:15
.= v + u1 by RLVECT_1:4;
then (v + u1) + W1 = (v + u1) + W2 by A1,A11,A12,Th71;
hence thesis by A2,Th87;
end;
V1 <> V2 by A2,Th49;
then not V1 c= V2 or not V2 c= V1;
hence thesis by A3,A8,XBOOLE_1:37;
end;
:: Theorems concerning cosets of subspace
:: regarded as subsets of the carrier.
theorem
C is linearly-closed iff C = the carrier of W
proof
thus C is linearly-closed implies C = the carrier of W
proof
assume
A1: C is linearly-closed;
consider v such that
A2: C = v + W by Def12;
C <> {} by A2,Th62;
then 0.V in v + W by A1,A2,Th20;
hence thesis by A2,Th66;
end;
thus thesis by Lm3;
end;
theorem
for W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being
Coset of W2 holds C1 = C2 implies W1 = W2
proof
let W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2;
( ex v1 st C1 = v1 + W1)& ex v2 st C2 = v2 + W2 by Def12;
hence thesis by Th88;
end;
theorem
{v} is Coset of (0).V
proof
v + (0).V = {v} by Th64;
hence thesis by Def12;
end;
theorem
V1 is Coset of (0).V implies ex v st V1 = {v}
proof
assume V1 is Coset of (0).V;
then consider v such that
A1: V1 = v + (0).V by Def12;
take v;
thus thesis by A1,Th64;
end;
theorem
the carrier of W is Coset of W
proof
the carrier of W = 0.V + W by Lm5;
hence thesis by Def12;
end;
theorem
the carrier of V is Coset of (Omega).V
proof
set v = the VECTOR of V;
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider A = the carrier of V as Subset of V;
A = v + (Omega).V by Th65;
hence thesis by Def12;
end;
theorem
V1 is Coset of (Omega).V implies V1 = the carrier of V
proof
assume V1 is Coset of (Omega).V;
then ex v st V1 = v + (Omega).V by Def12;
hence thesis by Th65;
end;
theorem
0.V in C iff C = the carrier of W
proof
ex v st C = v + W by Def12;
hence thesis by Th66;
end;
theorem Th97:
u in C iff C = u + W
proof
thus u in C implies C = u + W
proof
assume
A1: u in C;
ex v st C = v + W by Def12;
hence thesis by A1,Th73;
end;
thus thesis by Th62;
end;
theorem
u in C & v in C implies ex v1 st v1 in W & u + v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by Th97;
hence thesis by Th85;
end;
theorem
u in C & v in C implies ex v1 st v1 in W & u - v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by Th97;
hence thesis by Th86;
end;
theorem
(ex C st v1 in C & v2 in C) iff v1 - v2 in W
proof
thus (ex C st v1 in C & v2 in C) implies v1 - v2 in W
proof
given C such that
A1: v1 in C & v2 in C;
ex v st C = v + W by Def12;
hence thesis by A1,Th84;
end;
assume v1 - v2 in W;
then consider v such that
A2: v1 in v + W & v2 in v + W by Th84;
reconsider C = v + W as Coset of W by Def12;
take C;
thus thesis by A2;
end;
theorem
u in B & u in C implies B = C
proof
assume
A1: u in B & u in C;
( ex v1 st B = v1 + W) & ex v2 st C = v2 + W by Def12;
hence thesis by A1,Th75;
end;
begin :: Complex Normed Space
definition
struct(CLSStruct,N-ZeroStr) CNORMSTR (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier, Mult -> Function of [:COMPLEX, the
carrier:], the carrier, normF -> Function of the carrier, REAL #);
end;
registration
cluster non empty for CNORMSTR;
existence
proof
set A = the non empty set,Z = the Element of A,a = the BinOp of A,M =the
Function of [:COMPLEX,A:],A,n = the Function of A,REAL;
take CNORMSTR(#A,Z,a,M,n#);
thus the carrier of CNORMSTR(#A,Z,a,M,n#) is non empty;
end;
end;
deffunc 09(CNORMSTR) = 0.$1;
set V = the ComplexLinearSpace;
Lm7: the carrier of (0).V = {0.V} by Def9;
reconsider niltonil = (the carrier of (0).V) --> In(0,REAL)
as Function of the carrier
of (0).V, REAL;
0.V is VECTOR of (0).V by Lm7,TARSKI:def 1;
then
Lm8: niltonil.(0.V) = 0 by FUNCOP_1:7;
Lm9: for u being VECTOR of (0).V, z holds niltonil.(z * u) = |.z.| * niltonil.
u
proof
let u be VECTOR of (0).V;
let z;
niltonil.u = 0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
Lm10: for u, v being VECTOR of (0).V holds niltonil.(u + v) <= niltonil.u +
niltonil.v
proof
let u, v be VECTOR of (0).V;
u = 0.V & v = 0.V by Lm7,TARSKI:def 1;
hence thesis by Lm7,Lm8,TARSKI:def 1;
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;
Lm11: now
let x, y be Point of X;
let z;
reconsider u = x, w = y as VECTOR of (0).V;
09(X) = 0.V by Def8;
hence ||.x.|| = 0 iff x = 09(X) by Lm7,FUNCOP_1:7,TARSKI:def 1;
z * x = z * u;
hence ||.z * x.|| = |.z.| * ||.x.|| by Lm9;
x + y = u + w;
hence ||.x + y.|| <= ||.x.|| + ||.y.|| by Lm10;
end;
definition
let IT be non empty CNORMSTR;
attr IT is ComplexNormSpace-like means
:Def13:
for x, y being Point of IT, z holds
||.z * x.|| = |.z.| * ||.x.|| & ||.x + y .|| <= ||.x.|| + ||.y.||;
end;
registration
cluster reflexive discerning ComplexNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
strict for non empty CNORMSTR;
existence
proof
take X;
thus X is reflexive
by Lm11;
thus X is discerning ComplexNormSpace-like
by Lm11;
thus X is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
thus for z for v,w being VECTOR of X holds z * (v + w) = z * v + z * w
proof
let z;
let v,w be VECTOR of X;
reconsider v9= v, w9 = w as VECTOR of (0).V;
thus z * (v + w) = z *( v9 + w9) .= z * v9 + z * w9 by Def2
.= z * v + z * w;
end;
thus for z1,z2 for v being VECTOR of X holds (z1+z2) * v = z1 * v + z2 *
v
proof
let z1,z2;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus (z1 + z2) * v = (z1 + z2) * v9 .= z1 * v9 + z2 * v9 by Def3
.= z1 * v + z2 * v;
end;
thus for z1,z2 for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 *
v )
proof
let z1,z2;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus (z1 * z2) * v = (z1 * z2) * v9 .= z1 * (z2 * v9) by Def4
.= z1 * (z2 * v);
end;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus 1r * v = 1r * v9 .= v by Def5;
end;
A1: for x,y be VECTOR of X for x9,y9 be VECTOR of (0).V st x = x9 & y = y9
holds x + y= x9 + y9 & for z holds z * x = z * x9;
thus for v,w being VECTOR of X holds v + w = w + v
proof
let v,w be VECTOR of X;
reconsider v9= v, w9= w as VECTOR of (0).V;
thus v + w = w9+ v9 by A1
.= w + v;
end;
thus for u,v,w being VECTOR of X holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of X;
reconsider u9= u, v9= v, w9= w as VECTOR of (0).V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
thus for v being VECTOR of X holds v + 0.X = v
proof
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus v + 0.X = v9+ 0.(0).V .=v by RLVECT_1:4;
end;
thus X is right_complementable
proof
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
consider w9 be VECTOR of (0).V such that
A2: v9 + w9 = 0.(0).V by ALGSTR_0:def 11;
reconsider w = w9 as VECTOR of X;
take w;
thus thesis by A2;
end;
thus thesis;
end;
end;
definition
mode ComplexNormSpace is reflexive discerning ComplexNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
non empty CNORMSTR;
end;
reserve CNS for ComplexNormSpace;
reserve x, y, w, g, g1, g2 for Point of CNS;
theorem
||.0.CNS.|| = 0;
theorem Th103:
||.-x.|| = ||.x.||
proof
A1: |.-1r.| = 1 by COMPLEX1:48,52;
||.-x.|| = ||.(-1r) * x.|| by Th3
.= |.-1r.| * ||.x.|| by Def13;
hence thesis by A1;
end;
theorem Th104:
||.x - y.|| <= ||.x.|| + ||.y.||
proof
||.x - y.|| <= ||.x.|| + ||.(-y).|| by Def13;
hence thesis by Th103;
end;
theorem Th105:
0 <= ||.x.||
proof
||.x - x.|| = ||.09(CNS).|| by RLVECT_1:15
.= 0;
then 0 <= (||.x.|| + ||.x.||)/2 by Th104;
hence thesis;
end;
theorem
||.z1 * x + z2 * y.|| <= |.z1.| * ||.x.|| + |.z2.| * ||.y.||
proof
||.z1 * x + z2 * y.|| <= ||.z1 * x.|| + ||.z2 * y.|| by Def13;
then ||.z1 * x + z2 * y.|| <= |.z1.| * ||.x.|| + ||.z2 * y.|| by Def13;
hence thesis by Def13;
end;
theorem Th107:
||.x - y.|| = 0 iff x = y
proof
||.x - y.|| = 0 iff x - y = 09(CNS) by NORMSP_0:def 5;
hence thesis by RLVECT_1:15,21;
end;
theorem Th108:
||.x - y.|| = ||.y - x.||
proof
x - y = - (y - x) by RLVECT_1:33;
hence thesis by Th103;
end;
theorem Th109:
||.x.|| - ||.y.|| <= ||.x - y.||
proof
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - 09(CNS) by RLVECT_1:15
.= x by RLVECT_1:13;
then ||.x.|| <= ||.x - y.|| + ||.y.|| by Def13;
hence thesis by XREAL_1:20;
end;
theorem Th110:
|.||.x.|| - ||.y.||.| <= ||.x - y.||
proof
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - 09(CNS) by RLVECT_1:15
.= y by RLVECT_1:13;
then ||.y.|| <= ||.y - x.|| + ||.x.|| by Def13;
then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20;
then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th108;
then
A1: - ||.x - y.|| <= -(||.y.|| - ||.x.||) by XREAL_1:24;
||.x.|| - ||.y.|| <= ||.x - y.|| by Th109;
hence thesis by A1,ABSVALUE:5;
end;
theorem Th111:
||.x - w.|| <= ||.x - y.|| + ||.y - w.||
proof
x - w = x + (09(CNS) + (-w)) by RLVECT_1:4
.= x + (((-y) + y) + (-w)) by RLVECT_1:5
.= x + ((-y) + (y + (-w))) by RLVECT_1:def 3
.= (x - y) + (y - w) by RLVECT_1:def 3;
hence thesis by Def13;
end;
theorem
x <> y implies ||.x - y.|| <> 0 by Th107;
reserve S, S1, S2 for sequence of CNS;
reserve n, m, m1, m2 for Nat;
reserve r for Real;
definition
let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let z;
func z * S -> sequence of CNS means
:Def14:
for n holds it.n = z * S.n;
existence
proof
deffunc F(Nat) = z * S.$1;
consider S being sequence of CNS such that
A1: for n being Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of CNS;
assume that
A2: for n holds S1.n = z * S.n and
A3: for n holds S2.n = z * S.n;
for n being Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = z * S.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let CNS;
let S;
attr S is convergent means
ex g st for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
end;
theorem Th113:
S1 is convergent & S2 is convergent implies S1 + S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S1.n) - g1.|| < r
by A1;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds ||.(S2.n) - g2.|| < r
by A2;
take g = g1 + g2;
let r;
assume
A5: 0 < r;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
reconsider k = m1 + m2 as Nat;
take k;
let n such that
A8: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A8,XXREAL_0:2;
then
A9: ||.(S2.n) - g2.|| < r/2 by A7;
A10: ||.(S1 + S2).n - g.|| = ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by
NORMSP_1:def 2
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:31
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 3;
A11: ||.(S1.n) - g1 + ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) - g2
.|| by Def13;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A8,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,A11,XXREAL_0:2;
end;
theorem Th114:
S1 is convergent & S2 is convergent implies S1 - S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S1.n) - g1.|| < r
by A1;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds ||.(S2.n) - g2.|| < r
by A2;
take g = g1 - g2;
let r;
assume
A5: 0 < r;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A8,XXREAL_0:2;
then
A9: ||.(S2.n) - g2.|| < r/2 by A7;
A10: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by
NORMSP_1:def 3
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:29
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:27
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:27
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:29;
A11: ||.((S1.n) - g1) - ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) -
g2.|| by Th104;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A8,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,A11,XXREAL_0:2;
end;
theorem Th115:
S is convergent implies S - x is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
take h = g - x;
let r;
assume 0 < r;
then consider m1 such that
A2: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n;
assume k <= n;
then
A3: ||.(S.n) - g.|| < r by A2;
||.(S.n) - g.|| = ||.((S.n) - 09(CNS)) - g.|| by RLVECT_1:13
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:15
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:29
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 3
.= ||.((S.n) - x) - h.|| by RLVECT_1:33;
hence thesis by A3,NORMSP_1:def 4;
end;
theorem Th116:
S is convergent implies z * S is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
take h = z * g;
A2: now
assume
A3: z <> 0c;
then
A4: 0 < |.z.| by COMPLEX1:47;
let r;
assume 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r/|.z.| by A1,A4;
take k = m1;
let n;
assume k <= n;
then
A6: ||.(S.n) - g.|| < r/|.z.| by A5;
A7: 0 <> |.z.| by A3,COMPLEX1:47;
A8: |.z.| * (r/|.z.|) = |.z.| * (|.z.|" * r) by XCMPLX_0:def 9
.= |.z.| *|.z.|" * r
.= 1 * r by A7,XCMPLX_0:def 7
.= r;
||.(z * (S.n)) - (z * g).|| = ||.z * ((S.n) - g).|| by Th9
.= |.z.| * ||.(S.n) - g.|| by Def13;
then ||.(z *(S.n)) - h.|| < r by A4,A6,A8,XREAL_1:68;
hence ||.(z * S).n - h.|| < r by Def14;
end;
now
assume
A9: z = 0;
let r;
assume 0 < r;
then consider m1 such that
A10: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n;
assume k <= n;
then
A11: ||.(S.n) - g.|| < r by A10;
||.z * (S.n) - z * g.|| = ||.0c * (S.n) - 09(CNS).|| by A9,Th1
.= ||.09(CNS) - 09(CNS).|| by Th1
.= ||.09(CNS).|| by RLVECT_1:13
.= 0;
then ||.z * (S.n) - h.|| < r by A11,Th105;
hence ||.(z * S).n - h.|| < r by Def14;
end;
hence thesis by A2;
end;
theorem Th117:
S is convergent implies ||.S.|| is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
now
let r be Real;
assume
A2: 0 < r;
consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2;
take k = m1;
let n;
assume k <= n;
then
A4: ||.(S.n) - g.|| < r by A3;
|.||.(S.n).|| - ||.g.||.| <= ||.(S.n) - g.|| by Th110;
then |.||.(S.n).|| - ||.g.||.| < r by A4,XXREAL_0:2;
hence |.||.S.||.n - ||.g.||.| < r by NORMSP_0:def 4;
end;
hence thesis by SEQ_2:def 6;
end;
definition
let CNS;
let S;
assume
A1: S is convergent;
func lim S -> Point of CNS means
:Def16:
for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - it.|| < r;
existence by A1;
uniqueness
proof
for x, y st ( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) -
x.|| < r ) & ( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r
) holds x = y
proof
given x, y such that
A2: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - x.|| < r and
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r and
A4: x <> y;
A5: 0 <= ||.x - y.|| by Th105;
A6: ||.x - y.|| <> 0 by A4,Th107;
then consider m1 such that
A7: for n st m1 <= n holds ||.(S.n) - x.|| < ||.x - y.||/4 by A2,A5;
consider m2 such that
A8: for n st m2 <= n holds ||.(S.n) - y.|| < ||.x - y.||/4 by A3,A6,A5;
A9: now
||.x - y.|| <= ||.x - (S.m1).|| + ||.(S.m1) - y.|| by Th111;
then
A10: ||.x - y.|| <= ||.(S.m1) - x.|| + ||.(S.m1) - y.|| by Th108;
assume m2 <= m1;
then
A11: ||.(S.m1) - y.|| < ||.x - y.||/4 by A8;
||.(S.m1) - x.|| < ||.x - y.||/4 by A7;
then
||.(S.m1) - x.|| + ||.(S.m1) - y.|| < ||.x - y.||/4 + ||.x - y.||
/4 by A11,XREAL_1:8;
then not ||.x - y.||/2 < ||.x - y.|| by A10,XXREAL_0:2;
hence contradiction by A6,A5,XREAL_1:216;
end;
now
||.x - y.|| <= ||.x - (S.m2).|| + ||.(S.m2) - y.|| by Th111;
then
A12: ||.x - y.|| <= ||.(S.m2) - x.|| + ||.(S.m2) - y.|| by Th108;
assume m1 <= m2;
then
A13: ||.(S.m2) - x.|| < ||.x - y.||/4 by A7;
||.(S.m2) - y.|| < ||.x - y.||/4 by A8;
then
||.(S.m2) - x.|| + ||.(S.m2) - y.|| < ||.x - y.||/4 + ||.x - y.||
/4 by A13,XREAL_1:8;
then not ||.x - y.||/2 < ||.x - y.|| by A12,XXREAL_0:2;
hence contradiction by A6,A5,XREAL_1:216;
end;
hence contradiction by A9;
end;
hence thesis;
end;
end;
theorem
S is convergent & lim S = g implies ||.S - g.|| is convergent & lim
||.S - g.|| = 0
proof
assume that
A1: S is convergent and
A2: lim S = g;
A3: now
let r be Real;
assume
A4: 0 < r;
consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2,A4,Def16;
take k = m1;
let n;
assume k <= n;
then ||.(S.n) - g.|| < r by A5;
then
A6: ||.((S.n) - g ) - 09(CNS).|| < r by RLVECT_1:13;
|.||.(S.n) - g.|| - ||.09(CNS).||.| <= ||.((S.n) - g ) - 09(CNS).||
by Th110;
then |.||.(S.n) - g.|| - ||.09(CNS).||.| < r by A6,XXREAL_0:2;
then |.(||.(S.n) - g.|| - 0).| < r;
then |.(||.(S - g).n.|| - 0).| < r by NORMSP_1:def 4;
hence |.(||.S - g.||.n - 0).| < r by NORMSP_0:def 4;
end;
||.S - g.|| is convergent by A1,Th115,Th117;
hence thesis by A3,SEQ_2:def 7;
end;
theorem
S1 is convergent & S2 is convergent implies lim(S1+S2) = (lim S1) + (
lim S2 )
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
set g2 = lim S2;
set g1 = lim S1;
set g = g1 + g2;
A3: now
let r;
assume
A4: 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def16;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def16;
take k = m1 + m2;
let n such that
A7: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A7,XXREAL_0:2;
then
A8: ||.(S2.n) - g2.|| < r/2 by A6;
A9: ||.(S1 + S2).n - g.|| = ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by
NORMSP_1:def 2
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:31
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 3;
A10: ||.(S1.n) - g1 + ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) -
g2.|| by Def13;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A5;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A8,XREAL_1:8;
hence ||.(S1 + S2).n - g.|| < r by A9,A10,XXREAL_0:2;
end;
S1 + S2 is convergent by A1,A2,Th113;
hence thesis by A3,Def16;
end;
theorem
S1 is convergent & S2 is convergent implies lim (S1-S2) = (lim S1) - (
lim S2 )
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
set g2 = lim S2;
set g1 = lim S1;
set g = g1 - g2;
A3: now
let r;
assume
A4: 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def16;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def16;
take k = m1 + m2;
let n such that
A7: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A7,XXREAL_0:2;
then
A8: ||.(S2.n) - g2.|| < r/2 by A6;
A9: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by
NORMSP_1:def 3
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:29
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:27
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:27
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:29;
A10: ||.((S1.n) - g1) - ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n)
- g2.|| by Th104;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A5;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A8,XREAL_1:8;
hence ||.(S1 - S2).n - g.|| < r by A9,A10,XXREAL_0:2;
end;
S1 - S2 is convergent by A1,A2,Th114;
hence thesis by A3,Def16;
end;
theorem
S is convergent implies lim (S - x) = (lim S) - x
proof
set g = lim S;
set h = g - x;
assume
A1: S is convergent;
A2: now
let r;
assume 0 < r;
then consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def16;
take k = m1;
let n;
assume k <= n;
then
A4: ||.(S.n) - g.|| < r by A3;
||.(S.n) - g.|| = ||.((S.n) - 09(CNS)) - g.|| by RLVECT_1:13
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:15
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:29
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 3
.= ||.((S.n) - x) - h.|| by RLVECT_1:33;
hence ||.(S - x).n - h.|| < r by A4,NORMSP_1:def 4;
end;
S - x is convergent by A1,Th115;
hence thesis by A2,Def16;
end;
theorem
S is convergent implies lim (z * S) = z * (lim S)
proof
set g = lim S;
set h = z * g;
assume
A1: S is convergent;
A2: now
assume
A3: z = 0;
let r;
assume 0 < r;
then consider m1 such that
A4: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def16;
take k = m1;
let n;
assume k <= n;
then
A5: ||.(S.n) - g.|| < r by A4;
||.z * (S.n) - z * g.|| = ||.0c * (S.n) - 09(CNS).|| by A3,Th1
.= ||.09(CNS) - 09(CNS).|| by Th1
.= ||.09(CNS).|| by RLVECT_1:13
.= 0;
then ||.z * (S.n) - h.|| < r by A5,Th105;
hence ||.(z * S).n - h.|| < r by Def14;
end;
A6: now
assume
A7: z <> 0c;
then
A8: 0 < |.z.| by COMPLEX1:47;
let r;
assume 0 < r;
then consider m1 such that
A9: for n st m1 <= n holds ||.(S.n) - g.|| < r/|.z.| by A1,A8,Def16;
take k = m1;
let n;
assume k <= n;
then
A10: ||.(S.n) - g.|| < r/|.z.| by A9;
A11: 0 <> |.z.| by A7,COMPLEX1:47;
A12: |.z.| * (r/|.z.|) = |.z.| * (|.z.|" * r) by XCMPLX_0:def 9
.= |.z.| *|.z.|" * r
.= 1 * r by A11,XCMPLX_0:def 7
.= r;
||.(z * (S.n)) - (z * g).|| = ||.z * ((S.n) - g).|| by Th9
.= |.z.| * ||.(S.n) - g.|| by Def13;
then ||.(z *(S.n)) - h.|| < r by A8,A10,A12,XREAL_1:68;
hence ||.(z * S).n - h.|| < r by Def14;
end;
z * S is convergent by A1,Th116;
hence thesis by A2,A6,Def16;
end;
theorem
for V,V1,v for w be VECTOR of CLSStruct (# D,d1,A,M #) st
V1 = D & M = (the Mult of V) | [:COMPLEX,V1:] & w = v holds
z*w = z*v by Lm4;