:: Convex Sets and Convex Combinations on Complex Linear Spaces
:: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies SUBSET_1, FUNCT_1, PROB_2, FINSEQ_1, RLVECT_1, RELAT_1, FINSEQ_4,
ARYTM_1, BOOLE, JORDAN1, SETFAM_1, CONNSP_3, ARYTM_3, RUSUB_4, CONVEX1,
FUNCT_2, FINSET_1, SEQ_1, RLSUB_1, CARD_1, QC_LANG1, BINOP_1, CSSPACE,
RLVECT_2, FUNCOP_1, COMPLEX1, XCMPLX_0, CFUNCT_1, CLVECT_1, CONVEX4,
ARYTM, ALGSTR_0;
notations TARSKI, XBOOLE_0, ENUMSET1, DOMAIN_1, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, FRAENKEL, FINSEQ_1, ALGSTR_0, RLVECT_1,
SETFAM_1, STRUCT_0, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, FINSET_1,
PARTFUN1, FUNCOP_1, CARD_1, VALUED_1, XCMPLX_0, COMPLEX1, RVSUM_1,
RUSUB_4, RUSUB_5, NAT_1, BINOP_1, REAL_1, RLVECT_2, CFUNCT_1, CLVECT_1,
CSSPACE;
constructors STRUCT_0, SETFAM_1, DOMAIN_1, BINOP_1, FUNCOP_1, VALUED_1,
XXREAL_0, XREAL_0, REAL_1, NAT_1, FINSEQ_4, COMPLEX1, XCMPLX_0, CFUNCT_1,
PARTFUN1, REALSET1, BINOP_2, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5,
CLVECT_1, CSSPACE;
registrations STRUCT_0, MEMBERED, XXREAL_0, CSSPACE, RLVECT_1, RELSET_1,
FINSET_1, XREAL_0, SUBSET_1, XCMPLX_0, CLVECT_1, XBOOLE_0, NUMBERS,
ORDINAL1, NAT_1, FUNCT_2, VALUED_1, VALUED_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, TARSKI, XBOOLE_0, BINOP_1, RLVECT_1, RELAT_1, STRUCT_0,
REALSET1, FINSEQ_1, CLVECT_1, COMPLEX1, RVSUM_1, XCMPLX_0, ALGSTR_0,
RUSUB_4, RUSUB_5;
theorems SUBSET_1, STRUCT_0, RVSUM_1, REAL_2, SETFAM_1, ENUMSET1, BINOP_1,
CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
NAT_1, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, COMPLEX1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, FINSOP_1,
CLVECT_1, CSSPACE, CONVEX1, PARTFUN1, XREAL_0, VALUED_1, ALGSTR_0;
schemes DOMAIN_1, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
begin :: Complex Linear Combinations
definition
let V be non empty ZeroStr;
mode C_Linear_Combination of V -> Element of Funcs(the carrier of V, COMPLEX)
means :Def1:
ex T being finite Subset of V st
for v being Element of V st not v in T holds it.v = 0;
existence
proof
reconsider f = (the carrier of V) --> 0c
as Function of the carrier of V, COMPLEX;
reconsider f as Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:11;
take f;
{}V = {};
then reconsider P = {} as finite Subset of V;
take P;
thus thesis by FUNCOP_1:13;
end;
end;
definition
let V be non empty addLoopStr,
L be Element of Funcs(the carrier of V, COMPLEX);
func Carrier L -> Subset of V equals
{v where v is Element of V : L.v <> 0c};
coherence
proof set A = {v where v is Element of V : L.v <> 0c};
for x being set st x in A holds x in the carrier of V
proof let x be set;
assume x in A;
then ex v being Element of V st x = v & L.v <> 0c;
hence thesis;
end;
hence A is Subset of V by TARSKI:def 3;
end;
end;
registration
let V be non empty addLoopStr, L be C_Linear_Combination of V;
cluster Carrier L -> finite;
coherence
proof set A = Carrier L;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds L.v = 0c by Def1;
now let x be set;
assume x in A;
then ex v being Element of V st x = v & L.v <> 0c;
hence x in T by A1;
end;
then A c= T by TARSKI:def 3;
hence A is finite by FINSET_1:13;
end;
end;
theorem Th1:
for V be non empty addLoopStr,
L be C_Linear_Combination of V,
v be Element of V
holds
L.v = 0c iff not v in Carrier L
proof
let V be non empty addLoopStr,
L be C_Linear_Combination of V,
v be Element of V;
thus L.v = 0c implies not v in Carrier L
proof assume A1: L.v = 0c;
assume not thesis;
then ex u being Element of V st v=u & L.u <> 0c;
hence thesis by A1;
end;
assume not v in Carrier L;
hence thesis;
end;
definition
let V be non empty addLoopStr;
func ZeroCLC V -> C_Linear_Combination of V means :Def2:
Carrier it = {};
existence
proof
reconsider f = (the carrier of V) --> 0c
as Function of the carrier of V, COMPLEX;
reconsider f as Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:11;
f is C_Linear_Combination of V
proof
reconsider T = {}V as empty finite Subset of V;
take T;
thus thesis by FUNCOP_1:13;
end;
then reconsider f as C_Linear_Combination of V;
take f;
set C = {v where v is Element of V : f.v <> 0c};
now assume A2: C <> {};
consider x being Element of C;
x in C by A2;
then ex v being Element of V st x = v & f.v <> 0c;
hence contradiction by FUNCOP_1:13;
end;
hence thesis;
end;
uniqueness
proof
let L,L' be C_Linear_Combination of V;
assume that A3: Carrier L = {} & Carrier L' = {};
now let x be set;
assume x in the carrier of V;
then reconsider v = x as Element of V;
A5: L.v <> 0c implies v in {u where u is Element of V : L.u <> 0c};
L'.v <> 0c implies v in {u where u is Element of V : L'.u <> 0c};
hence L.x = L'.x by A3,A5;
end;
hence L = L' by FUNCT_2:18;
end;
end;
registration
let V be non empty addLoopStr;
cluster Carrier ZeroCLC V -> empty;
coherence by Def2;
end;
theorem Th30:
for V be non empty addLoopStr, v be Element of V holds
(ZeroCLC V).v = 0c
proof
let V be non empty addLoopStr, v be Element of V;
Carrier (ZeroCLC V) = {} & not v in {};
hence thesis;
end;
definition
let V be non empty addLoopStr;
let A be Subset of V;
mode C_Linear_Combination of A -> C_Linear_Combination of V means :Def3:
Carrier it c= A;
existence
proof
take L = ZeroCLC V;
Carrier L = {} by Def2;
hence thesis by XBOOLE_1:2;
end;
end;
theorem
for V be non empty addLoopStr, A,B be Subset of V,
l be C_Linear_Combination of A st
A c= B holds l is C_Linear_Combination of B
proof
let V be non empty addLoopStr;
let A,B be Subset of V;
let l be C_Linear_Combination of A;
assume A1: A c= B;
Carrier l c= A by Def3;
then Carrier l c= B by A1,XBOOLE_1:1;
hence thesis by Def3;
end;
theorem Th34:
for V be non empty addLoopStr, A be Subset of V holds
ZeroCLC V is C_Linear_Combination of A
proof
let V be non empty addLoopStr;
let A be Subset of V;
Carrier ZeroCLC V = {} & {} c= A by XBOOLE_1:2;
hence thesis by Def3;
end;
theorem Th35:
for V being non empty addLoopStr,
l being C_Linear_Combination of {}the carrier of V holds
l = ZeroCLC V
proof
let V be non empty addLoopStr;
let l be C_Linear_Combination of {}(the carrier of V);
Carrier l c= {} by Def3;
then Carrier l = {} by XBOOLE_1:3;
hence thesis by Def2;
end;
reserve x,y for set,
i for Nat;
definition
let V be non empty CLSStruct;
let F be FinSequence of the carrier of V;
let f be Function of the carrier of V,COMPLEX;
func f (#) F -> FinSequence of the carrier of V means :Def4:
len it = len F &
for i st i in dom it holds it.i = f.(F/.i) * F/.i;
existence
proof
deffunc Q(set)= f.(F/.$1) * F/.$1;
consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n)
from FINSEQ_1:sch 2;
rng G c= the carrier of V
proof let x;
assume x in rng G;
then consider y such that
A3: y in dom G & G.y = x by FUNCT_1:def 5;
reconsider y as Element of NAT by A3;
G.y = f.(F/.y) * F/.y & f.(F/.y) * F/.y in the carrier of V by A2,A3;
hence thesis by A3;
end;
then reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;
take G;
thus thesis by A1,A2;
end;
uniqueness
proof
let H1,H2 be FinSequence of the carrier of V;
assume that A6: len H1 = len F and
A7: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A8: len H2 = len F and
A9: for i st i in dom H2 holds H2.i = f.(F/.i) * F/.i;
now
let k be Nat;
assume 1 <= k & k <= len H1;
then k in Seg len H1 by FINSEQ_1:3;
then k in dom H1 & k in dom H2 by A6,A8,FINSEQ_1:def 3;
then H1.k = f.(F/.k) * F/.k & H2.k = f.(F/.k) * F/.k by A7,A9;
hence H1.k = H2.k;
end;
hence thesis by A6,A8,FINSEQ_1:18;
end;
end;
reserve V for non empty CLSStruct,
u,v,v1,v2,v3,w for VECTOR of V,
A, B for Subset of V,
l, l1, l2 for C_Linear_Combination of A,
x,y,y1,y2 for set,
a,b for Complex,
i,j,k,n for Nat,
F,G,H1,H2 for FinSequence of the carrier of V,
f for Function of the carrier of V, COMPLEX;
theorem Th40:
x in dom F & v = F.x implies (f (#) F).x = f.v * v
proof
assume that A1: x in dom F and A2: v = F.x;
len(f (#) F) = len F by Def4;
then A3: x in dom(f (#) F) by A1,FINSEQ_3:31;
A4:F/.x = F.x by A1,PARTFUN1:def 8;
reconsider i = x as Nat by A1,FINSEQ_3:25;
(f(#)F).i = f.v * v by A2,A3,A4,Def4;
hence (f (#) F).x = f.v * v;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def4
.= 0 by FINSEQ_1:32;
hence thesis by FINSEQ_1:32;
end;
theorem Th42:
f (#) <* v *> = <* f.v * v *>
proof
A1: len(f (#) <* v *>) = len<* v *> by Def4
.= 1 by FINSEQ_1:57; then
dom(f (#)<* v *>) = {1} & 1 in {1} by FINSEQ_1:4,def 3; then
(f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by Def4
.= f.(<* v *>/.1) * v by FINSEQ_4:25
.= f.v * v by FINSEQ_4:25;
hence thesis by A1,FINSEQ_1:57;
end;
theorem Th43:
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def4
.= 2 by FINSEQ_1:61; then
A2: dom(f (#) <* v1,v2 *>) = {1,2} & 1 in {1,2} & 2 in {1,2}
by FINSEQ_1:4,def 3; then
A3: (f (#) <* v1,v2 *>).1 = f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by Def4
.= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:26
.= f.v1 * v1 by FINSEQ_4:26;
(f (#) <* v1,v2 *>).2 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2 by A2,Def4
.= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:26
.= f.v2 * v2 by FINSEQ_4:26;
hence thesis by A1,A3,FINSEQ_1:61;
end;
theorem Th44:
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def4
.= 3 by FINSEQ_1:62; then
A2: dom(f (#)<* v1,v2,v3 *>) = {1,2,3} & 1 in {1,2,3} & 2 in {1,2,3} &
3 in {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1; then
A3: (f (#) <* v1,v2,v3 *>).1
= f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1 by Def4
.= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:27
.= f.v1 * v1 by FINSEQ_4:27;
A4: (f (#) <* v1,v2,v3 *>).2
= f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2 by A2,Def4
.= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:27
.= f.v2 * v2 by FINSEQ_4:27;
(f (#) <* v1,v2,v3 *>).3
= f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3 by A2,Def4
.= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:27
.= f.v3 * v3 by FINSEQ_4:27;
hence thesis by A1,A3,A4,FINSEQ_1:62;
end;
reserve K,L,L1,L2,L3 for C_Linear_Combination of V;
definition
let V be Abelian add-associative right_zeroed
right_complementable non empty CLSStruct;
let L be C_Linear_Combination of V;
func Sum L -> Element of V means :Def5:
ex F being FinSequence of the carrier of V
st F is one-to-one & rng F = Carrier L & it = Sum(L (#) F);
existence
proof
consider F being FinSequence such that
A1: rng F = Carrier L & F is one-to-one by FINSEQ_4:73;
reconsider F as FinSequence of the carrier of V by A1,FINSEQ_1:def 4;
take Sum(L (#) F);
take F;
thus thesis by A1;
end;
uniqueness
proof
let v1,v2 be Element of V;
given F1 being FinSequence of the carrier of V such that
A3: F1 is one-to-one & rng F1 = Carrier L & v1 = Sum(L (#) F1);
given F2 being FinSequence of the carrier of V such that
A6: F2 is one-to-one & rng F2 = Carrier L & v2 = Sum(L (#) F2);
set G1 = L (#) F1; set G2 = L (#) F2;
A9: len F1 = len F2 & len G1 = len F1 & len G2 = len F2
by A3,A6,Def4,FINSEQ_1:65;
A10: dom F1 = Seg len F1 & dom F2 = Seg len F2 &
dom G1 = Seg len G1 & dom G2 = Seg len G2 by FINSEQ_1:def 3;
defpred P[set,set] means {$2} = F1"{F2.$1};
A12: for x st x in dom F1 ex y st y in dom F1 & P[x,y]
proof let x;
assume x in dom F1;
then F2.x in rng F1 by A3,A6,A9,A10,FUNCT_1:def 5;
then consider y such that A13: F1"{F2.x} = {y} by A3,FUNCT_1:144;
take y;
y in F1"{F2.x} by A13,TARSKI:def 1;
hence thesis by A13,FUNCT_1:def 13;
end;
consider f being Function of dom F1, dom F1 such that
A15: for x st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A16: rng f = dom F1
proof
thus rng f c= dom F1 by RELSET_1:12;
let y;
assume A17: y in dom F1; then
F1.y in rng F2 by A3,A6,FUNCT_1:def 5; then
consider x such that
A18: x in dom F2 & F2.x = F1.y by FUNCT_1:def 5;
A20: x in dom f by A9,A10,A18,FUNCT_2:def 1;
F1"{F2.x} = F1"Im(F1,y) by A17,A18,FUNCT_1:117; then
F1"{F2.x} c= {y} by A3,FUNCT_1:152; then
{f.x} c= {y} by A9,A10,A15,A18; then
f.x = y by ZFMISC_1:24;
hence thesis by A20,FUNCT_1:def 5;
end;
f is one-to-one
proof let y1,y2;
assume that A21: y1 in dom f & y2 in dom f and A22: f.y1 = f.y2;
A24: F1"{F2.y1} = {f.y1} & F1"{F2.y2} = {f.y2} by A15,A21;
F2.y1 in rng F1 & F2.y2 in rng F1 by A3,A6,A9,A10,A21,FUNCT_1:def 5; then
{F2.y1} c= rng F1 & {F2.y2} c= rng F1 by ZFMISC_1:37; then
{F2.y1} = {F2.y2} by A22,A24,FUNCT_1:161; then
F2.y1 = F2.y2 & y1 in dom F2 & y2 in dom F2
by A9,A10,A21,ZFMISC_1:6;
hence thesis by A6,FUNCT_1:def 8;
end;
then reconsider f as Permutation of dom F1 by A16,FUNCT_2:83;
dom F1 = Seg len F1 & dom G1 = Seg len G1 by FINSEQ_1:def 3;
then reconsider f as Permutation of dom G1 by A9;
now
let i be Element of NAT;
assume A25: i in dom G2; then
i in dom f by A9,A10,FUNCT_2:def 1; then
A26: f.i in dom F1 by A16,FUNCT_1:def 5; then
reconsider m = f.i as Element of NAT;
{F1.(f.i)} = Im(F1,f.i) by A26,FUNCT_1:117
.= F1.:(F1"{F2.i}) by A9,A10,A15,A25; then
{F1.(f.i)} c= {F2.i} by FUNCT_1:145; then
F2.i = F1.m & G2.i = L.(F2/.i) * F2/.i &
G1.m = L.(F1/.m) * F1/.m & F1.m = F1/.m & F2.i = F2/.i
by A9,A10,A25,A26,Def4,PARTFUN1:def 8,ZFMISC_1:24;
hence G2.i = G1.(f.i);
end;
hence thesis by A3,A6,A9,RLVECT_2:8;
end;
end;
theorem Lm2:
for V being Abelian add-associative right_zeroed
right_complementable non empty CLSStruct holds
Sum(ZeroCLC V) = 0.V
proof
let V be Abelian add-associative right_zeroed
right_complementable non empty CLSStruct;
consider F being FinSequence of the carrier of V
such that F is one-to-one and
A1: rng F = Carrier (ZeroCLC V) & Sum(ZeroCLC V) = Sum(ZeroCLC V (#) F)
by Def5;
F = {} by A1,RELAT_1:64;
then len(ZeroCLC V (#) F) = 0 by Def4,CARD_1:47;
hence thesis by A1,RLVECT_1:94;
end;
theorem
for V being ComplexLinearSpace,
A being Subset of V holds
A <> {} implies ( A is linearly-closed iff
for l being C_Linear_Combination of A holds Sum l in A )
proof
let V be ComplexLinearSpace;
let A be Subset of V;
assume A1: A <> {};
thus A is linearly-closed implies
for l being C_Linear_Combination of A holds Sum l in A
proof
assume A2: A is linearly-closed;
defpred P[Nat] means
for l being C_Linear_Combination of A
st card(Carrier l) = $1 holds Sum l in A;
now let l be C_Linear_Combination of A;
assume card(Carrier l) = 0;
then Carrier l = {} by CARD_2:59;
then l = ZeroCLC V by Def2;
then Sum l = 0.V by Lm2;
hence Sum l in A by A1,A2,CLVECT_1:21;
end; then
A3: P[0];
A4: for k be Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume A5: P[k];
hereby let l be C_Linear_Combination of A;
consider F being FinSequence of the carrier of V such that
A7: F is one-to-one & rng F = Carrier l & Sum l = Sum(l (#) F) by Def5;
assume A6: card(Carrier l) = k + 1; then
A10: len F = k + 1 by A7,FINSEQ_4:77;
reconsider G = F | Seg k as FinSequence of the carrier of V
by FINSEQ_1:23;
A11: len G = k by A10,FINSEQ_3:59;
A12: k + 1 in Seg(k + 1) by FINSEQ_1:6;
then reconsider v = F.(k + 1) as VECTOR of V by A10,RLVECT_1:54;
A13: k + 1 in dom F by A10,A12,FINSEQ_1:def 3;
then A14: v in Carrier l & Carrier l c= A by A7,Def3,FUNCT_1:def 5;
then A15: l.v * v in A by A2,CLVECT_1:def 4;
deffunc F(Element of V)= l.$1;
consider f being Function of the carrier of V, COMPLEX such that
A16: f.v = 0c &
for u being Element of V st u <> v holds f.u = F(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, COMPLEX)
by FUNCT_2:11;
now let u be VECTOR of V;
assume not u in Carrier l; then
l.u = 0c;
hence f.u = 0c by A16;
end;
then reconsider f as C_Linear_Combination of V by Def1;
A19: Carrier f = Carrier l \ {v}
proof
now let x;
assume x in Carrier f;
then A20: ex u being VECTOR of V st u = x & f.u <> 0c;
then f.x = l.x by A16;
then x in Carrier l & not x in {v} by A16,A20,TARSKI:def 1;
hence x in Carrier l \ {v} by XBOOLE_0:def 4;
end;
hence Carrier f c= Carrier l \ {v} by TARSKI:def 3;
let x;
assume A21: x in Carrier l \ {v};
then A22:x in Carrier l & not x in {v} by XBOOLE_0:def 4; then
x <> v by TARSKI:def 1; then
A23: l.x = f.x by A16,A21;
ex u being VECTOR of V st x = u & l.u <> 0c by A22;
hence thesis by A23;
end;
then Carrier f c= A \ {v} by A14,XBOOLE_1:33;
then Carrier f c= A by XBOOLE_1:106;
then reconsider f as C_Linear_Combination of A by Def3;
A23: G is one-to-one by A7,FUNCT_1:84;
A24: rng G = Carrier f
proof
thus rng G c= Carrier f
proof
let x;
assume x in rng G;
then consider y such that
A25: y in dom G & G.y = x by FUNCT_1:def 5;
reconsider y as Element of NAT by A25;
dom G c= dom F by RELAT_1:89;
then A27: y in dom F & G.y = F.y by A25,FUNCT_1:70;
then A28: x in rng F by A25,FUNCT_1:def 5;
x = v implies k + 1 = y & y <= k & k < k + 1
by A7,A11,A13,A25,A27,FINSEQ_3:27,FUNCT_1:def 8,XREAL_1:31;
then not x in {v} by TARSKI:def 1;
hence thesis by A7,A19,A28,XBOOLE_0:def 4;
end;
let x;
assume A29: x in Carrier f;
then x in rng F by A7,A19,XBOOLE_0:def 4;
then consider y such that A30: y in dom F & F.y = x by FUNCT_1:def 5;
now assume not y in Seg k;
then y in dom F \ Seg k by A30,XBOOLE_0:def 4;
then y in Seg(k + 1) \ Seg k by A10,FINSEQ_1:def 3;
then y in {k + 1} by FINSEQ_3:16;
then y = k + 1 by TARSKI:def 1;
then not v in {v} by A19,A29,A30,XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A30,XBOOLE_0:def 3;
then A32: y in dom G by RELAT_1:90;
then G.y = F.y by FUNCT_1:70;
hence thesis by A30,A32,FUNCT_1:def 5;
end;
then A33: Sum(f (#) G) = Sum f by A23,Def5;
A34: len(l (#) F) = k + 1 & len (f (#) G) = k by A10,A11,Def4;
Seg(k + 1) /\ Seg k = Seg k by NAT_1:12, FINSEQ_1:9
.= dom(f (#) G) by A34,FINSEQ_1:def 3;
then A35: dom(f (#) G) = dom(l (#) F) /\ Seg k by A34,FINSEQ_1:def 3;
now
let x;
assume A36: x in dom(f (#) G); then
A37: x in dom G by A11,A34,FINSEQ_3:31;
then A38: G.x in rng G by FUNCT_1:def 5;
reconsider u = G.x as VECTOR of V by A38;
not u in {v} by A19,A24,A38,XBOOLE_0:def 4;
then A39: u <> v by TARSKI:def 1;
A40: (f (#) G).x = f.u * u by A37,Th40
.= l.u * u by A16,A39;
x in dom(l (#) F) by A35,A36,XBOOLE_0:def 3;
then A41: x in dom F by A10,A34,FINSEQ_3:31;
F.x = u by A37,FUNCT_1:70;
hence (f (#) G).x = (l (#) F).x by A40,A41,Th40;
end;
then A42: f (#) G = (l (#) F) | Seg k by A35,FUNCT_1:68;
A43: dom(f (#) G) = Seg len (f (#) G) by FINSEQ_1:def 3;
(l (#) F).(len F) = l.v * v by A10,A13,Th40;
then A44: Sum(l (#) F) = Sum(f (#) G) + l.v * v
by A10,A34,A42,A43,RLVECT_1:55;
v in rng F by A13,FUNCT_1:def 5; then
{v} c= Carrier l by A7,ZFMISC_1:37;
then card(Carrier f) = k + 1 - card{v} by A6,A19,CARD_2:63;
then card(Carrier f) = k + 1 - 1 by CARD_1:79;
then Sum f in A by A5;
hence Sum l in A by A2,A7,A15,A33,A44,CLVECT_1:def 4;
end;
end;
A45: for k be Element of NAT holds P[k] from NAT_1:sch 1(A3,A4);
let l be C_Linear_Combination of A;
card(Carrier l) = card(Carrier l);
hence Sum l in A by A45;
end;
assume A46: for l be C_Linear_Combination of A holds Sum l in A;
ZeroCLC V is C_Linear_Combination of A & Sum(ZeroCLC V) = 0.V by Lm2,Th34;
then A47: 0.V in A by A46;
A48: for a being Complex,v being VECTOR of V st v in A holds a * v in A
proof
let a be Complex, v be VECTOR of V;
assume A49: v in A;
now assume A50: a <> 0;
deffunc F(Element of V) = 0c;
consider f being Function of the carrier of V, COMPLEX such that
A51: f.v = a &
for u being Element of V st u <> v holds f.u = F(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:11;
now let u be VECTOR of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0 by A51;
end;
then reconsider f as C_Linear_Combination of V by Def1;
A53: Carrier f = {v}
proof
now let x;
assume x in Carrier f;
then ex u being VECTOR of V st x = u & f.u <> 0; then
x = v by A51;
hence x in {v} by TARSKI:def 1;
end;
hence Carrier f c= {v} by TARSKI:def 3;
let x;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A50,A51;
end;
{v} c= A by A49,ZFMISC_1:37;
then reconsider f as C_Linear_Combination of A by A53,Def3;
consider F being FinSequence of the carrier of V such that
A55: F is one-to-one & rng F = Carrier f & Sum(f(#)F) = Sum f by Def5;
F = <* v *> by A53,A55,FINSEQ_3:106;
then f (#) F = <* f.v * v *> by Th42;
then Sum f = a * v by A51,A55,RLVECT_1:61;
hence a * v in A by A46;
end;
hence thesis by A47,CLVECT_1:2;
end;
for v,u being VECTOR of V st v in A & u in A holds v + u in A
proof let v,u be VECTOR of V;
assume A58: v in A & u in A;
C: 1r * u = u & 1r * v = v by CLVECT_1:def 2; then
B: v + v = (1r + 1r) * v by CLVECT_1:def 2;
now assume A60: v <> u;
deffunc F(Element of V)=0c;
consider f being Function of the carrier of V, COMPLEX
such that A61: f.v = 1r & f.u = 1r and
A63: for w being Element of V st w <> v & w <> u holds
f.w = F(w) from FUNCT_2:sch 7(A60);
reconsider f as Element of Funcs(the carrier of V, COMPLEX)
by FUNCT_2:11;
now let w be VECTOR of V;
assume not w in {v,u};
then w <> v & w <> u by TARSKI:def 2;
hence f.w = 0 by A63;
end;
then reconsider f as C_Linear_Combination of V by Def1;
A64: Carrier f = {v,u}
proof
thus Carrier f c= {v,u}
proof
let x;
assume x in Carrier f;
then ex w being VECTOR of V st x = w & f.w <> 0c;
then x = v or x = u by A63;
hence thesis by TARSKI:def 2;
end;
let x;
assume x in {v,u};
then (x = v or x = u) & 0c <> 1r by TARSKI:def 2;
hence thesis by A61;
end;
then Carrier f c= A by A58,ZFMISC_1:38;
then reconsider f as C_Linear_Combination of A by Def3;
consider F being FinSequence of the carrier of V such that
A65: F is one-to-one & rng F = Carrier f & Sum(f (#) F) = Sum f by Def5;
F = <* v,u *> or F = <* u,v *> by A60,A64,A65,FINSEQ_3:108; then
(f(#)F = <* 1r*v, 1r*u *> or f(#)F = <* 1r*u, 1r*v *>) by A61,Th43;
then Sum f = v + u by A65,C,RLVECT_1:62;
hence v + u in A by A46;
end;
hence thesis by B,A48,A58;
end;
hence thesis by A48,CLVECT_1:def 4;
end;
theorem
for V being Abelian add-associative right_zeroed
right_complementable non empty CLSStruct,
l being C_Linear_Combination of {}(the carrier of V) holds
Sum l = 0.V
proof
let V be Abelian add-associative right_zeroed
right_complementable non empty CLSStruct;
let l be C_Linear_Combination of {}(the carrier of V);
l = ZeroCLC V by Th35;
hence thesis by Lm2;
end;
theorem Th50:
for V being ComplexLinearSpace,
v being VECTOR of V,
l being C_Linear_Combination of {v} holds Sum l = l.v * v
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let l be C_Linear_Combination of {v};
A1: Carrier l c= {v} by Def3;
per cases by A1,ZFMISC_1:39;
suppose Carrier l = {};
then A2: l = ZeroCLC V by Def2;
hence Sum l = 0.V by Lm2
.= 0c * v by CLVECT_1:2
.= l.v * v by A2,Th30;
end;
suppose Carrier l = {v};
then consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = {v} & Sum l = Sum(l (#) F) by Def5;
F = <* v *> by A3,FINSEQ_3:106;
then l (#) F = <* l.v * v *> by Th42;
hence thesis by A3,RLVECT_1:61;
end;
end;
theorem Th51:
for V being ComplexLinearSpace,
v1, v2 being VECTOR of V holds
v1 <> v2 implies
for l being C_Linear_Combination of {v1,v2} holds
Sum l = l.v1 * v1 + l.v2 * v2
proof
let V be ComplexLinearSpace;
let v1, v2 be VECTOR of V;
assume A1: v1 <> v2;
let l be C_Linear_Combination of {v1,v2};
A2: Carrier l c= {v1,v2} by Def3;
B1:0.V = 0c*v1 & 0.V = 0c*v2 by CLVECT_1:2;
per cases by A2,ZFMISC_1:42;
suppose Carrier l = {};
then A3: l = ZeroCLC V by Def2;
hence Sum l = 0.V by Lm2
.= 0.V + 0.V by RLVECT_1:10
.= l.v1 * v1 + 0c* v2 by A3,B1,Th30
.= l.v1 * v1 + l.v2 * v2 by A3,Th30;
end;
suppose A4: Carrier l = {v1};
then reconsider L = l as C_Linear_Combination of {v1} by Def3;
A5: not v2 in Carrier l by A1,A4,TARSKI:def 1;
Sum L = l.v1 * v1 by Th50; then
Sum l = l.v1 * v1 + 0.V by RLVECT_1:10;
hence Sum l = l.v1 * v1 + l.v2 * v2 by A5,B1;
end;
suppose A6: Carrier l = {v2};
then reconsider L = l as C_Linear_Combination of {v2} by Def3;
A7: not v1 in Carrier l by A1,A6,TARSKI:def 1;
Sum L = l.v2 * v2 by Th50; then
Sum l = 0.V + l.v2 * v2 by RLVECT_1:10;
hence Sum l = l.v1 * v1 + l.v2 * v2 by A7,B1;
end;
suppose Carrier l = {v1,v2};
then consider F being FinSequence of the carrier of V
such that A8: F is one-to-one & rng F = {v1,v2} and
A9: Sum l = Sum(l (#) F) by Def5;
F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:108;
then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or
l (#) F = <* l.v2 * v2, l.v1 * v1 *> by Th43;
hence Sum l = l.v1 * v1 + l.v2 * v2 by A9,RLVECT_1:62;
end;
end;
theorem
for V being Abelian add-associative right_zeroed
right_complementable non empty CLSStruct,
L being C_Linear_Combination of V holds
Carrier L = {} implies Sum L = 0.V
proof
let V be Abelian add-associative right_zeroed
right_complementable non empty CLSStruct;
let L be C_Linear_Combination of V;
assume Carrier L = {};
then L = ZeroCLC V by Def2;
hence thesis by Lm2;
end;
theorem
for V being ComplexLinearSpace,
L being C_Linear_Combination of V,
v being VECTOR of V holds
Carrier L = {v} implies Sum L = L.v * v
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v be VECTOR of V;
assume Carrier L = {v};
then L is C_Linear_Combination of {v} by Def3;
hence thesis by Th50;
end;
theorem Th54:
for V being ComplexLinearSpace,
L being C_Linear_Combination of V,
v1, v2 being VECTOR of V holds
Carrier L = {v1,v2} & v1 <> v2 implies Sum L = L.v1 * v1 + L.v2 * v2
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v1, v2 be VECTOR of V;
assume A1: Carrier L = {v1,v2} & v1 <> v2; then
L is C_Linear_Combination of {v1,v2} by Def3;
hence thesis by A1,Th51;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be C_Linear_Combination of V;
redefine pred L1 = L2 means
for v being Element of V holds L1.v = L2.v;
compatibility by FUNCT_2:113;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be C_Linear_Combination of V;
redefine func L1 + L2 -> C_Linear_Combination of V means
:Def6:
for v being Element of V holds it.v = L1.v + L2.v;
coherence
proof
reconsider f = L1+L2 as Element of Funcs(the carrier of V,COMPLEX)
by FUNCT_2:11;
now
let v be Element of V;
assume not v in Carrier(L1) \/ Carrier(L2);
then not v in Carrier(L1) & not v in Carrier(L2) by XBOOLE_0:def 2;
then L1.v = 0 & L2.v = 0;
hence f.v = 0 + 0 by VALUED_1:1
.= 0;
end;
hence thesis by Def1;
end;
compatibility
proof
let f be C_Linear_Combination of V;
thus f=L1+L2 implies
for v being Element of V holds f.v = L1.v + L2.v by VALUED_1:1;
dom f = the carrier of V & dom L1 = the carrier of V
& dom L2 = the carrier of V by FUNCT_2:169;
then
A1: dom f = dom L1 /\ dom L2;
assume for v being Element of V holds f.v = L1.v + L2.v; then
for c being set st c in dom f holds f.c = L1.c + L2.c;
hence f=L1+L2 by A1,VALUED_1:def 1;
end;
end;
theorem Th58:
Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2
proof
let x;
assume x in Carrier(L1 + L2);
then consider u such that A1: x = u & (L1 + L2).u <> 0c;
(L1 + L2).u = L1.u + L2.u by Def6;
then L1.u <> 0c or L2.u <> 0c by A1;
then x in Carrier L1 or x in Carrier L2 by A1;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th59:
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies
L1 + L2 is C_Linear_Combination of A
proof
assume L1 is C_Linear_Combination of A &
L2 is C_Linear_Combination of A;
then Carrier L1 c= A & Carrier L2 c= A by Def3;
then Carrier L1 \/ Carrier L2 c= A &
Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2 by Th58,XBOOLE_1:8;
hence Carrier(L1 + L2) c= A by XBOOLE_1:1;
end;
definition let V,A; let L1,L2 be C_Linear_Combination of A;
redefine func L1 + L2 -> C_Linear_Combination of A;
coherence by Th59;
end;
theorem
for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V holds
L1 + L2 = L2 + L1;
theorem Th61:
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def6
.= L1.v + (L2.v + L3.v) by Def6
.= L1.v + L2.v + L3.v
.= (L1 + L2).v + L3.v by Def6
.= (L1 + L2 + L3).v by Def6;
end;
theorem Th62:
L + ZeroCLC V = L
proof
let v;
thus (L + ZeroCLC V).v = L.v + (ZeroCLC V).v by Def6
.= L.v + 0c by Th30
.= L.v;
end;
definition
let V,a; let L;
func a * L -> C_Linear_Combination of V means :Def7:
for v holds it.v = a * L.v;
existence
proof
deffunc F(Element of V)=a * L.$1;
consider f being Function of the carrier of V, COMPLEX such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:11;
now
let v;
assume not v in Carrier L;
then L.v = 0c;
hence f.v = a * 0c by A1
.= 0c;
end;
then reconsider f as C_Linear_Combination of V by Def1;
take f;
let v;
thus f.v = a * L.v by A1;
thus thesis;
end;
uniqueness
proof
let L1,L2;
assume A2: for v holds L1.v = a * L.v;
assume A3: for v holds L2.v = a * L.v;
let v;
thus L1.v = a * L.v by A2
.= L2.v by A3;
end;
end;
theorem Th65:
a <> 0c implies Carrier (a * L) = Carrier L
proof
assume A1: a <> 0c;
set T = {u : (a * L).u <> 0c}; set S = {v : L.v <> 0c};
T = S
proof
thus T c= S
proof
let x;
assume x in T;
then consider u such that A3: x = u & (a * L).u <> 0c;
(a * L).u = a * L.u by Def7;
then L.u <> 0c by A3;
hence thesis by A3;
end;
let x;
assume x in S;
then consider v such that A5: x = v & L.v <> 0c;
(a * L).v = a * L.v by Def7;
then (a * L).v <> 0c by A1,A5,XCMPLX_1:6;
hence thesis by A5;
end;
hence thesis;
end;
theorem Th66:
0c * L = ZeroCLC V
proof
let v;
thus (0c * L).v = 0c * L.v by Def7
.= (ZeroCLC V).v by Th30;
end;
theorem Th67:
L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A
proof
assume A1: L is C_Linear_Combination of A;
A2:a = 0c implies a*L = ZeroCLC V by Th66;
now assume a <> 0c;
then Carrier (a * L) = Carrier L & Carrier L c= A by A1,Def3,Th65;
hence a*L is C_Linear_Combination of A by Def3;
end;
hence thesis by A2,Th34;
end;
theorem Th68:
(a + b) * L = a * L + b * L
proof
let v;
thus ((a + b) * L).v = (a + b) * L.v by Def7
.= a * L.v + b * L.v
.= (a * L).v + b * L.v by Def7
.= (a * L).v + (b * L). v by Def7
.= ((a * L) + (b * L)).v by Def6;
end;
theorem Th69:
a * (L1 + L2) = a * L1 + a * L2
proof
let v;
thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def7
.= a * (L1.v + L2.v) by Def6
.= a * L1.v + a * L2.v
.= (a * L1).v + a * L2.v by Def7
.= (a * L1).v + (a * L2). v by Def7
.= ((a * L1) + (a * L2)).v by Def6;
end;
theorem Th70:
a * (b * L) = (a * b) * L
proof
let v;
thus (a * (b * L)).v = a * (b * L).v by Def7
.= a * (b * L.v) by Def7
.= a * b * L.v
.= ((a * b) * L).v by Def7;
end;
theorem Th71:
1r * L = L
proof
let v;
thus (1r * L).v = 1r * L.v by Def7
.= L.v;
end;
definition
let V,L;
func - L -> C_Linear_Combination of V equals (- 1r) * L;
correctness;
end;
theorem Th73:
(- L).v = - L.v
proof
thus (- L).v = (- 1r) * L.v by Def7
.= - L.v;
end;
theorem
L1 + L2 = ZeroCLC V implies L2 = - L1
proof
assume A1: L1 + L2 = ZeroCLC V;
let v;
L1.v + L2.v = (ZeroCLC V).v by A1,Def6
.= 0c by Th30;
hence L2.v = - L1.v
.= (- L1).v by Th73;
end;
theorem
- (- L) = L
proof
let v;
thus (- (- L)).v = ((- 1r) * (- 1r) * L).v by Th70
.= 1r * L.v by Def7
.= L.v;
end;
definition let V; let L1,L2;
func L1 - L2 -> C_Linear_Combination of V equals
L1 + (- L2);
correctness;
end;
theorem Th79:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by Def6
.= L1.v - L2.v by Th73;
end;
theorem
Carrier(L1 - L2) c= Carrier L1 \/ Carrier L2
proof
Carrier(L1 - L2) c= Carrier L1 \/ Carrier -L2 by Th58;
hence thesis by Th65;
end;
theorem
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A
implies L1 - L2 is C_Linear_Combination of A
proof
assume A1: L1 is C_Linear_Combination of A &
L2 is C_Linear_Combination of A; then
- L2 is C_Linear_Combination of A by Th67;
hence thesis by A1,Th59;
end;
theorem Th82:
L - L = ZeroCLC V
proof
let v;
thus (L - L).v = L.v - L.v by Th79
.= (ZeroCLC V).v by Th30;
end;
definition let V;
func C_LinComb V -> set means
:Def8: x in it iff x is C_Linear_Combination of V;
existence
proof
defpred P[set] means $1 is C_Linear_Combination of V;
consider A being set such that
A1: for x holds x in A iff x in Funcs(the carrier of V, COMPLEX) &
P[x] from XBOOLE_0:sch 1;
take A;
let x;
thus x in A implies x is C_Linear_Combination of V by A1;
assume x is C_Linear_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set;
assume A2: for x holds x in D1 iff x is C_Linear_Combination of V;
assume A3: for x holds x in D2 iff x is C_Linear_Combination of V;
thus D1 c= D2
proof
let x;
assume x in D1;
then x is C_Linear_Combination of V by A2;
hence thesis by A3;
end;
let x;
assume x in D2;
then x is C_Linear_Combination of V by A3;
hence thesis by A2;
end;
end;
registration let V;
cluster C_LinComb V -> non empty;
coherence
proof
consider x being C_Linear_Combination of V;
x in C_LinComb V by Def8;
hence thesis;
end;
end;
reserve e,e1,e2 for Element of C_LinComb V;
definition let V; let e;
func @e -> C_Linear_Combination of V equals e;
coherence by Def8;
end;
definition let V; let L;
func @L -> Element of C_LinComb V equals L;
coherence by Def8;
end;
definition let V;
func C_LCAdd V -> BinOp of C_LinComb V means :Def9:
for e1,e2 holds it.(e1,e2) = @e1 + @e2;
existence
proof
deffunc F(Element of C_LinComb V,Element of C_LinComb V)=@(@$1 + @$2);
consider o being BinOp of C_LinComb V such that
A1: for e1,e2 holds o.(e1,e2) = F(e1,e2) from BINOP_1:sch 4;
take o;
let e1,e2;
thus o.(e1,e2) = @(@e1 + @e2) by A1
.= @e1 + @e2;
end;
uniqueness
proof
let o1,o2 be BinOp of C_LinComb V;
assume A2: for e1,e2 holds o1.(e1,e2) = @e1 + @e2;
assume A3: for e1,e2 holds o2.(e1,e2) = @e1 + @e2;
now
let e1,e2;
thus o1.(e1,e2) = @e1 + @e2 by A2
.= o2.(e1,e2) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition let V;
func C_LCMult V -> Function of [:COMPLEX,C_LinComb V:], C_LinComb V
means :Def10:
for a,e holds it.[a,e] = a * @e;
existence
proof
defpred P[Element of COMPLEX,Element of C_LinComb V,set] means
ex a st a = $1 & $3 = a * @$2;
A1: for x being (Element of COMPLEX), e1 ex e2 st P[x,e1,e2]
proof
let x be (Element of COMPLEX), e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:COMPLEX,C_LinComb V:], C_LinComb V
such that
A2: for x being (Element of COMPLEX), e holds P[x,e,g.(x,e)]
from BINOP_1:sch 3(A1);
take g;
let a,e;
ex b st b = a & g.(a,e) = b * @e by A2;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of [:COMPLEX,C_LinComb V:], C_LinComb V;
assume A3: for a,e holds g1.[a,e] = a * @e;
assume A4: for a,e holds g2.[a,e] = a * @e;
now
let x be (Element of COMPLEX), e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
definition let V;
func LC_CLSpace V -> ComplexLinearSpace equals
CLSStruct (# C_LinComb V, @ZeroCLC V, C_LCAdd V, C_LCMult V #);
coherence
proof
set S = CLSStruct (# C_LinComb V, @ZeroCLC V, C_LCAdd V, C_LCMult V #);
X0: now
let a,b be Complex, v,u,w be VECTOR of S;
reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a * v,
az = a * w, bx = b * v as Element of C_LinComb V;
@x = v & @y = u & @z = w & @yx = u + v & @xz = v + w & @ax = a * v &
@az = a * w & @bx = b * v;
then reconsider K = v, L = u, M = w, LK = u + v, KM = v + w, aK = a * v,
aM = a * w, bK = b * v as C_Linear_Combination of V;
A1: now
let v,u be (VECTOR of S), K,L;
assume A2: v = K & u = L;
@@K = K & @@L = L;
hence v + u = K + L by A2,Def9;
end;
A4: now
let v be (VECTOR of S), L,a;
assume v = L; then
(C_LCMult V).[a,v] = a*@@L by Def10;
hence a*v = a*L;
end;
thus v + w = K + M by A1
.= w + v by A1;
thus (u + v) + w = LK + M by A1
.= L + K + M by A1
.= L + (K + M) by Th61
.= L + KM by A1
.= u + (v + w) by A1;
thus v + 0.S = K + ZeroCLC V by A1
.= v by Th62;
- K in the carrier of S by Def8;
then - K in S by STRUCT_0:def 5;
then - K = vector(S,- K) by RLVECT_2:def 1;
then v + vector(S,- K) = K - K by A1
.= 0.S by Th82;
hence ex w being VECTOR of S st v + w = 0.S;
thus a * (v + w) = a * KM by A4
.= a * (K + M) by A1
.= a * K + a * M by Th69
.= aK + a * M by A4
.= aK + aM by A4
.= a * v + a * w by A1;
thus (a + b) * v = (a + b) * K by A4
.= a * K + b * K by Th68
.= aK + b * K by A4
.= aK + bK by A4
.= a * v + b * v by A1;
thus (a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th70
.= a * (bK) by A4
.= a * (b * v) by A4;
thus 1r * v = 1r * K by A4
.= v by Th71;
end;
then
X1:
(for v,w being VECTOR of S holds v + w = w + v) &
(for u,v,w being VECTOR of S holds (u + v) + w = u + (v + w)) &
(for v being VECTOR of S holds v + 0.S = v) &
(for v being VECTOR of S
ex w being VECTOR of S st v + w = 0.S) &
(for a for v,w being VECTOR of S holds a * (v + w) = a * v + a * w) &
(for a,b for v being VECTOR of S holds (a + b) * v = a * v + b * v) &
(for a,b for v being VECTOR of S holds (a * b) * v = a * (b * v)) &
for v being VECTOR of S holds 1r * v = v;
now let v be Element of S;
ex w be VECTOR of S st v + w = 0.S by X0;
hence v is right_complementable by ALGSTR_0:def 11;
end;
hence S is ComplexLinearSpace
by X1,CLVECT_1:def 2,RLVECT_1:def 5,def 6,def 7,ALGSTR_0:def 16;
end;
end;
registration let V;
cluster LC_CLSpace V -> strict non empty;
coherence;
end;
theorem Th96:
vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = L1 + L2
proof
set v1 = vector(LC_CLSpace V,L1);
set v2 = vector(LC_CLSpace V,L2);
L1 in the carrier of LC_CLSpace V &
L2 in the carrier of LC_CLSpace V by Def8;
then A1: L1 in LC_CLSpace V & L2 in LC_CLSpace V by STRUCT_0:def 5;
A2: L1 = @@L1 & L2 = @@L2;
thus vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2)
= (C_LCAdd V).[L1,v2] by A1,RLVECT_2:def 1
.= (C_LCAdd V).(@L1,@L2) by A1,RLVECT_2:def 1
.= L1 + L2 by A2,Def9;
end;
theorem Th97:
a * vector(LC_CLSpace V,L) = a * L
proof
L in the carrier of LC_CLSpace V by Def8; then
L in LC_CLSpace V by STRUCT_0:def 5; then
A1:(C_LCMult V).[a,vector(LC_CLSpace V,L)]
= (C_LCMult V).[a,@L] by RLVECT_2:def 1;
@@L = L;
hence a * vector(LC_CLSpace V,L) = a * L by A1,Def10;
end;
theorem Th98:
- vector(LC_CLSpace V,L) = - L
proof
thus - vector(LC_CLSpace V,L)
= (- 1r) * (vector(LC_CLSpace V,L)) by CLVECT_1:4
.= - L by Th97;
end;
theorem
vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2
proof
- L2 in C_LinComb V &
the carrier of LC_CLSpace V = C_LinComb V by Def8;
then A1: - L2 in LC_CLSpace V by STRUCT_0:def 5;
- vector(LC_CLSpace V,L2)
= - L2 by Th98
.= vector(LC_CLSpace V,- L2) by A1,RLVECT_2:def 1;
hence vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2 by Th96;
end;
definition let V; let A;
func LC_CLSpace A -> strict Subspace of LC_CLSpace V means
the carrier of it = {l : not contradiction};
existence
proof
set X = {l : not contradiction};
X c= the carrier of LC_CLSpace V
proof
let x;
assume x in X;
then ex l st x = l;
hence thesis by Def8;
end;
then reconsider X as Subset of LC_CLSpace V;
ZeroCLC V is C_Linear_Combination of A by Th34;
then A1: ZeroCLC V in X;
B1: for v,u being VECTOR of LC_CLSpace V st v in X & u in X holds v + u in X
proof
let v,u be VECTOR of LC_CLSpace V;
assume that A2: v in X & u in X;
consider l1 such that A4: v = l1 by A2;
consider l2 such that A5: u = l2 by A2;
v = vector(LC_CLSpace V,l1) &
u = vector(LC_CLSpace V,l2) by A4,A5,RLVECT_2:3;
then v + u = l1 + l2 by Th96;
hence thesis;
end;
for a being Complex, v being VECTOR of LC_CLSpace V st v in X holds a*v in X
proof
let a be Complex;
let v be VECTOR of LC_CLSpace V;
assume v in X;
then consider l such that A6: v = l;
a * v = a * vector(LC_CLSpace V,l) by A6,RLVECT_2:3
.= a * l by Th97;
then a * v is C_Linear_Combination of A by Th67;
hence thesis;
end; then
X is linearly-closed by B1,CLVECT_1:def 4;
hence thesis by A1,CLVECT_1:55;
end;
uniqueness by CLVECT_1:50;
end;
begin :: Preliminaries for Complex Convex Sets
definition
let V be ComplexLinearSpace, W be Subspace of V;
func Up W -> Subset of V equals
the carrier of W;
coherence by CLVECT_1:def 5;
end;
registration
let V be ComplexLinearSpace, W be Subspace of V;
cluster Up W -> non empty;
coherence;
end;
definition
let V be non empty CLSStruct, S be Subset of V;
attr S is Affine means :Def101:
for x,y being VECTOR of V, z being Complex st
(ex a being Real st a = z) &
x in S & y in S holds (1r - z) * x + z * y in S;
end;
definition
let V be ComplexLinearSpace;
func (Omega).V -> strict Subspace of V equals
the CLSStruct of V;
coherence
proof
set W = the CLSStruct of V;
W is Abelian add-associative right_zeroed
right_complementable ComplexLinearSpace-like
proof
thus for v,w being VECTOR of W holds v + w = w + v
proof
let v,w be VECTOR of W;
reconsider v'=v,w'=w as VECTOR of V;
v+w = v'+w';
hence v + w = w' + v' .= w + v;
end;
thus 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 u'=u,v'=v,w'=w as VECTOR of V;
(u' + v') + w' = u' + (v' + w') by RLVECT_1:def 6;
hence (u + v) + w = u + (v + w);
end;
thus for v being VECTOR of W holds v + 0.W = v
proof
let v be VECTOR of W;
reconsider v'=v as VECTOR of V;
thus v + 0.W = v' + 0.V .= v by RLVECT_1:10;
end;
for v being VECTOR of W holds v is right_complementable
proof
let v be VECTOR of W;
reconsider v' = v as VECTOR of V;
v' is right_complementable by ALGSTR_0:def 16; then
consider w' being VECTOR of V such that
A2: v' + w' = 0.V by ALGSTR_0:def 11;
reconsider w = w' as VECTOR of W;
take w;
thus v + w = 0.W by A2;
end;
hence W is right_complementable by ALGSTR_0:def 16;
thus for a for v,w being VECTOR of W holds a * (v + w) = a * v + a * w
proof
let a; let v,w be VECTOR of W;
reconsider v'=v,w'=w as VECTOR of V;
a * (v' + w') = a * v' + a * w' by CLVECT_1:def 2;
hence a * (v + w) = a * v + a * w;
end;
thus for a,b for v being VECTOR of W holds (a + b) * v = a * v + b * v
proof
let a,b; let v be VECTOR of W;
reconsider v'=v as VECTOR of V;
(a + b) * v' = a * v' + b * v' by CLVECT_1:def 2;
hence (a + b) * v = a * v + b * v;
end;
thus for a,b for v being VECTOR of W holds (a * b) * v = a * (b * v)
proof
let a,b; let v be VECTOR of W;
reconsider v'=v as VECTOR of V;
(a * b) * v' = a * (b * v') by CLVECT_1:def 2;
hence (a * b) * v = a * (b * v);
end;
thus for v being VECTOR of W holds 1r * v = v
proof
let v be VECTOR of W;
reconsider v'=v as VECTOR of V;
thus 1r * v = 1r * v' .= v by CLVECT_1:def 2;
end;
end;
then reconsider W as ComplexLinearSpace;
W is Subspace of V
proof
thus the carrier of W c= the carrier of V & 0.W = 0.V;
thus thesis by FUNCT_2:40;
end;
hence thesis;
end;
end;
Th100:
for V being non empty CLSStruct holds [#]V is Affine & {}V is Affine
proof
let V be non empty CLSStruct;
for x,y being VECTOR of V, z being Complex st
(ex a being Real st z=a ) & x in [#]V & y in [#]V
holds (1r - z) * x + z * y in [#]V;
hence [#]V is Affine by Def101;
for x,y being VECTOR of V, z being Complex st
(ex a being Real st z=a ) & x in {}V & y in {}V
holds (1r - z) * x + z * y in {}V;
hence thesis by Def101;
end;
registration
let V be non empty CLSStruct;
cluster [#]V -> Affine;
coherence by Th100;
cluster {}V -> Affine;
coherence by Th100;
end;
registration
let V be non empty CLSStruct;
cluster non empty Affine Subset of V;
existence
proof
take [#]V;
thus thesis;
end;
cluster empty Affine Subset of V;
existence
proof
take {}V;
thus thesis;
end;
end;
theorem Th101:
for a being real number, z being complex number holds
Re(a*z)=a*Re(z)
proof
let a be real number;
let z be complex number;
A1: a in REAL by XREAL_0:def 1;
Re(a * z)
= Re a * Re z - Im a * Im z by COMPLEX1:24
.= Re a * Re z - 0 * Im z by A1,COMPLEX1:def 3
.= a * Re (z) by A1,COMPLEX1:def 2;
hence thesis;
end;
theorem Th102:
for a being real number, z being complex number holds
Im(a*z) = a*Im(z)
proof
let a be real number;
let z be complex number;
A1: a in REAL by XREAL_0:def 1;
Im(a * z)
= Re a * Im z + Re z * Im a by COMPLEX1:24
.= Re a * Im z + Re z * 0 by A1,COMPLEX1:def 3
.= a * Im (z) by A1,COMPLEX1:def 2;
hence thesis;
end;
theorem Th103:
for a being real number , z being complex number
st ( 0<=a & a<=1 ) holds
|.a*z.| = a*|.z.| & |.(1r-a)*z.| = (1r-a)*|.z.|
proof
let a be real number;
let z be complex number;
assume A1: 0<=a & a<=1;
A2: 1-a >= 0 by A1,XREAL_1:50;
A3: |.a*z.| = |.a.|*|.z.| by COMPLEX1:151
.= a * |.z.| by A1,COMPLEX1:129;
|.(1r-a)*z.| = |.1r-a.|*|.z.| by COMPLEX1:151
.= (1r-a)*|.z.| by A2,COMPLEX1:129;
hence thesis by A3;
end;
begin :: Complex Convex Sets
definition
let V be non empty CLSStruct;
let M be Subset of V;
let r be Element of COMPLEX;
func r*M -> Subset of V equals
{r * v where v is Element of V: v in M};
coherence
proof
defpred P[set] means $1 in M;
deffunc F(Element of V) = r * $1;
{F(v) where v is Element of V: P[v]} is Subset of V from DOMAIN_1:sch 8;
hence thesis;
end;
end;
definition
let V be non empty CLSStruct;
let M be Subset of V;
attr M is convex means :Def202:
for u,v being VECTOR of V, z be Complex st
(ex r be Real st z=r & 0 < r & r < 1 ) & u in M & v in M
holds z*u + (1r-z)*v in M;
end;
theorem
for V being ComplexLinearSpace-like (non empty CLSStruct),
M being Subset of V, z being Complex st M is convex holds
z*M is convex
proof
let V be ComplexLinearSpace-like (non empty CLSStruct);
let M be Subset of V;
let z be Complex;
assume
A1: M is convex;
for u,v being VECTOR of V, s being Complex st
(ex p being Real st s=p & 0 < p & p < 1) & u in z*M & v in z*M
holds s*u + (1r-s)*v in z*M
proof
let u,v be VECTOR of V;
let s be Complex;
assume
A2: (ex p being Real st s=p & 0 < p & p < 1) & u in z*M & v in z*M;
then consider u' be Element of V such that
A3: u = z * u' & u' in M;
consider v' be Element of V such that
A4: v = z*v' & v' in M by A2;
A5: s*u + (1r-s)*v = s*z*u' + (1r-s)*(z*v') by A3,A4,CLVECT_1:def 2
.= z*s*u' + z*(1r-s)*v' by CLVECT_1:def 2
.= z*(s*u') + z*(1r-s)*v' by CLVECT_1:def 2
.= z*(s*u') + z*((1r-s)*v') by CLVECT_1:def 2
.= z*(s*u' + (1r-s)*v') by CLVECT_1:def 2;
s*u' + (1r-s)*v' in M by A1,A2,A3,A4,Def202;
hence thesis by A5;
end;
hence thesis by Def202;
end;
theorem
for V being Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct),
M,N being Subset of V st M is convex & N is convex holds
M + N is convex
proof
let V be Abelian add-associative
ComplexLinearSpace-like (non empty CLSStruct);
let M,N be Subset of V;
assume that
A1: M is convex & N is convex;
for u,v being VECTOR of V, z being Complex st
(ex r being Real st z=r & 0 < r & r < 1) & u in M+N & v in M+N
holds z*u + (1r-z)*v in M+N
proof
let u,v be VECTOR of V;
let z be Complex;
assume
A3: (ex r being Real st z=r & 0 < r & r < 1) & u in M+N & v in M+N;
then consider x1,y1 being Element of V such that
A4: u = x1 + y1 & x1 in M & y1 in N;
consider x2,y2 being Element of V such that
A5: v = x2 + y2 & x2 in M & y2 in N by A3;
A6: z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A3,A4,A5,Def202;
z*u + (1r-z)*v = z*x1 + z*y1 + (1r-z)*(x2+y2) by A4,A5,CLVECT_1:def 2
.= z*x1 + z*y1 + ((1r-z)*x2 + (1r-z)*y2) by CLVECT_1:def 2
.= z*x1 + z*y1 + (1r-z)*x2 + (1r-z)*y2 by RLVECT_1:def 6
.= z*x1 + (1r-z)*x2 + z*y1 + (1r-z)*y2 by RLVECT_1:def 6
.= (z*x1 + (1r-z)*x2) + (z*y1 + (1r-z)*y2) by RLVECT_1:def 6;
hence thesis by A6;
end;
hence thesis by Def202;
end;
theorem
for V being ComplexLinearSpace, M,N being Subset of V st
M is convex & N is convex holds M - N is convex
proof
let V be ComplexLinearSpace;
let M,N be Subset of V;
assume that
A1: M is convex & N is convex;
for u,v being VECTOR of V, z being Complex st
(ex r being Real st z=r & 0 < r & r < 1) & u in M-N & v in M-N
holds z*u + (1r-z)*v in M-N
proof
let u,v be VECTOR of V;
let z be Complex;
assume
A3: (ex r being Real st z=r & 0 < r & r < 1) & u in M-N & v in M-N; then
consider x1,y1 being Element of V such that
A4: u = x1 - y1 & x1 in M & y1 in N;
consider x2,y2 being Element of V such that
A5: v = x2 - y2 & x2 in M & y2 in N by A3;
A6: z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A3,A4,A5,Def202;
z*u + (1r-z)*v = z*x1 - z*y1 + (1r-z)*(x2-y2) by A4,A5,CLVECT_1:10
.= z*x1 - z*y1 + ((1r-z)*x2 - (1r-z)*y2) by CLVECT_1:10
.= z*x1 - z*y1 + (1r-z)*x2 - (1r-z)*y2 by RLVECT_1:def 6
.= z*x1 - (z*y1 - (1r-z)*x2) - (1r-z)*y2 by RLVECT_1:43
.= z*x1 + ((1r-z)*x2 + (-z*y1)) - (1r-z)*y2 by RLVECT_1:47
.= z*x1 + (1r-z)*x2 + (-z*y1) - (1r-z)*y2 by RLVECT_1:def 6
.= z*x1 + (1r-z)*x2 + ((-z*y1) - (1r-z)*y2) by RLVECT_1:def 6
.= (z*x1 + (1r-z)*x2) - (z*y1 + (1r-z)*y2) by RLVECT_1:44;
hence thesis by A6;
end;
hence thesis by Def202;
end;
theorem Th204:
for V being non empty CLSStruct, M being Subset of V holds
M is convex iff
( for z being Complex st (ex r being Real st z=r & 0 < r & r < 1) holds
z*M + (1r-z)*M c= M )
proof
let V be non empty CLSStruct;
let M be Subset of V;
A1: M is convex implies
(for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
holds z*M + (1r-z)*M c= M )
proof
assume A2: M is convex;
let z be Complex;
assume A3: ex r being Real st z=r & 0 < r & r < 1;
for x being Element of V st x in z*M + (1r-z)*M holds x in M
proof
let x be Element of V;
assume x in z*M + (1r-z)*M; then
consider u,v be Element of V such that
A4: x = u + v & u in z*M & v in (1r-z)*M;
A5: ex w1 be Element of V st u = z * w1 & w1 in M by A4;
ex w2 be Element of V st v = (1r-z)*w2 & w2 in M by A4;
hence thesis by A2,A3,A4,A5,Def202;
end;
hence thesis by SUBSET_1:7;
end;
( for z being Complex st ( ex r being Real st z=r & 0 < r & r < 1 )
holds z*M + (1r-z)*M c= M )
implies M is convex
proof
assume
A7: for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
holds z*M + (1r-z)*M c= M;
let u,v be VECTOR of V;
let z be Complex;
assume ex r being Real st z=r & 0 < r & r < 1; then
A11:z*M + (1r-z)*M c= M by A7;
assume u in M & v in M;
then z*u in z*M & (1r-z)*v in (1r-z)*M; then
z*u + (1r-z)*v in z*M + (1r-z)*M;
hence thesis by A11;
end;
hence thesis by A1;
end;
theorem
for V being Abelian (non empty CLSStruct), M being Subset of V st M is convex
holds
for z being Complex st (ex r being Real st z=r & 0 < r & r < 1) holds
(1r-z)*M + z*M c= M
proof
let V be Abelian (non empty CLSStruct);
let M be Subset of V;
assume A1: M is convex;
let z be Complex;
assume A2:ex r being Real st z=r & 0 < r & r < 1;
for x being Element of V st x in (1r-z)*M + z*M
holds x in M
proof
let x be Element of V;
assume x in (1r-z)*M + z*M;
then consider u,v be Element of V such that
A3: x = u + v & u in (1r-z)*M & v in z*M;
A4: ex w1 be Element of V st u = (1r-z) * w1 & w1 in M by A3;
ex w2 be Element of V st v = z*w2 & w2 in M by A3;
hence thesis by A1,A2,A3,A4,Def202;
end;
hence thesis by SUBSET_1:7;
end;
theorem
for V being Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct), M,N being Subset of V st
M is convex & N is convex holds
for z being Complex st (ex r being Real st z=r) holds
z*M + (1r-z)*N is convex
proof
let V be Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct);
let M,N be Subset of V;
assume that
A1: M is convex & N is convex;
let z be Complex such that ex r being Real st z=r;
let u,v be VECTOR of V;
let s be Complex;
assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4:u in z*M + (1r-z)*N & v in z*M + (1r-z)*N;
consider x1,y1 be VECTOR of V such that
A6:u = x1 + y1 & x1 in z*M & y1 in (1r-z)*N by A4;
consider x2,y2 be VECTOR of V such that
A7: v = x2 + y2 & x2 in z*M & y2 in (1r-z)*N by A4;
consider mx1 be VECTOR of V such that
A8:x1 = z*mx1 & mx1 in M by A6;
consider ny1 be VECTOR of V such that
A9: y1 = (1r-z)*ny1 & ny1 in N by A6;
consider mx2 be VECTOR of V such that
A10: x2 = z*mx2 & mx2 in M by A7;
consider ny2 be VECTOR of V such that
A11:y2 = (1r-z)*ny2 & ny2 in N by A7;
A12:s*mx1 + (1r-s)*mx2 in M & s*ny1 + (1r-s)*ny2 in N
by A1,A3,A8,A9,A10,A11,Def202;
s*x1 + (1r-s)*x2 = s*z*mx1 + (1r-s)*(z*mx2) by A8,A10,CLVECT_1:def 2
.= s*z*mx1 + (1r-s)*z*mx2 by CLVECT_1:def 2
.= z*(s*mx1) + (1r-s)*z*mx2 by CLVECT_1:def 2
.= z*(s*mx1) + z*((1r-s)*mx2) by CLVECT_1:def 2
.= z*(s*mx1 + (1r-s)*mx2) by CLVECT_1:def 2;
then
A14: s*x1 + (1r-s)*x2 in z*M by A12;
s*y1 + (1r-s)*y2
= s*(1r-z)*ny1 + (1r-s)*((1r-z)*ny2) by A9,A11, CLVECT_1:def 2
.= s*(1r-z)*ny1 + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 2
.= (1r-z)*(s*ny1) + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 2
.= (1r-z)*(s*ny1) + (1r-z)*((1r-s)*ny2) by CLVECT_1:def 2
.= (1r-z)*(s*ny1 + (1r-s)*ny2) by CLVECT_1:def 2;
then
A15: s*y1 + (1r-s)*y2 in (1r-z)*N by A12;
s*u + (1r-s)*v
= s*x1 + s*y1 + (1r-s)*(x2 + y2) by A6,A7,CLVECT_1:def 2
.= s*x1 + s*y1 + ((1r-s)*x2 + (1r-s)*y2) by CLVECT_1:def 2
.= s*x1 + s*y1 + (1r-s)*x2 + (1r-s)*y2 by RLVECT_1:def 6
.= s*x1 + (1r-s)*x2 + s*y1 + (1r-s)*y2 by RLVECT_1:def 6
.= (s*x1 + (1r-s)*x2) + (s*y1 + (1r-s)*y2) by RLVECT_1:def 6;
hence thesis by A14,A15;
end;
theorem Lm201:
for V being ComplexLinearSpace-like (non empty CLSStruct), M be Subset of V
holds 1r*M = M
proof
let V be ComplexLinearSpace-like (non empty CLSStruct);
let M be Subset of V;
for v being Element of V st v in 1r*M holds v in M
proof
let v be Element of V;
assume v in 1r*M;
then ex x be Element of V st v = 1r*x & x in M;
hence thesis by CLVECT_1:def 2;
end;
then A2:1r*M c= M by SUBSET_1:7;
for v being Element of V st v in M holds v in 1r*M
proof
let v be Element of V;
assume A3: v in M;
v = 1r*v by CLVECT_1:def 2;
hence thesis by A3;
end;
then M c= 1r*M by SUBSET_1:7;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Lm202:
for V being ComplexLinearSpace, M be non empty Subset of V holds
0c * M = {0.V}
proof
let V be ComplexLinearSpace;
let M be non empty Subset of V;
for v being Element of V st v in 0c * M holds v in {0.V}
proof
let v be Element of V;
assume v in 0c * M;
then ex x be Element of V st v = 0c * x & x in M;
then v = 0.V by CLVECT_1:2;
hence thesis by TARSKI:def 1;
end; then
A2: 0c * M c= {0.V} by SUBSET_1:7;
for v being Element of V st v in {0.V} holds v in 0c * M
proof
let v be Element of V;
assume v in {0.V};
then A3: v = 0.V by TARSKI:def 1;
consider x be set such that
A4: x in M by XBOOLE_0:def 1;
reconsider x as Element of V by A4;
v = 0c * x by A3,CLVECT_1:2;
hence thesis by A4;
end;
then {0.V} c= 0c * M by SUBSET_1:7;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
for V be add-associative (non empty addLoopStr), M1,M2,M3 be Subset of V holds
(M1 + M2) + M3 = M1 + (M2 + M3)
proof
let V be add-associative (non empty addLoopStr);
let M1,M2,M3 be Subset of V;
for x being Element of V st x in (M1 + M2) + M3
holds x in M1 + (M2 + M3)
proof
let x be Element of V;
assume x in (M1 + M2) + M3;
then consider x',x3 be Element of V such that
A1: x = x' + x3 & x' in M1 + M2 & x3 in M3;
consider x1,x2 be Element of V such that
A2: x' = x1 + x2 & x1 in M1 & x2 in M2 by A1;
A3: x = x1 + (x2 + x3) by A1,A2,RLVECT_1:def 6;
x2 + x3 in M2 + M3 by A1,A2;
hence thesis by A2,A3;
end;
then
A4:(M1 + M2) + M3 c= M1 + (M2 + M3) by SUBSET_1:7;
for x being Element of V st x in M1 + (M2 + M3)
holds x in (M1 + M2) + M3
proof
let x be Element of V;
assume x in M1 + (M2 + M3); then
consider x1,x' be Element of V such that
A5: x = x1 + x' & x1 in M1 & x' in M2+M3;
consider x2,x3 be Element of V such that
A6: x' = x2 + x3 & x2 in M2 & x3 in M3 by A5;
A7: x= (x1 + x2) + x3 by A5,A6,RLVECT_1:def 6;
x1 + x2 in M1 + M2 by A5,A6;
hence thesis by A6,A7;
end;
then M1 + (M2 + M3) c= (M1 + M2) + M3 by SUBSET_1:7;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem Lm204:
for V being ComplexLinearSpace-like (non empty CLSStruct),
M being Subset of V, z1,z2 being Complex holds
z1*(z2*M) = (z1*z2)*M
proof
let V be ComplexLinearSpace-like (non empty CLSStruct);
let M be Subset of V;
let z1,z2 be Complex;
for x being VECTOR of V st x in z1*(z2*M) holds x in (z1*z2)*M
proof
let x be VECTOR of V;
assume x in z1*(z2*M); then
consider w1 be VECTOR of V such that
A1: x = z1*w1 & w1 in z2*M;
consider w2 be VECTOR of V such that
A2: w1 = z2*w2 & w2 in M by A1;
x = (z1*z2)*w2 by A1,A2,CLVECT_1:def 2;
hence thesis by A2;
end;
then
A3: z1*(z2*M) c= (z1*z2)*M by SUBSET_1:7;
for x being VECTOR of V st x in (z1*z2)*M holds x in z1*(z2*M)
proof
let x be VECTOR of V;
assume x in (z1*z2)*M; then
consider w1 be VECTOR of V such that
A4: x = (z1*z2)*w1 & w1 in M;
A5: x = z1*(z2*w1) by A4,CLVECT_1:def 2;
z2*w1 in z2*M by A4;
hence thesis by A5;
end; then
(z1*z2)*M c= z1*(z2*M) by SUBSET_1:7;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Lm205:
for V being ComplexLinearSpace-like (non empty CLSStruct),
M1,M2 being Subset of V, z being Complex holds
z*(M1 + M2) = z*M1 + z*M2
proof
let V be ComplexLinearSpace-like (non empty CLSStruct);
let M1,M2 be Subset of V;
let z be Complex;
for x being VECTOR of V st x in z*(M1+M2) holds x in z*M1 + z*M2
proof
let x be VECTOR of V;
assume x in z*(M1+M2); then
consider w' be VECTOR of V such that
A1: x = z*w' & w' in M1 + M2;
consider w1,w2 be VECTOR of V such that
A2: w' = w1 + w2 & w1 in M1 & w2 in M2 by A1;
A3: x = z*w1 + z*w2 by A1,A2,CLVECT_1:def 2;
z*w1 in z*M1 & z*w2 in z*M2 by A2;
hence thesis by A3;
end; then
A5: z*(M1 + M2) c= z*M1 + z*M2 by SUBSET_1:7;
for x being VECTOR of V st x in z*M1 + z*M2 holds x in z*(M1+M2)
proof
let x be VECTOR of V;
assume x in z*M1 + z*M2; then
consider w1,w2 be VECTOR of V such that
A6: x = w1 + w2 & w1 in z*M1 & w2 in z*M2;
consider v1 be VECTOR of V such that
A7: w1 = z * v1 & v1 in M1 by A6;
consider v2 be VECTOR of V such that
A8: w2 = z * v2 & v2 in M2 by A6;
A9: x = z*(v1 + v2) by A6,A7,A8,CLVECT_1:def 2;
v1 + v2 in M1 + M2 by A7,A8;
hence thesis by A9;
end;
then z*M1 + z*M2 c= z*(M1+M2) by SUBSET_1:7;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem
for V being ComplexLinearSpace, M being Subset of V, v being VECTOR of V
holds M is convex iff v + M is convex
proof
let V be ComplexLinearSpace;
let M be Subset of V;
let v be VECTOR of V;
A1: M is convex implies v + M is convex
proof
assume A2: M is convex;
let w1,w2 be VECTOR of V;
let z be Complex;
assume that
A3: ex r being Real st z=r & 0 < r & r < 1 and
A4: w1 in v + M & w2 in v + M;
consider x1 be VECTOR of V such that
A5: w1 = v + x1 & x1 in M by A4;
consider x2 be VECTOR of V such that
A6: w2 = v + x2 & x2 in M by A4;
A7: z*x1 + (1r-z)*x2 in M by A2,A3,A5,A6,Def202;
z*w1 + (1r-z)*w2
= z*v + z*x1 + (1r-z)*(v+x2) by A5,A6,CLVECT_1:def 2
.= z*v + z*x1 + ((1r-z)*v + (1r-z)*x2) by CLVECT_1:def 2
.= z*v + z*x1 + (1r-z)*v + (1r-z)*x2 by RLVECT_1:def 6
.= z*v + (1r-z)*v + z*x1 + (1r-z)*x2 by RLVECT_1:def 6
.= (z+(1r-z))*v + z*x1 + (1r-z)*x2 by CLVECT_1:def 2
.= v + z*x1 + (1r-z)*x2 by CLVECT_1:def 2
.= v + (z*x1 + (1r-z)*x2) by RLVECT_1:def 6;
hence thesis by A7;
end;
v + M is convex implies M is convex
proof
assume A8: v + M is convex;
let w1,w2 be VECTOR of V;
let z be Complex;
assume that
A9: ex r being Real st z=r & 0 < r & r < 1 and
A10: w1 in M & w2 in M;
set x1 = v + w1, x2 = v + w2;
A11: x1 in v + M by A10;
x2 in {v + w where w is VECTOR of V : w in M} by A10; then
A12: z*x1 + (1r-z)*x2 in v + M by A8,A9,A11,Def202;
z*x1 + (1r-z)*x2
= z*v + z*w1 + (1r-z)*(v + w2) by CLVECT_1:def 2
.= z*v + z*w1 + ((1r-z)*v + (1r-z)*w2) by CLVECT_1:def 2
.= z*v + z*w1 + (1r-z)*v + (1r-z)*w2 by RLVECT_1:def 6
.= z*v + (1r-z)*v + z*w1 + (1r-z)*w2 by RLVECT_1:def 6
.= (z+(1r-z))*v + z*w1 + (1r-z)*w2 by CLVECT_1:def 2
.= v + z*w1 + (1r-z)*w2 by CLVECT_1:def 2
.= v + (z*w1 + (1r-z)*w2) by RLVECT_1:def 6; then
ex w be VECTOR of V st v + (z*w1 + (1r-z)*w2) = v + w & w in M by A12;
hence thesis by RLVECT_1:21;
end;
hence thesis by A1;
end;
theorem
for V being ComplexLinearSpace holds Up((0).V) is convex
proof
let V be ComplexLinearSpace;
let u,v be VECTOR of V;
let z be Complex;
assume that
ex r being Real st z=r & 0 < r & r < 1 and
A1: u in Up((0).V) & v in Up((0).V);
u in {0.V} by A1,CLVECT_1:def 6; then
A2: u = 0.V by TARSKI:def 1;
v in {0.V} by A1,CLVECT_1:def 6; then
v = 0.V by TARSKI:def 1; then
z * u + (1r-z) * v
= 0.V + (1r-z) * 0.V by A2,CLVECT_1:2
.= 0.V + 0.V by CLVECT_1:2
.= 0.V by RLVECT_1:10;
then
z * u + (1r-z) * v in {0.V} by TARSKI:def 1;
hence thesis by CLVECT_1:def 6;
end;
theorem
for V being ComplexLinearSpace holds Up((Omega).V) is convex
proof
let V be ComplexLinearSpace;
let u,v be VECTOR of V;
thus thesis;
end;
theorem Th210:
for V being non empty CLSStruct, M being Subset of V st M = {} holds
M is convex
proof
let V be non empty CLSStruct;
let M be Subset of V;
assume A1:M = {};
for u,v being VECTOR of V, z be Complex st
(ex r be Real st z=r & 0 < r & r < 1) & u in {} & v in {}
holds z*u + (1r-z)*v in {};
hence thesis by A1,Def202;
end;
theorem Th211:
for V being Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct), M1,M2 being Subset of V, z1,z2 being Complex st
M1 is convex & M2 is convex holds z1*M1 + z2*M2 is convex
proof
let V be Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct);
let M1,M2 be Subset of V;
let z1,z2 be Complex;
assume that
A1: M1 is convex & M2 is convex;
let u,v be VECTOR of V;
let s be Complex;
assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4:u in z1*M1 + z2*M2 & v in z1*M1 + z2*M2;
consider u1,u2 be VECTOR of V such that
A6: u = u1 + u2 & u1 in z1*M1 & u2 in z2*M2 by A4;
consider x1 be VECTOR of V such that
A7: u1 = z1*x1 & x1 in M1 by A6;
consider x2 be VECTOR of V such that
A8: u2 = z2*x2 & x2 in M2 by A6;
consider v1,v2 be VECTOR of V such that
A9: v = v1 + v2 & v1 in z1*M1 & v2 in z2*M2 by A4;
consider y1 be VECTOR of V such that
A10: v1 = z1*y1 & y1 in M1 by A9;
consider y2 be VECTOR of V such that
A11: v2 = z2*y2 & y2 in M2 by A9;
A12: s*x1 + (1r-s)*y1 in M1 & s*x2 + (1r-s)*y2 in M2
by A1,A3,A7,A8,A10,A11,Def202;
s*u1 + (1r-s)*v1
= z1*s*x1 + (1r-s)*(z1*y1) by A7,A10,CLVECT_1:def 2
.= z1*s*x1 + z1*(1r-s)*y1 by CLVECT_1:def 2
.= z1*(s*x1) + z1*(1r-s)*y1 by CLVECT_1:def 2
.= z1*(s*x1) + z1*((1r-s)*y1) by CLVECT_1:def 2
.= z1*(s*x1 + (1r-s)*y1) by CLVECT_1:def 2; then
A13: s*u1 + (1r-s)*v1 in z1*M1 by A12;
s*u2 + (1r-s)*v2
= z2*s*x2 + (1r-s)*(z2*y2) by A8,A11,CLVECT_1:def 2
.= z2*s*x2 + z2*(1r-s)*y2 by CLVECT_1:def 2
.= z2*(s*x2) + z2*(1r-s)*y2 by CLVECT_1:def 2
.= z2*(s*x2) + z2*((1r-s)*y2) by CLVECT_1:def 2
.= z2*(s*x2 + (1r-s)*y2) by CLVECT_1:def 2; then
A14: s*u2 + (1r-s)*v2 in z2*M2 by A12;
s*(u1+u2) + (1r-s)*(v1+v2)
= s*u1 + s*u2 + (1r-s)*(v1+v2) by CLVECT_1:def 2
.= s*u1 + s*u2 + ((1r-s)*v1 + (1r-s)*v2) by CLVECT_1:def 2
.= s*u1 + s*u2 + (1r-s)*v1 + (1r-s)*v2 by RLVECT_1:def 6
.= s*u1 + (1r-s)*v1 + s*u2 + (1r-s)*v2 by RLVECT_1:def 6
.= s*u1 + (1r-s)*v1 + (s*u2 + (1r-s)*v2) by RLVECT_1:def 6;
hence thesis by A6,A9,A13,A14;
end;
theorem Th212:
for V being ComplexLinearSpace-like (non empty CLSStruct),
M being Subset of V, z1,z2 being Complex holds
(z1 + z2)*M c= z1*M + z2*M
proof
let V be ComplexLinearSpace-like (non empty CLSStruct);
let M be Subset of V;
let z1,z2 be Complex;
for x being VECTOR of V st x in (z1+z2)*M holds x in z1*M + z2*M
proof
let x be VECTOR of V;
assume x in (z1+z2)*M; then
consider w be VECTOR of V such that
A1: x = (z1 + z2)*w & w in M;
A2: x = z1*w + z2*w by A1,CLVECT_1:def 2;
z1*w in z1*M & z2*w in z2*M by A1;
hence thesis by A2;
end;
hence thesis by SUBSET_1:7;
end;
theorem Lm206:
for V being non empty CLSStruct, M,N being Subset of V,
z being Complex st M c= N holds z*M c= z*N
proof
let V be non empty CLSStruct;
let M,N be Subset of V;
let z be Complex;
assume A1: M c= N;
now let x be VECTOR of V;
assume x in z*M;
then ex w be VECTOR of V st x = z*w & w in M;
hence x in z*N by A1;
end;
hence thesis by SUBSET_1:7;
end;
theorem Lm207:
for V being non empty CLSStruct, M being empty Subset of V,
z being Complex holds z * M = {}
proof
let V be non empty CLSStruct;
let M be empty Subset of V;
let z be Complex;
now let x be VECTOR of V;
assume x in z * M;
then ex v be VECTOR of V st x = z * v & v in {};
hence x in {};
end;
then z * M c= {} by SUBSET_1:7;
hence thesis by XBOOLE_1:3;
end;
theorem Lm208:
for V being non empty addLoopStr, M being empty Subset of V,
N being Subset of V holds M + N = {}
proof
let V be non empty addLoopStr;
let M be empty Subset of V;
let N be Subset of V;
now let x be Element of V;
assume x in M+N;
then ex u,v be Element of V st x = u + v & u in {} & v in N;
hence x in {};
end;
then M + N c= {} by SUBSET_1:7;
hence thesis by XBOOLE_1:3;
end;
theorem Lm209:
for V being right_zeroed (non empty addLoopStr), M being Subset of V holds
M + {0.V} = M
proof
let V be right_zeroed (non empty addLoopStr);
let M be Subset of V;
for x being Element of V st x in M + {0.V} holds x in M
proof
let x be Element of V;
assume x in M + {0.V}; then
consider u,v be Element of V such that
A1: x = u + v & u in M & v in {0.V};
v = 0.V by A1,TARSKI:def 1;
hence thesis by A1,RLVECT_1:def 7;
end; then
A2: M + {0.V} c= M by SUBSET_1:7;
for x being Element of V st x in M holds x in M + {0.V}
proof
let x be Element of V;
assume A3: x in M;
A4: x = x + 0.V by RLVECT_1:def 7;
0.V in {0.V} by TARSKI:def 1;
hence thesis by A3,A4;
end;
then M c= M + {0.V} by SUBSET_1:7;
hence thesis by A2,XBOOLE_0:def 10;
end;
Lm210:
for V being ComplexLinearSpace,
M being Subset of V, z1,z2 being Complex st
(ex r1,r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 ) & M is convex
holds
z1*M + z2*M c= (z1 + z2)*M
proof
let V be ComplexLinearSpace;
let M be Subset of V;
let z1,z2 be Complex;
assume that
A1: ex r1, r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 and
A2: M is convex;
consider r1, r2 being Real such that
B1: z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 by A1;
per cases;
suppose M is empty;
then z1*M = {} & z2*M = {} & (z1+z2)*M = {} by Lm207;
hence thesis by Lm208;
end;
suppose
A3: M is non empty;
per cases;
suppose A4: z1 = 0;
then z1*M = {0.V} by A3,Lm202;
hence thesis by A4,Lm209;
end;
suppose A5: z2 = 0;
then z2*M = {0.V} by A3,Lm202;
hence thesis by A5,Lm209;
end;
suppose A6: z1 <> 0 & z2 <> 0;
then A7: r1 + r2 > 0 + 0 & r1 + r2 > r1 & r1 + r2 > r2 by B1,XREAL_1:31;
then 0 < r1/(r1+r2) & r1/(r1+r2) < 1 &
0 < r2/(r1+r2) & r2/(r1+r2) < 1 by B1,A6,REAL_2:127,142; then
z1/(z1+z2) * M + (1r - z1/(z1+z2)) * M c= M by B1,A2,Th204; then
A10: (z1+z2)*(z1/(z1+z2)*M + (1r-z1/(z1+z2))*M) c= (z1+z2)*M by Lm206;
A11: (z1+z2)*(z1/(z1+z2)*M) = (z1/(z1+z2))*(z1+z2)*M by Lm204
.= z1*M by B1,A7,XCMPLX_1:88;
1-r1/(r1+r2) = (r1+r2)/(r1+r2) - r1/(r1+r2) by A7,XCMPLX_1:60; then
1-r1/(r1+r2) = (r1+r2-r1)/(r1+r2); then
(z1+z2)*((1r-z1/(z1+z2))*M) = z2/(z1+z2)*(z1+z2)*M by B1,Lm204
.= z2*M by B1,A7,XCMPLX_1:88;
hence thesis by A10,A11,Lm205;
end;
end;
end;
theorem
for V being ComplexLinearSpace, M being Subset of V, z1,z2 being Complex st
(ex r1,r2 being Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0) &
M is convex
holds
z1*M + z2*M = (z1 + z2)*M
proof
let V be ComplexLinearSpace,
M be Subset of V,
z1,z2 be Complex;
assume (ex r1,r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0)
& M is convex;
hence z1*M + z2*M c= (z1 + z2)*M by Lm210;
thus thesis by Th212;
end;
theorem
for V being Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct),
M1,M2,M3 being Subset of V, z1,z2,z3 being Complex st
M1 is convex & M2 is convex & M3 is convex holds
z1*M1 + z2*M2 + z3*M3 is convex
proof
let V be Abelian add-associative ComplexLinearSpace-like
(non empty CLSStruct);
let M1,M2,M3 be Subset of V;
let z1,z2,z3 be Complex;
assume that
A1: M1 is convex & M2 is convex & M3 is convex;
z1*M1 + z2*M2 is convex by A1,Th211;
then 1r*(z1*M1 + z2*M2) + z3*M3 is convex by A1,Th211;
hence thesis by Lm201;
end;
theorem Th215:
for V being non empty CLSStruct, F being Subset-Family of V st
(for M being Subset of V st M in F holds M is convex)
holds
meet F is convex
proof
let V be non empty CLSStruct;
let F be Subset-Family of V;
assume A1: for M being Subset of V st M in F holds M is convex;
per cases;
suppose F = {};
then meet F = {} by SETFAM_1:def 1;
hence meet F is convex by Th210;
end;
suppose A2: F <> {};
thus meet F is convex
proof
let u,v be VECTOR of V;
let z be Complex;
assume that
A3: ex r being Real st z=r & 0 < r & r < 1 and
A4: u in meet F & v in meet F;
for M being set st M in F holds z*u + (1r-z)*v in M
proof
let M be set;
assume A5: M in F;
then reconsider M as Subset of V;
A6: M is convex by A1,A5;
u in M & v in M by A4,A5,SETFAM_1:def 1;
hence thesis by A3,A6,Def202;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
end;
end;
theorem Th216:
for V being non empty CLSStruct, M being Subset of V st
M is Affine holds M is convex
proof
let V be non empty CLSStruct;
let M be Subset of V;
assume A1: M is Affine;
let u,v be VECTOR of V;
let z be Complex;
assume A2: (ex r being Real st z=r & 0 < r & r < 1) & u in M & v in M; then
consider r being Real such that
A3: z=r & 0 < r & r < 1;
set s = 1r-z;
1-r is Real & s=1-r by A3; then
(1r-s)*u+s*v in M by A1,A2,Def101;
hence thesis;
end;
registration
let V be non empty CLSStruct;
cluster non empty convex Subset of V;
existence
proof
consider M be non empty Affine Subset of V;
M is convex by Th216;
hence thesis;
end;
end;
registration
let V be non empty CLSStruct;
cluster empty convex Subset of V;
existence
proof
consider M being empty Subset of V;
M is convex by Th210;
hence thesis;
end;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Re(u .|. v) >= r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume A1: M = {u where u is VECTOR of V : Re(u.|.v) >= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3:x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) >= r by A1,A3; then
A8: p*Re(x.|.v) >= p*r by A4,XREAL_1:66;
A6:ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) >= r by A1,A3;
A7: Re( (s*x+(1r-s)*y).|.v )
= Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A4,Th101
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A4,Th101;
1-p > 0 by A4,XREAL_1:52;
then (1-p)*Re(y.|.v) >= (1-p)*r by A6,XREAL_1:66;
then p*Re(x.|.v) + (1-p)*Re(y.|.v ) >= p*r + (1-p)*r by A8,XREAL_1:9;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Re(u .|. v) > r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) > r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) > r by A1,A3; then
A8: p*Re(x.|.v) > p*r by A4,XREAL_1:70;
A6:ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) > r by A1,A3;
A7: Re( (s*x+(1r-s)*y).|.v )
= Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A4,Th101
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A4,Th101;
1-p > 0 by A4,XREAL_1:52;
then (1-p)*Re(y.|.v) > (1-p)*r by A6,XREAL_1:70;
then p*Re(x.|.v) + (1-p)*Re(y.|.v ) > p*r + (1-p)*r by A8,XREAL_1:10;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Re(u .|. v) <= r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) <= r by A1,A3; then
A8: p*Re(x.|.v) <= p*r by A4,XREAL_1:66;
A6: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) <= r by A1,A3;
A7: Re( (s*x+(1r-s)*y).|.v )
= Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A4, Th101
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A4,Th101;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Re(y.|.v) <= (1-p)*r by A6,XREAL_1:66; then
p*Re(x.|.v) + (1-p)*Re(y.|.v ) <= p*r + (1-p)*r by A8,XREAL_1:9;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Re(u .|. v) < r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) < r by A1,A3; then
A8: p*Re(x.|.v) < p*r by A4,XREAL_1:70;
A6: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) < r by A1,A3;
A7: Re( (s*x+(1r-s)*y).|.v )
= Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A4, Th101
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A4,Th101;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Re(y.|.v) < (1-p)*r by A6,XREAL_1:70; then
p*Re(x.|.v) + (1-p)*Re(y.|.v ) < p*r + (1-p)*r by A8,XREAL_1:10;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Im(u .|. v) >= r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) >= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) >= r by A1,A3; then
A8: p*Im(x.|.v) >= p*r by A4,XREAL_1:66;
A6: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) >= r by A1,A3;
A7: Im( (s*x+(1r-s)*y).|.v )
= Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A4,Th102
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A4,Th102;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Im(y.|.v) >= (1-p)*r by A6,XREAL_1:66; then
p*Im(x.|.v) + (1-p)*Im(y.|.v ) >= p*r + (1-p)*r by A8,XREAL_1:9;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Im(u .|. v) > r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) > r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3:x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) > r by A1,A3; then
A8: p*Im(x.|.v) > p*r by A4,XREAL_1:70;
A6: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) > r by A1,A3;
A7: Im( (s*x+(1r-s)*y).|.v )
= Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A4, Th102
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A4,Th102;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Im(y.|.v) > (1-p)*r by A6,XREAL_1:70; then
p*Im(x.|.v) + (1-p)*Im(y.|.v ) > p*r + (1-p)*r by A8,XREAL_1:10;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Im(u .|. v) <= r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) <= r by A1,A3; then
A8: p*Im(x.|.v) <= p*r by A4,XREAL_1:66;
A6: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) <= r by A1,A3;
A7: Im( (s*x+(1r-s)*y).|.v )
= Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A4,Th102
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A4,Th102;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Im(y.|.v) <= (1-p)*r by A6,XREAL_1:66; then
p*Im(x.|.v) + (1-p)*Im(y.|.v ) <= p*r + (1-p)*r by A8,XREAL_1:9;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : Im(u .|. v) < r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) < r by A1,A3; then
A8: p*Im(x.|.v) < p*r by A4,XREAL_1:70;
A6: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) < r by A1,A3;
A7: Im( (s*x+(1r-s)*y).|.v )
= Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:19
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A4,Th102
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A4,Th102;
1-p > 0 by A4,XREAL_1:52; then
(1-p)*Im(y.|.v) < (1-p)*r by A6,XREAL_1:70; then
p*Im(x.|.v) + (1-p)*Im(y.|.v ) < p*r + (1-p)*r by A8,XREAL_1:10;
hence thesis by A1,A7;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : |.u .|. v .| <= r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume A1: M = {u where u is VECTOR of V : |.u.|.v.| <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| <= r by A1,A3; then
A12: p*|.x.|.v.| <= p*r by A4,XREAL_1:66;
A6: ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| <= r by A1,A3;
A7: |.(s*x+(1r-s)*y).|.v.|
= |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
|.s*(x.|.v).| = p*|.x.|.v.| &
|.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A4,Th103; then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <=
p*|.x.|.v.| + (1-p)*|.y.|.v.| by COMPLEX1:142;
1-p > 0 by A4,XREAL_1:52;
then (1-p)*|.y.|.v.| <= (1-p)*r by A6,XREAL_1:66; then
p*|.x.|.v.|+(1-p)*|.y.|.v.| <= p*r + (1-p)*r by A12,XREAL_1:9; then
|.(s*x+(1r-s)*y).|.v.| <= r by A7,A11,XXREAL_0:2;
hence thesis by A1;
end;
theorem
for V being ComplexUnitarySpace-like (non empty CUNITSTR),
M being Subset of V, v being VECTOR of V, r being Real st
M = {u where u is VECTOR of V : |.u .|. v .| < r }
holds
M is convex
proof
let V be ComplexUnitarySpace-like (non empty CUNITSTR);
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume A1: M = {u where u is VECTOR of V : |.u.|.v.| < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: (ex p being Real st s=p & 0 < p & p < 1) and
A3: x in M & y in M;
consider p being Real such that
A4: s=p & 0 < p & p < 1 by A2;
ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| < r by A1,A3; then
A12: p*|.x.|.v.| < p*r by A4,XREAL_1:70;
A6: ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| < r by A1,A3;
A7: |.(s*x+(1r-s)*y).|.v.|
= |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
|.s*(x.|.v).| = p*|.x.|.v.| &
|.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A4,Th103; then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <= p*|.x.|.v.| + (1-p)*|.y.|.v.|
by COMPLEX1:142;
1-p > 0 by A4,XREAL_1:52;
then (1-p)*|.y.|.v.| < (1-p)*r by A6,XREAL_1:70; then
p*|.x.|.v.|+(1-p)*|.y.|.v.| < p*r + (1-p)*r by A12,XREAL_1:10;
then |.(s*x+(1r-s)*y).|.v.| < r by A7,A11,XXREAL_0:2;
hence thesis by A1;
end;
begin :: Complex Convex Combinations
definition
let V be ComplexLinearSpace, L be C_Linear_Combination of V;
attr
L is convex means :Def203:
ex F being FinSequence of the carrier of V st
F is one-to-one & rng F = Carrier L &
(ex f being FinSequence of REAL st len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0));
end;
theorem Th221:
for V being ComplexLinearSpace, L being C_Linear_Combination of V st
L is convex holds Carrier L <> {}
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
assume L is convex; then
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier L &
ex f being FinSequence of REAL st len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0)
by Def203;
assume Carrier L = {}; then
len F = 0 by A3,CARD_1:78,FINSEQ_4:77;
hence contradiction by A3,FINSEQ_1:32,RVSUM_1:102;
end;
theorem
for V being ComplexLinearSpace, L being C_Linear_Combination of V,
v being VECTOR of V st
L is convex & ( ex r being Real st r = L.v & r <= 0 )
holds
not v in Carrier L
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v be VECTOR of V;
assume that
A1: L is convex and
A2: ex r being Real st r = L.v & r <= 0;
consider r being Real such that
B1: r = L.v & r <= 0 by A2;
per cases by B1;
suppose r = 0;
hence not v in Carrier L by B1,Th1;
end;
suppose A3: r < 0;
now assume
A4: v in Carrier L;
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A5: rng F = Carrier L and
A6: ex f being FinSequence of REAL st
len f = len F & Sum(f) = 1 &
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
by A1,Def203;
consider f being FinSequence of REAL such that
A7: len f = len F and
Sum f = 1 and
A8: for n being Nat st n in dom f holds f.n =L.(F.n) & f.n >= 0 by A6;
consider n be set such that
A9: n in dom F & F.n = v by A4,A5,FUNCT_1:def 5;
reconsider n as Element of NAT by A9;
n in Seg len F by A9,FINSEQ_1:def 3;
then A10: n in dom f by A7,FINSEQ_1:def 3;
then L.v = f.n by A8,A9;
hence contradiction by A3,A8,A10,B1;
end;
hence not v in Carrier L;
end;
end;
theorem
for V being ComplexLinearSpace, L being C_Linear_Combination of V st
L is convex holds L <> ZeroCLC V
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
assume A1: L is convex;
assume A2: L = ZeroCLC V;
Carrier L <> {} by A1,Th221;
hence contradiction by A2,Def2;
end;
theorem Lm211:
for V being ComplexLinearSpace, v being VECTOR of V,
L being C_Linear_Combination of V st
L is convex & Carrier L = {v}
holds
( ex r being Real st r = L.v & r = 1 ) & Sum L = L.v * v
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v};
reconsider L as C_Linear_Combination of {v} by A2,Def3;
consider F being FinSequence of the carrier of V such that
A3:F is one-to-one & rng F = Carrier L &
ex f being FinSequence of REAL st len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0)
by A1,Def203;
consider f be FinSequence of REAL such that
A4:len f = len F & Sum f = 1 &
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A3;
card Carrier L = 1 by A2,CARD_1:79;
then len F = 1 by A3,FINSEQ_4:77;
then A5: dom f = Seg 1 by A4,FINSEQ_1:def 3;
then A6: 1 in dom f;
then A7: f.1 = L.(F.1) by A4;
A8: f.1 = f/.1 by A6,PARTFUN1:def 8;
reconsider r = f/.1 as Element of REAL;
f = <* r *> by A5,A8,FINSEQ_1:def 8;
then A9: Sum f = r by FINSOP_1:12;
F = <*v*> by A2,A3,FINSEQ_3:106;
then r = L.v by A7,A8,FINSEQ_1:def 8;
hence thesis by A4,A9,Th50;
end;
theorem Lm212:
for V being ComplexLinearSpace, v1,v2 being VECTOR of V,
L being C_Linear_Combination of V st
L is convex & Carrier L = {v1,v2} & v1 <> v2
holds
( ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 &
r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) &
Sum L = L.v1 * v1 + L.v2 * v2
proof
let V be ComplexLinearSpace;
let v1,v2 be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2;
reconsider L as C_Linear_Combination of {v1,v2} by A2,Def3;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L &
(ex f being FinSequence of REAL st len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0))
by A1,Def203;
consider f be FinSequence of REAL such that
A5: len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0) by A4;
len F = card {v1,v2} by A2,A4,FINSEQ_4:77; then
A6: len f = 2 by A3,A5,CARD_2:76; then
dom f = {1,2} by FINSEQ_1:4,def 3; then
A7: 1 in dom f & 2 in dom f by TARSKI:def 2; then
A8: f.1 = L.(F.1) & f.1 >= 0 by A5; then
f/.1 = L.(F.1) by A7,PARTFUN1:def 8; then
reconsider r1 = L.(F.1) as Real;
A9: f.2 = L.(F.2) & f.2 >= 0 by A5,A7; then
f/.2 = L.(F.2) by A7,PARTFUN1:def 8; then
reconsider r2 = L.(F.2) as Real;
A10: f = <*r1,r2*> by A6,A8,A9,FINSEQ_1:61;
ex c1,c2 being Real st c1=L.v1 & c2=L.v2 & c1+c2=1 & c1>=0 &c2>=0
proof
per cases by A2,A3,A4,FINSEQ_3:108;
suppose F = <*v1,v2*>;
then r1 = L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0
by A5,A8,A9,A10,RVSUM_1:107,FINSEQ_1:61;
hence thesis;
end;
suppose F = <*v2,v1*>;
then r1 = L.v2 & r2 = L.v1 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0
by A5,A8,A9,A10,RVSUM_1:107,FINSEQ_1:61;
hence thesis;
end;
end;
hence thesis by A3,Th51;
end;
Lm214:
for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V,
L being C_Linear_Combination of {v1,v2,v3} st
v1 <> v2 & v2 <> v3 & v3 <> v1
holds
Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2,v3};
assume that
A1: v1 <> v2 & v2 <> v3 & v3 <> v1;
A2: Carrier L c= {v1,v2,v3} by Def3;
per cases by A2,ZFMISC_1:142;
suppose Carrier L = {};
then A3: L = ZeroCLC V by Def2;
then Sum L = 0.V by Lm2
.= 0.V + 0.V by RLVECT_1:10
.= 0.V + 0.V + 0.V by RLVECT_1:10
.= 0c * v1 + 0.V + 0.V by CLVECT_1:2
.= 0c * v1 + 0c * v2 + 0.V by CLVECT_1:2
.= 0c * v1 + 0c * v2 + 0c * v3 by CLVECT_1:2
.= L.v1 * v1 + 0c * v2 + 0c * v3 by A3,Th30
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A3,Th30
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A3,Th30;
hence thesis;
end;
suppose A4: Carrier L = {v1};
then reconsider L as C_Linear_Combination of {v1} by Def3;
A5: not v2 in Carrier L & not v3 in Carrier L by A1,A4,TARSKI:def 1;
Sum L = L.v1 * v1 by Th50
.= L.v1 * v1 + 0.V by RLVECT_1:10
.= L.v1 * v1 + 0.V + 0.V by RLVECT_1:10
.= L.v1 * v1 + 0c * v2 + 0.V by CLVECT_1:2
.= L.v1 * v1 + 0c * v2 + 0c * v3 by CLVECT_1:2
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A5
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A5;
hence thesis;
end;
suppose A6: Carrier L = {v2};
then reconsider L as C_Linear_Combination of {v2} by Def3;
A7: not v1 in Carrier L & not v3 in Carrier L by A1,A6,TARSKI:def 1;
Sum L = L.v2 * v2 by Th50
.= 0.V + L.v2 * v2 by RLVECT_1:10
.= 0.V + L.v2 * v2 + 0.V by RLVECT_1:10
.= 0c * v1 + L.v2 * v2 + 0.V by CLVECT_1:2
.= 0c * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:2
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A7
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A7;
hence thesis;
end;
suppose A8: Carrier L = {v3};
then reconsider L as C_Linear_Combination of {v3} by Def3;
A9: not v1 in Carrier L & not v2 in Carrier L by A1,A8,TARSKI:def 1;
Sum L = L.v3 * v3 by Th50
.= 0.V + L.v3 * v3 by RLVECT_1:10
.= 0.V + 0.V + L.v3 * v3 by RLVECT_1:10
.= 0c * v1 + 0.V + L.v3 * v3 by CLVECT_1:2
.= 0c * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:2
.= L.v1 * v1 + 0c * v2 + L.v3 * v3 by A9
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A9;
hence thesis;
end;
suppose A10: Carrier L = {v1,v2};
then A11: not v3 in Carrier L by A1,TARSKI:def 2;
Sum L = L.v1 * v1 + L.v2 * v2 by A1,A10,Th54
.= L.v1 * v1 + L.v2 * v2 + 0.V by RLVECT_1:10
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:2;
hence thesis by A11;
end;
suppose A12: Carrier L = {v1,v3};
then A13: not v2 in Carrier L by A1,TARSKI:def 2;
Sum L = L.v1 * v1 + L.v3 * v3 by A1,A12,Th54
.= L.v1 * v1 + 0.V + L.v3 * v3 by RLVECT_1:10
.= L.v1 * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:2;
hence thesis by A13;
end;
suppose A14: Carrier L = {v2,v3};
then A15: not v1 in Carrier L by A1,TARSKI:def 2;
Sum L = L.v2 * v2 + L.v3 * v3 by A1,A14,Th54
.= 0.V + L.v2 * v2 + L.v3 * v3 by RLVECT_1:10
.= 0c * v1 + L.v2 * v2 + L.v3 * v3 by CLVECT_1:2;
hence thesis by A15;
end;
suppose Carrier L = {v1,v2,v3};
then consider F be FinSequence of the carrier of V such that
A16: F is one-to-one & rng F = {v1,v2,v3} and
A17: Sum L = Sum(L (#) F) by Def5;
F = <* v1,v2,v3 *> or F = <* v1,v3,v2 *> or F = <* v2,v1,v3 *> or
F = <* v2,v3,v1 *> or F = <* v3,v1,v2 *> or F = <* v3,v2,v1 *>
by A1,A16,CONVEX1:31;
then L (#) F = <* L.v1 * v1, L.v2 * v2, L.v3 * v3 *> or
L (#) F = <* L.v1 * v1, L.v3 * v3, L.v2 * v2 *> or
L (#) F = <* L.v2 * v2, L.v1 * v1, L.v3 * v3 *> or
L (#) F = <* L.v2 * v2, L.v3 * v3, L.v1 * v1 *> or
L (#) F = <* L.v3 * v3, L.v1 * v1, L.v2 * v2 *> or
L (#) F = <* L.v3 * v3, L.v2 * v2, L.v1 * v1 *> by Th44;
then Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3 or
Sum L = L.v1 * v1 + (L.v2 * v2 + L.v3 * v3) or
Sum L = L.v2 * v2 + (L.v1 * v1 + L.v3 * v3) by A17,RLVECT_1:63;
hence thesis by RLVECT_1:def 6;
end;
end;
theorem Lm215:
for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V,
L being C_Linear_Combination of V st
L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1
holds
( ex r1, r2, r3 being real number st
r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) &
Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v1,v2,v3} and
A3: v1 <> v2 & v2 <> v3 & v3 <> v1;
reconsider L as C_Linear_Combination of {v1,v2,v3} by A2,Def3;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L &
(ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0))
by A1,Def203;
consider f be FinSequence of REAL such that
A5: len f = len F & Sum f = 1 &
(for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0) by A4;
len F = card {v1,v2,v3} by A2,A4,FINSEQ_4:77;
then A6: len f = 3 by A3,A5,CARD_2:77;
then dom f = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then A7:1 in dom f & 2 in dom f & 3 in dom f by ENUMSET1:def 1;
then A8:f.1 = L.(F.1) & f.1 >= 0 by A5;
then f/.1 = L.(F.1) by A7,PARTFUN1:def 8;
then reconsider r1 = L.(F.1) as Element of REAL;
A9: f.2 = L.(F.2) & f.2 >= 0 by A5,A7;
then f/.2 = L.(F.2) by A7,PARTFUN1:def 8;
then reconsider r2 = L.(F.2) as Element of REAL;
A10: f.3 = L.(F.3) & f.3 >= 0 by A5,A7;
then f/.3 = L.(F.3) by A7,PARTFUN1:def 8;
then reconsider r3 = L.(F.3) as Element of REAL;
B1: f = <*r1,r2,r3*> by A6,A8,A9,A10,FINSEQ_1:62;
then A11: r1 + r2 + r3 = 1 by A5,RVSUM_1:108;
ex a, b, c being real number st a = L.v1 & b = L.v2 & c = L.v3 &
a + b + c = 1 & a >= 0 & b >= 0 & c >= 0
proof
per cases by A2,A3,A4,CONVEX1:31;
suppose F = <*v1,v2,v3*>;
then r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0
by B1,A5,RVSUM_1:108,A8,A9,A10,FINSEQ_1:62;
hence thesis;
end;
suppose F = <*v1,v3,v2*>;
then r1 = L.v1 & r3 = L.v2 & r2 = L.v3 &
r1 + r3 + r2 = 1 & r1 >= 0 & r3 >= 0 & r2 >= 0
by A8,A9,A10,A11,FINSEQ_1:62;
hence thesis;
end;
suppose F = <*v2,v1,v3*>;
then r2 = L.v1 & r1 = L.v2 & r3 = L.v3 &
r2 + r1 + r3 = 1 & r2 >= 0 & r1 >= 0 & r3 >= 0
by B1,A5,RVSUM_1:108,A8,A9,A10,FINSEQ_1:62;
hence thesis;
end;
suppose F = <*v2,v3,v1*>;
then r3 = L.v1 & r1 = L.v2 & r2 = L.v3 &
r3 + r1 + r2 = 1 & r3 >= 0 & r1 >= 0 & r2 >= 0
by A8,A9,A10,A11,FINSEQ_1:62;
hence thesis;
end;
suppose F = <*v3,v1,v2*>;
then r2 = L.v1 & r3 = L.v2 & r1 = L.v3 &
r2 + r3 + r1 = 1 & r2 >= 0 & r3 >= 0 & r1 >= 0
by A8,A9,A10,A11,FINSEQ_1:62;
hence thesis;
end;
suppose F = <*v3,v2,v1*>;
then r3 = L.v1 & r2 = L.v2 & r1 = L.v3 &
r3 + r2 + r1 = 1 & r3 >= 0 & r2 >= 0 & r1 >= 0
by A8,A9,A10,A11,FINSEQ_1:62;
hence thesis;
end;
end;
hence thesis by A3,Lm214;
end;
theorem
for V being ComplexLinearSpace, v being VECTOR of V,
L being C_Linear_Combination of {v} st
L is convex
holds
( ex r being Real st r = L.v & r = 1 ) & Sum L = L.v * v
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let L be C_Linear_Combination of {v};
assume A1: L is convex;
Carrier L c= {v} by Def3;
then Carrier L = {} or Carrier L = {v} by ZFMISC_1:39;
hence thesis by A1,Lm211,Th221;
end;
theorem
for V being ComplexLinearSpace, v1,v2 being VECTOR of V,
L being C_Linear_Combination of {v1,v2} st
v1 <> v2 & L is convex
holds
( ex r1, r2 being real number st r1 = L.v1 & r2 = L.v2 &r1 >= 0 & r2 >= 0 )&
Sum L = L.v1 * v1 + L.v2 * v2
proof
let V be ComplexLinearSpace;
let v1,v2 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2};
assume that
A1: v1 <> v2 and
A2: L is convex;
A3: Carrier L c= {v1,v2} by Def3;
A4: Carrier L <> {} by A2,Th221;
ex r1, r2 being real number st r1 = L.v1 & r2 = L.v2 & r1 >= 0 & r2 >= 0
proof
per cases by A3,A4,ZFMISC_1:42;
suppose A5: Carrier L = {v1};
then A6: ( ex r being Real st r = L.v1 & r = 1 ) &
Sum L = L.v1 * v1 by A2,Lm211;
not v2 in Carrier(L) by A1,A5,TARSKI:def 1;
then 1=L.v1 & 0 = L.v2 & 1 + 0 = 1 & 1 >= 0 & 0 >=0 by A6;
hence thesis;
end;
suppose A7: Carrier L = {v2};
then A8: ( ex r being Real st r =L.v2 & r = 1 ) &
Sum L = L.v2 * v2 by A2,Lm211;
not v1 in Carrier L by A1,A7,TARSKI:def 1;
then 0=L.v1 & 1 = L.v2 & 0 + 1 = 1 & 0 >= 0 & 1 >=0 by A8;
hence thesis;
end;
suppose Carrier L = {v1,v2};
then ex r1,r2 being Real st r1=L.v1 & r2 = L.v2 &
r1 + r2 = 1 & r1 >= 0 & r2 >=0 by A1,A2,Lm212;
hence thesis;
end;
end;
hence thesis by A1,Th51;
end;
theorem
for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V,
L being C_Linear_Combination of {v1,v2,v3} st
v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex
holds
( ex r1, r2, r3 being real number st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) &
Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2,v3};
assume that
A1: v1 <> v2 & v2 <> v3 & v3 <> v1 and
A2: L is convex;
A3: Carrier L c= {v1,v2,v3} by Def3;
A4: Carrier L <> {} by A2,Th221;
ex r1, r2, r3 being real number st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0
proof
per cases by A3,A4,ZFMISC_1:142;
suppose A5: Carrier L = {v1};
then A6: ex r being Real st r = L.v1 & r = 1 by A2,Lm211;
not v2 in Carrier L & not v3 in Carrier L by A1,A5,TARSKI:def 1;
then 1 = L.v1 & 0 = L.v2 & 0 = L.v3 & 1 + 0 + 0 =1 &
1 >= 0 & 0 >= 0 & 0 >= 0 by A6;
hence thesis;
end;
suppose A7: Carrier L = {v2};
then A8: ex r being Real st r = L.v2 & r = 1 by A2,Lm211;
not v1 in Carrier L & not v3 in Carrier L by A1,A7,TARSKI:def 1;
then 0 = L.v1 & 1 = L.v2 & 0 = L.v3 & 0 + 1 + 0 =1 &
0 >= 0 & 1 >= 0 & 0 >= 0 by A8;
hence thesis;
end;
suppose A9: Carrier L = {v3};
then A10: ex r being Real st r = L.v3 & r = 1 by A2,Lm211;
not v1 in Carrier L & not v2 in Carrier L by A1,A9,TARSKI:def 1;
then 0 = L.v1 & 0 = L.v2 & 1 = L.v3 & 0 + 0 + 1 =1 &
0 >= 0 & 0 >= 0 & 1 >= 0 by A10;
hence thesis;
end;
suppose A11: Carrier L = {v1,v2}; then
B1: not v3 in {v where v is Element of V : L.v <> 0} by A1,TARSKI:def 2;
set r3 = 0;
consider r1, r2 being Real such that
A13: r1 = L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0
by A1,A2,A11,Lm212;
r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 by B1,A13;
hence thesis;
end;
suppose A14: Carrier L = {v2,v3};
then B2: not v1 in Carrier L by A1,TARSKI:def 2;
set r1 = 0;
consider r2,r3 being Real such that
A16: r2 = L.v2 & r3 = L.v3 & r2 + r3 = 1 & r2 >= 0 & r3 >= 0
by A1,A2,A14,Lm212;
r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 by B2,A16;
hence thesis;
end;
suppose A17: Carrier L = {v1,v3};
then B3: not v2 in Carrier(L) by A1,TARSKI:def 2;
set r2 = 0;
consider r1, r3 being Real such that
A19: r1 = L.v1 & r3 = L.v3 & r1 + r3 = 1 & r1 >= 0 & r3 >= 0
by A1,A2,A17,Lm212;
r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 by B3,A19;
hence thesis;
end;
suppose Carrier L = {v1,v2,v3};
hence ex r1, r2, r3 be real number st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 by A1,A2,Lm215;
end;
end;
hence thesis by A1,Lm214;
end;
begin :: Complex Convex Hull
definition
let V be non empty CLSStruct, M be Subset of V;
func Convex-Family M -> Subset-Family of V means :Def204:
for N being Subset of V holds N in it iff (N is convex & M c= N);
existence
proof
defpred P[Subset of V] means $1 is convex & M c= $1;
thus ex F be Subset-Family of V st
for N being Subset of V holds N in F iff P[N] from SUBSET_1:sch 3;
end;
uniqueness
proof
let SF,SG be Subset-Family of V;
assume that
A1:for N being Subset of V holds N in SF iff N is convex & M c= N and
A2:for N being Subset of V holds N in SG iff N is convex & M c= N;
for Y being Subset of V holds Y in SF iff Y in SG
proof
let Y be Subset of V;
hereby assume Y in SF;
then Y is convex & M c= Y by A1;
hence Y in SG by A2;
end;
assume Y in SG;
then Y is convex & M c= Y by A2;
hence Y in SF by A1;
end;
hence SF = SG by SETFAM_1:44;
end;
end;
definition let V be non empty CLSStruct, M be Subset of V;
func conv M -> convex Subset of V equals
meet (Convex-Family M);
coherence
proof
for N being Subset of V st N in Convex-Family M holds N is convex by Def204;
hence thesis by Th215;
end;
end;
theorem
for V being non empty CLSStruct, M being Subset of V,
N being convex Subset of V st M c= N holds
conv M c= N
proof
let V be non empty CLSStruct;
let M be Subset of V;
let N be convex Subset of V;
assume M c= N;
then N in Convex-Family M by Def204;
hence thesis by SETFAM_1:4;
end;