:: 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;