:: CONVEX4 semantic presentation begin definition let V be non empty 1-sorted ; mode C_Linear_Combination of V -> Element of Funcs ( the carrier of V,COMPLEX) means :Def1: :: CONVEX4:def 1 ex T being finite Subset of V st for v being Element of V st not v in T holds it . v = 0 ; existence ex b1 being Element of Funcs ( the carrier of V,COMPLEX) ex T being finite Subset of V st for v being Element of V st not v in T holds b1 . v = 0 proof reconsider f = the carrier of V --> 0c as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; take f ; ::_thesis: ex T being finite Subset of V st for v being Element of V st not v in T holds f . v = 0 take {} V ; ::_thesis: for v being Element of V st not v in {} V holds f . v = 0 thus for v being Element of V st not v in {} V holds f . v = 0 by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem Def1 defines C_Linear_Combination CONVEX4:def_1_:_ for V being non empty 1-sorted for b2 being Element of Funcs ( the carrier of V,COMPLEX) holds ( b2 is C_Linear_Combination of V iff ex T being finite Subset of V st for v being Element of V st not v in T holds b2 . v = 0 ); notation let V be non empty addLoopStr ; let L be Element of Funcs ( the carrier of V,COMPLEX); synonym Carrier L for support V; end; Lm1: now__::_thesis:_for_V_being_non_empty_addLoopStr_ for_L_being_Element_of_Funcs_(_the_carrier_of_V,COMPLEX)_holds_Carrier_c=_the_carrier_of_V let V be non empty addLoopStr ; ::_thesis: for L being Element of Funcs ( the carrier of V,COMPLEX) holds Carrier c= the carrier of V let L be Element of Funcs ( the carrier of V,COMPLEX); ::_thesis: Carrier c= the carrier of V A1: support L c= dom L by PRE_POLY:37; thus Carrier c= the carrier of V ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in the carrier of V ) assume x in support L ; ::_thesis: x in the carrier of V then x in dom L by A1; hence x in the carrier of V ; ::_thesis: verum end; end; definition let V be non empty addLoopStr ; let L be Element of Funcs ( the carrier of V,COMPLEX); :: original: Carrier redefine func Carrier L -> Subset of V equals :: CONVEX4:def 2 { v where v is Element of V : L . v <> 0c } ; coherence Carrier is Subset of V by Lm1; compatibility for b1 being Subset of V holds ( b1 = Carrier iff b1 = { v where v is Element of V : L . v <> 0c } ) proof let X be Subset of V; ::_thesis: ( X = Carrier iff X = { v where v is Element of V : L . v <> 0c } ) set A = Carrier ; set B = { v where v is Element of V : L . v <> 0 } ; thus ( X = Carrier implies X = { v where v is Element of V : L . v <> 0 } ) ::_thesis: ( X = { v where v is Element of V : L . v <> 0c } implies X = Carrier ) proof assume A1: X = Carrier ; ::_thesis: X = { v where v is Element of V : L . v <> 0 } thus X c= { v where v is Element of V : L . v <> 0 } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Element of V : L . v <> 0 } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { v where v is Element of V : L . v <> 0 } ) assume A2: x in X ; ::_thesis: x in { v where v is Element of V : L . v <> 0 } then L . x <> 0 by A1, PRE_POLY:def_7; hence x in { v where v is Element of V : L . v <> 0 } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : L . v <> 0 } or x in X ) assume x in { v where v is Element of V : L . v <> 0 } ; ::_thesis: x in X then ex v being Element of V st ( x = v & L . v <> 0 ) ; hence x in X by A1, PRE_POLY:def_7; ::_thesis: verum end; assume A3: X = { v where v is Element of V : L . v <> 0 } ; ::_thesis: X = Carrier thus X c= Carrier :: according to XBOOLE_0:def_10 ::_thesis: Carrier c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Carrier ) assume x in X ; ::_thesis: x in Carrier then ex v being Element of V st ( x = v & L . v <> 0 ) by A3; hence x in Carrier by PRE_POLY:def_7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in X ) assume A4: x in Carrier ; ::_thesis: x in X then A5: L . x <> 0 by PRE_POLY:def_7; Carrier c= the carrier of V by Lm1; hence x in X by A3, A4, A5; ::_thesis: verum end; end; :: deftheorem defines Carrier CONVEX4:def_2_:_ for V being non empty addLoopStr for L being Element of Funcs ( the carrier of V,COMPLEX) holds Carrier L = { v where v is Element of V : L . v <> 0c } ; registration let V be non empty addLoopStr ; let L be C_Linear_Combination of V; cluster Carrier -> finite ; coherence Carrier L is finite 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__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_ x_in_T let x be set ; ::_thesis: ( x in Carrier L implies x in T ) assume x in Carrier L ; ::_thesis: x in T then ex v being Element of V st ( x = v & L . v <> 0c ) ; hence x in T by A1; ::_thesis: verum end; then Carrier L c= T by TARSKI:def_3; hence Carrier L is finite ; ::_thesis: verum end; end; theorem Th1: :: CONVEX4:1 for V being non empty addLoopStr for L being C_Linear_Combination of V for v being Element of V holds ( L . v = 0c iff not v in Carrier L ) proof let V be non empty addLoopStr ; ::_thesis: for L being C_Linear_Combination of V for v being Element of V holds ( L . v = 0c iff not v in Carrier L ) let L be C_Linear_Combination of V; ::_thesis: for v being Element of V holds ( L . v = 0c iff not v in Carrier L ) let v be Element of V; ::_thesis: ( L . v = 0c iff not v in Carrier L ) thus ( L . v = 0c implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0c ) proof assume A1: L . v = 0c ; ::_thesis: not v in Carrier L assume v in Carrier L ; ::_thesis: contradiction then ex u being Element of V st ( v = u & L . u <> 0c ) ; hence contradiction by A1; ::_thesis: verum end; thus ( not v in Carrier L implies L . v = 0c ) ; ::_thesis: verum end; definition let V be non empty addLoopStr ; func ZeroCLC V -> C_Linear_Combination of V means :Def3: :: CONVEX4:def 3 Carrier it = {} ; existence ex b1 being C_Linear_Combination of V st Carrier b1 = {} proof reconsider f = the carrier of V --> 0c as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; f is C_Linear_Combination of V proof take {} V ; :: according to CONVEX4:def_1 ::_thesis: for v being Element of V st not v in {} V holds f . v = 0 thus for v being Element of V st not v in {} V holds f . v = 0 by FUNCOP_1:7; ::_thesis: verum end; then reconsider f = f as C_Linear_Combination of V ; take f ; ::_thesis: Carrier f = {} set C = { v where v is Element of V : f . v <> 0c } ; now__::_thesis:_not__{__v_where_v_is_Element_of_V_:_f_._v_<>_0c__}__<>_{} set x = the Element of { v where v is Element of V : f . v <> 0c } ; assume { v where v is Element of V : f . v <> 0c } <> {} ; ::_thesis: contradiction then the Element of { v where v is Element of V : f . v <> 0c } in { v where v is Element of V : f . v <> 0c } ; then ex v being Element of V st ( the Element of { v where v is Element of V : f . v <> 0c } = v & f . v <> 0c ) ; hence contradiction by FUNCOP_1:7; ::_thesis: verum end; hence Carrier f = {} ; ::_thesis: verum end; uniqueness for b1, b2 being C_Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds b1 = b2 proof let L, L9 be C_Linear_Combination of V; ::_thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 ) assume A1: ( Carrier L = {} & Carrier L9 = {} ) ; ::_thesis: L = L9 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ L_._x_=_L9_._x let x be set ; ::_thesis: ( x in the carrier of V implies L . x = L9 . x ) assume x in the carrier of V ; ::_thesis: L . x = L9 . x then reconsider v = x as Element of V ; A2: ( L9 . v <> 0c implies v in { u where u is Element of V : L9 . u <> 0c } ) ; ( L . v <> 0c implies v in { u where u is Element of V : L . u <> 0c } ) ; hence L . x = L9 . x by A1, A2; ::_thesis: verum end; hence L = L9 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines ZeroCLC CONVEX4:def_3_:_ for V being non empty addLoopStr for b2 being C_Linear_Combination of V holds ( b2 = ZeroCLC V iff Carrier b2 = {} ); registration let V be non empty addLoopStr ; cluster Carrier -> empty ; coherence Carrier (ZeroCLC V) is empty by Def3; end; theorem Th2: :: CONVEX4:2 for V being non empty addLoopStr for v being Element of V holds (ZeroCLC V) . v = 0c proof let V be non empty addLoopStr ; ::_thesis: for v being Element of V holds (ZeroCLC V) . v = 0c let v be Element of V; ::_thesis: (ZeroCLC V) . v = 0c ( Carrier (ZeroCLC V) = {} & not v in {} ) ; hence (ZeroCLC V) . v = 0c ; ::_thesis: verum 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 :Def4: :: CONVEX4:def 4 Carrier it c= A; existence ex b1 being C_Linear_Combination of V st Carrier b1 c= A proof take L = ZeroCLC V; ::_thesis: Carrier L c= A Carrier L = {} ; hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines C_Linear_Combination CONVEX4:def_4_:_ for V being non empty addLoopStr for A being Subset of V for b3 being C_Linear_Combination of V holds ( b3 is C_Linear_Combination of A iff Carrier b3 c= A ); theorem :: CONVEX4:3 for V being non empty addLoopStr for A, B being Subset of V for l being C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B proof let V be non empty addLoopStr ; ::_thesis: for A, B being Subset of V for l being C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B let A, B be Subset of V; ::_thesis: for l being C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B let l be C_Linear_Combination of A; ::_thesis: ( A c= B implies l is C_Linear_Combination of B ) assume A1: A c= B ; ::_thesis: l is C_Linear_Combination of B Carrier l c= A by Def4; then Carrier l c= B by A1, XBOOLE_1:1; hence l is C_Linear_Combination of B by Def4; ::_thesis: verum end; theorem Th4: :: CONVEX4:4 for V being non empty addLoopStr for A being Subset of V holds ZeroCLC V is C_Linear_Combination of A proof let V be non empty addLoopStr ; ::_thesis: for A being Subset of V holds ZeroCLC V is C_Linear_Combination of A let A be Subset of V; ::_thesis: ZeroCLC V is C_Linear_Combination of A ( Carrier (ZeroCLC V) = {} & {} c= A ) by XBOOLE_1:2; hence ZeroCLC V is C_Linear_Combination of A by Def4; ::_thesis: verum end; theorem Th5: :: CONVEX4:5 for V being non empty addLoopStr for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V proof let V be non empty addLoopStr ; ::_thesis: for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V let l be C_Linear_Combination of {} the carrier of V; ::_thesis: l = ZeroCLC V Carrier l c= {} by Def4; then Carrier l = {} ; hence l = ZeroCLC V by Def3; ::_thesis: verum end; 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; funcf (#) F -> FinSequence of the carrier of V means :Def5: :: CONVEX4:def 5 ( len it = len F & ( for i being Nat st i in dom it holds it . i = (f . (F /. i)) * (F /. i) ) ); existence ex b1 being FinSequence of the carrier of V st ( len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) ) proof deffunc H1( set ) -> Element of the carrier of V = (f . (F /. $1)) * (F /. $1); consider G being FinSequence such that A1: len G = len F and A2: for n being Nat st n in dom G holds G . n = H1(n) from FINSEQ_1:sch_2(); rng G c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of V ) assume x in rng G ; ::_thesis: x in the carrier of V then consider y being set such that A3: y in dom G and A4: G . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A3; G . y = (f . (F /. y)) * (F /. y) by A2, A3; hence x in the carrier of V by A4; ::_thesis: verum end; then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def_4; take G ; ::_thesis: ( len G = len F & ( for i being Nat st i in dom G holds G . i = (f . (F /. i)) * (F /. i) ) ) thus ( len G = len F & ( for i being Nat st i in dom G holds G . i = (f . (F /. i)) * (F /. i) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of the carrier of V st len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds b2 . i = (f . (F /. i)) * (F /. i) ) holds b1 = b2 proof let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being Nat st i in dom H2 holds H2 . i = (f . (F /. i)) * (F /. i) ) implies H1 = H2 ) assume that A5: len H1 = len F and A6: for i being Nat st i in dom H1 holds H1 . i = (f . (F /. i)) * (F /. i) and A7: len H2 = len F and A8: for i being Nat st i in dom H2 holds H2 . i = (f . (F /. i)) * (F /. i) ; ::_thesis: H1 = H2 now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_H1_holds_ H1_._k_=_H2_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k ) assume ( 1 <= k & k <= len H1 ) ; ::_thesis: H1 . k = H2 . k then A9: k in Seg (len H1) by FINSEQ_1:1; then k in dom H1 by FINSEQ_1:def_3; then A10: H1 . k = (f . (F /. k)) * (F /. k) by A6; k in dom H2 by A5, A7, A9, FINSEQ_1:def_3; hence H1 . k = H2 . k by A8, A10; ::_thesis: verum end; hence H1 = H2 by A5, A7, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def5 defines (#) CONVEX4:def_5_:_ for V being non empty CLSStruct for F being FinSequence of the carrier of V for f being Function of the carrier of V,COMPLEX for b4 being FinSequence of the carrier of V holds ( b4 = f (#) F iff ( len b4 = len F & ( for i being Nat st i in dom b4 holds b4 . i = (f . (F /. i)) * (F /. i) ) ) ); theorem Th6: :: CONVEX4:6 for V being non empty CLSStruct for v being VECTOR of V for x being set for F being FinSequence of the carrier of V for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds (f (#) F) . x = (f . v) * v proof let V be non empty CLSStruct ; ::_thesis: for v being VECTOR of V for x being set for F being FinSequence of the carrier of V for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds (f (#) F) . x = (f . v) * v let v be VECTOR of V; ::_thesis: for x being set for F being FinSequence of the carrier of V for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds (f (#) F) . x = (f . v) * v let x be set ; ::_thesis: for F being FinSequence of the carrier of V for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds (f (#) F) . x = (f . v) * v let F be FinSequence of the carrier of V; ::_thesis: for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds (f (#) F) . x = (f . v) * v let f be Function of the carrier of V,COMPLEX; ::_thesis: ( x in dom F & v = F . x implies (f (#) F) . x = (f . v) * v ) assume that A1: x in dom F and A2: v = F . x ; ::_thesis: (f (#) F) . x = (f . v) * v A3: F /. x = F . x by A1, PARTFUN1:def_6; len (f (#) F) = len F by Def5; then x in dom (f (#) F) by A1, FINSEQ_3:29; hence (f (#) F) . x = (f . v) * v by A2, A3, Def5; ::_thesis: verum end; theorem :: CONVEX4:7 for V being non empty CLSStruct for f being Function of the carrier of V,COMPLEX holds f (#) (<*> the carrier of V) = <*> the carrier of V proof let V be non empty CLSStruct ; ::_thesis: for f being Function of the carrier of V,COMPLEX holds f (#) (<*> the carrier of V) = <*> the carrier of V let f be Function of the carrier of V,COMPLEX; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def5 .= 0 ; hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum end; theorem Th8: :: CONVEX4:8 for V being non empty CLSStruct for v being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*> proof let V be non empty CLSStruct ; ::_thesis: for v being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*> let v be VECTOR of V; ::_thesis: for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*> let f be Function of the carrier of V,COMPLEX; ::_thesis: f (#) <*v*> = <*((f . v) * v)*> A1: 1 in {1} by FINSEQ_1:2; A2: len (f (#) <*v*>) = len <*v*> by Def5 .= 1 by FINSEQ_1:40 ; then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3; then (f (#) <*v*>) . 1 = (f . (<*v*> /. 1)) * (<*v*> /. 1) by A1, Def5 .= (f . (<*v*> /. 1)) * v by FINSEQ_4:16 .= (f . v) * v by FINSEQ_4:16 ; hence f (#) <*v*> = <*((f . v) * v)*> by A2, FINSEQ_1:40; ::_thesis: verum end; theorem Th9: :: CONVEX4:9 for V being non empty CLSStruct for v1, v2 being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> proof let V be non empty CLSStruct ; ::_thesis: for v1, v2 being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let v1, v2 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let f be Function of the carrier of V,COMPLEX; ::_thesis: f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def5 .= 2 by FINSEQ_1:44 ; then A2: dom (f (#) <*v1,v2*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; 2 in {1,2} by FINSEQ_1:2; then A3: (f (#) <*v1,v2*>) . 2 = (f . (<*v1,v2*> /. 2)) * (<*v1,v2*> /. 2) by A2, Def5 .= (f . (<*v1,v2*> /. 2)) * v2 by FINSEQ_4:17 .= (f . v2) * v2 by FINSEQ_4:17 ; 1 in {1,2} by FINSEQ_1:2; then (f (#) <*v1,v2*>) . 1 = (f . (<*v1,v2*> /. 1)) * (<*v1,v2*> /. 1) by A2, Def5 .= (f . (<*v1,v2*> /. 1)) * v1 by FINSEQ_4:17 .= (f . v1) * v1 by FINSEQ_4:17 ; hence f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> by A1, A3, FINSEQ_1:44; ::_thesis: verum end; theorem Th10: :: CONVEX4:10 for V being non empty CLSStruct for v1, v2, v3 being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> proof let V be non empty CLSStruct ; ::_thesis: for v1, v2, v3 being VECTOR of V for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let v1, v2, v3 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let f be Function of the carrier of V,COMPLEX; ::_thesis: f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def5 .= 3 by FINSEQ_1:45 ; then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1; 3 in {1,2,3} by FINSEQ_3:1; then A3: (f (#) <*v1,v2,v3*>) . 3 = (f . (<*v1,v2,v3*> /. 3)) * (<*v1,v2,v3*> /. 3) by A2, Def5 .= (f . (<*v1,v2,v3*> /. 3)) * v3 by FINSEQ_4:18 .= (f . v3) * v3 by FINSEQ_4:18 ; 2 in {1,2,3} by FINSEQ_3:1; then A4: (f (#) <*v1,v2,v3*>) . 2 = (f . (<*v1,v2,v3*> /. 2)) * (<*v1,v2,v3*> /. 2) by A2, Def5 .= (f . (<*v1,v2,v3*> /. 2)) * v2 by FINSEQ_4:18 .= (f . v2) * v2 by FINSEQ_4:18 ; 1 in {1,2,3} by FINSEQ_3:1; then (f (#) <*v1,v2,v3*>) . 1 = (f . (<*v1,v2,v3*> /. 1)) * (<*v1,v2,v3*> /. 1) by A2, Def5 .= (f . (<*v1,v2,v3*> /. 1)) * v1 by FINSEQ_4:18 .= (f . v1) * v1 by FINSEQ_4:18 ; hence f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum end; definition let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; let L be C_Linear_Combination of V; func Sum L -> Element of V means :Def6: :: CONVEX4:def 6 ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) ); existence ex b1 being Element of V ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) proof consider F being FinSequence such that A1: rng F = Carrier L and A2: F is one-to-one by FINSEQ_4:58; reconsider F = F as FinSequence of the carrier of V by A1, FINSEQ_1:def_4; take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) take F ; ::_thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) thus ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & b2 = Sum (L (#) F) ) holds b1 = b2 proof let v1, v2 be Element of V; ::_thesis: ( ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 ) given F1 being FinSequence of the carrier of V such that A3: F1 is one-to-one and A4: rng F1 = Carrier L and A5: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of the carrier of V holds ( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 ) given F2 being FinSequence of the carrier of V such that A6: F2 is one-to-one and A7: rng F2 = Carrier L and A8: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2 defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)}; A9: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48; A10: dom F1 = Seg (len F1) by FINSEQ_1:def_3; A11: dom F2 = Seg (len F2) by FINSEQ_1:def_3; A12: for x being set st x in dom F1 holds ex y being set st ( y in dom F1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in dom F1 implies ex y being set st ( y in dom F1 & S1[x,y] ) ) assume x in dom F1 ; ::_thesis: ex y being set st ( y in dom F1 & S1[x,y] ) then F2 . x in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def_3; then consider y being set such that A13: F1 " {(F2 . x)} = {y} by A3, FUNCT_1:74; take y ; ::_thesis: ( y in dom F1 & S1[x,y] ) y in F1 " {(F2 . x)} by A13, TARSKI:def_1; hence ( y in dom F1 & S1[x,y] ) by A13, FUNCT_1:def_7; ::_thesis: verum end; consider f being Function of (dom F1),(dom F1) such that A14: for x being set st x in dom F1 holds S1[x,f . x] from FUNCT_2:sch_1(A12); A15: rng f = dom F1 proof thus rng f c= dom F1 by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: dom F1 c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom F1 or y in rng f ) assume A16: y in dom F1 ; ::_thesis: y in rng f then F1 . y in rng F2 by A4, A7, FUNCT_1:def_3; then consider x being set such that A17: x in dom F2 and A18: F2 . x = F1 . y by FUNCT_1:def_3; F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A16, A18, FUNCT_1:59; then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82; then {(f . x)} c= {y} by A9, A10, A11, A14, A17; then A19: f . x = y by ZFMISC_1:18; x in dom f by A9, A10, A11, A17, FUNCT_2:def_1; hence y in rng f by A19, FUNCT_1:def_3; ::_thesis: verum end; set G1 = L (#) F1; A20: len (L (#) F1) = len F1 by Def5; A21: f is one-to-one proof let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 ) let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 ) assume that A22: y1 in dom f and A23: y2 in dom f and A24: f . y1 = f . y2 ; ::_thesis: y1 = y2 F2 . y1 in rng F1 by A4, A7, A9, A10, A11, A22, FUNCT_1:def_3; then A25: {(F2 . y1)} c= rng F1 by ZFMISC_1:31; F2 . y2 in rng F1 by A4, A7, A9, A10, A11, A23, FUNCT_1:def_3; then A26: {(F2 . y2)} c= rng F1 by ZFMISC_1:31; ( F1 " {(F2 . y1)} = {(f . y1)} & F1 " {(F2 . y2)} = {(f . y2)} ) by A14, A22, A23; then {(F2 . y1)} = {(F2 . y2)} by A24, A25, A26, FUNCT_1:91; then F2 . y1 = F2 . y2 by ZFMISC_1:3; hence y1 = y2 by A6, A9, A10, A11, A22, A23, FUNCT_1:def_4; ::_thesis: verum end; set G2 = L (#) F2; A27: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3; reconsider f = f as Permutation of (dom F1) by A15, A21, FUNCT_2:57; ( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def_3; then reconsider f = f as Permutation of (dom (L (#) F1)) by A20; A28: len (L (#) F2) = len F2 by Def5; A29: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(L_(#)_F2)_holds_ (L_(#)_F2)_._i_=_(L_(#)_F1)_._(f_._i) let i be Element of NAT ; ::_thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) ) assume A30: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i) then A31: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A28, A11, A27, Def5, PARTFUN1:def_6; i in dom f by A9, A28, A10, A27, A30, FUNCT_2:def_1; then A32: f . i in dom F1 by A15, FUNCT_1:def_3; then reconsider m = f . i as Element of NAT ; {(F1 . (f . i))} = Im (F1,(f . i)) by A32, FUNCT_1:59 .= F1 .: (F1 " {(F2 . i)}) by A9, A28, A10, A27, A14, A30 ; then A33: F2 . i = F1 . m by FUNCT_1:75, ZFMISC_1:18; F1 . m = F1 /. m by A32, PARTFUN1:def_6; hence (L (#) F2) . i = (L (#) F1) . (f . i) by A20, A10, A29, A32, A33, A31, Def5; ::_thesis: verum end; hence v1 = v2 by A3, A4, A5, A6, A7, A8, A20, A28, FINSEQ_1:48, RLVECT_2:6; ::_thesis: verum end; end; :: deftheorem Def6 defines Sum CONVEX4:def_6_:_ for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct for L being C_Linear_Combination of V for b3 being Element of V holds ( b3 = Sum L iff ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & b3 = Sum (L (#) F) ) ); theorem Th11: :: CONVEX4:11 for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct holds Sum (ZeroCLC V) = 0. V proof let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; ::_thesis: Sum (ZeroCLC V) = 0. V consider F being FinSequence of the carrier of V such that F is one-to-one and A1: rng F = Carrier (ZeroCLC V) and A2: Sum (ZeroCLC V) = Sum ((ZeroCLC V) (#) F) by Def6; F = {} by A1, RELAT_1:41; then len ((ZeroCLC V) (#) F) = 0 by Def5, CARD_1:27; hence Sum (ZeroCLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum end; theorem :: CONVEX4:12 for V being ComplexLinearSpace for A being Subset of V st A <> {} holds ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) proof let V be ComplexLinearSpace; ::_thesis: for A being Subset of V st A <> {} holds ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) let A be Subset of V; ::_thesis: ( A <> {} implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) ) assume A1: A <> {} ; ::_thesis: ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) thus ( A is linearly-closed implies for l being C_Linear_Combination of A holds Sum l in A ) ::_thesis: ( ( for l being C_Linear_Combination of A holds Sum l in A ) implies A is linearly-closed ) proof defpred S1[ Nat] means for l being C_Linear_Combination of A st card (Carrier l) = $1 holds Sum l in A; assume A2: A is linearly-closed ; ::_thesis: for l being C_Linear_Combination of A holds Sum l in A A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] hereby ::_thesis: verum let l be C_Linear_Combination of A; ::_thesis: ( card (Carrier l) = k + 1 implies Sum l in A ) deffunc H1( Element of V) -> Element of COMPLEX = l . $1; consider F being FinSequence of the carrier of V such that A5: F is one-to-one and A6: rng F = Carrier l and A7: Sum l = Sum (l (#) F) by Def6; reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18; assume A8: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A then A9: len F = k + 1 by A5, A6, FINSEQ_4:62; then A10: len (l (#) F) = k + 1 by Def5; k + 1 in Seg (k + 1) by FINSEQ_1:4; then A11: k + 1 in dom F by A9, FINSEQ_1:def_3; then reconsider v = F . (k + 1) as VECTOR of V by FUNCT_1:102; consider f being Function of the carrier of V,COMPLEX such that A12: ( f . v = 0c & ( for u being Element of V st u <> v holds f . u = H1(u) ) ) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_Carrier_l_holds_ f_._u_=_0c let u be VECTOR of V; ::_thesis: ( not u in Carrier l implies f . u = 0c ) assume not u in Carrier l ; ::_thesis: f . u = 0c then l . u = 0c ; hence f . u = 0c by A12; ::_thesis: verum end; then reconsider f = f as C_Linear_Combination of V by Def1; A13: Carrier f = (Carrier l) \ {v} proof now__::_thesis:_for_x_being_set_st_x_in_Carrier_f_holds_ x_in_(Carrier_l)_\_{v} let x be set ; ::_thesis: ( x in Carrier f implies x in (Carrier l) \ {v} ) assume x in Carrier f ; ::_thesis: x in (Carrier l) \ {v} then A14: ex u being VECTOR of V st ( u = x & f . u <> 0c ) ; then f . x = l . x by A12; then A15: x in Carrier l by A14; not x in {v} by A12, A14, TARSKI:def_1; hence x in (Carrier l) \ {v} by A15, XBOOLE_0:def_5; ::_thesis: verum end; hence Carrier f c= (Carrier l) \ {v} by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \ {v} c= Carrier f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ {v} or x in Carrier f ) assume A16: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f then not x in {v} by XBOOLE_0:def_5; then x <> v by TARSKI:def_1; then A17: l . x = f . x by A12, A16; x in Carrier l by A16, XBOOLE_0:def_5; then ex u being VECTOR of V st ( x = u & l . u <> 0c ) ; hence x in Carrier f by A17; ::_thesis: verum end; A18: Carrier l c= A by Def4; then Carrier f c= A \ {v} by A13, XBOOLE_1:33; then Carrier f c= A by XBOOLE_1:106; then reconsider f = f as C_Linear_Combination of A by Def4; A19: len G = k by A9, FINSEQ_3:53; then A20: len (f (#) G) = k by Def5; A21: rng G = Carrier f proof thus rng G c= Carrier f :: according to XBOOLE_0:def_10 ::_thesis: Carrier f c= rng G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in Carrier f ) assume x in rng G ; ::_thesis: x in Carrier f then consider y being set such that A22: y in dom G and A23: G . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A22; A24: ( dom G c= dom F & G . y = F . y ) by A22, FUNCT_1:47, RELAT_1:60; then ( x = v implies ( k + 1 = y & y <= k & k < k + 1 ) ) by A5, A19, A11, A22, A23, FINSEQ_3:25, FUNCT_1:def_4, XREAL_1:29; then A25: not x in {v} by TARSKI:def_1; x in rng F by A22, A23, A24, FUNCT_1:def_3; hence x in Carrier f by A6, A13, A25, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in rng G ) assume A26: x in Carrier f ; ::_thesis: x in rng G then x in rng F by A6, A13, XBOOLE_0:def_5; then consider y being set such that A27: y in dom F and A28: F . y = x by FUNCT_1:def_3; now__::_thesis:_y_in_Seg_k assume not y in Seg k ; ::_thesis: contradiction then y in (dom F) \ (Seg k) by A27, XBOOLE_0:def_5; then y in (Seg (k + 1)) \ (Seg k) by A9, FINSEQ_1:def_3; then y in {(k + 1)} by FINSEQ_3:15; then y = k + 1 by TARSKI:def_1; then not v in {v} by A13, A26, A28, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then y in (dom F) /\ (Seg k) by A27, XBOOLE_0:def_4; then A29: y in dom G by RELAT_1:61; then G . y = F . y by FUNCT_1:47; hence x in rng G by A28, A29, FUNCT_1:def_3; ::_thesis: verum end; (Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12 .= dom (f (#) G) by A20, FINSEQ_1:def_3 ; then A30: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A10, FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(f_(#)_G)_holds_ (f_(#)_G)_._x_=_(l_(#)_F)_._x let x be set ; ::_thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x ) assume A31: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x then A32: x in dom G by A19, A20, FINSEQ_3:29; then A33: G . x in rng G by FUNCT_1:def_3; then reconsider u = G . x as VECTOR of V ; A34: F . x = u by A32, FUNCT_1:47; not u in {v} by A13, A21, A33, XBOOLE_0:def_5; then A35: u <> v by TARSKI:def_1; x in dom (l (#) F) by A30, A31, XBOOLE_0:def_4; then A36: x in dom F by A9, A10, FINSEQ_3:29; (f (#) G) . x = (f . u) * u by A32, Th6 .= (l . u) * u by A12, A35 ; hence (f (#) G) . x = (l (#) F) . x by A36, A34, Th6; ::_thesis: verum end; then A37: f (#) G = (l (#) F) | (Seg k) by A30, FUNCT_1:46; v in rng F by A11, FUNCT_1:def_3; then {v} c= Carrier l by A6, ZFMISC_1:31; then card (Carrier f) = (k + 1) - (card {v}) by A8, A13, CARD_2:44; then card (Carrier f) = (k + 1) - 1 by CARD_1:30; then A38: Sum f in A by A4; v in Carrier l by A6, A11, FUNCT_1:def_3; then A39: (l . v) * v in A by A2, A18, CLVECT_1:def_7; G is one-to-one by A5, FUNCT_1:52; then A40: Sum (f (#) G) = Sum f by A21, Def6; ( dom (f (#) G) = Seg (len (f (#) G)) & (l (#) F) . (len F) = (l . v) * v ) by A9, A11, Th6, FINSEQ_1:def_3; then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A9, A10, A20, A37, RLVECT_1:38; hence Sum l in A by A2, A7, A39, A40, A38, CLVECT_1:def_7; ::_thesis: verum end; end; let l be C_Linear_Combination of A; ::_thesis: Sum l in A A41: card (Carrier l) = card (Carrier l) ; now__::_thesis:_for_l_being_C_Linear_Combination_of_A_st_card_(Carrier_l)_=_0_holds_ Sum_l_in_A let l be C_Linear_Combination of A; ::_thesis: ( card (Carrier l) = 0 implies Sum l in A ) assume card (Carrier l) = 0 ; ::_thesis: Sum l in A then Carrier l = {} ; then l = ZeroCLC V by Def3; then Sum l = 0. V by Th11; hence Sum l in A by A1, A2, CLVECT_1:20; ::_thesis: verum end; then A42: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A42, A3); hence Sum l in A by A41; ::_thesis: verum end; assume A43: for l being C_Linear_Combination of A holds Sum l in A ; ::_thesis: A is linearly-closed ( ZeroCLC V is C_Linear_Combination of A & Sum (ZeroCLC V) = 0. V ) by Th4, Th11; then A44: 0. V in A by A43; A45: for a being Complex for v being VECTOR of V st v in A holds a * v in A proof let a be Complex; ::_thesis: for v being VECTOR of V st v in A holds a * v in A let v be VECTOR of V; ::_thesis: ( v in A implies a * v in A ) assume A46: v in A ; ::_thesis: a * v in A now__::_thesis:_(_a_<>_0_implies_a_*_v_in_A_) reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2; deffunc H1( Element of V) -> Element of COMPLEX = 0c ; consider f being Function of the carrier of V,COMPLEX such that A47: ( f . v = a1 & ( for u being Element of V st u <> v holds f . u = H1(u) ) ) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v} implies f . u = 0 ) assume not u in {v} ; ::_thesis: f . u = 0 then u <> v by TARSKI:def_1; hence f . u = 0 by A47; ::_thesis: verum end; then reconsider f = f as C_Linear_Combination of V by Def1; assume A48: a <> 0 ; ::_thesis: a * v in A A49: Carrier f = {v} proof now__::_thesis:_for_x_being_set_st_x_in_Carrier_f_holds_ x_in_{v} let x be set ; ::_thesis: ( x in Carrier f implies x in {v} ) assume x in Carrier f ; ::_thesis: x in {v} then ex u being VECTOR of V st ( x = u & f . u <> 0 ) ; then x = v by A47; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; hence Carrier f c= {v} by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: {v} c= Carrier f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in Carrier f ) assume x in {v} ; ::_thesis: x in Carrier f then x = v by TARSKI:def_1; hence x in Carrier f by A48, A47; ::_thesis: verum end; {v} c= A by A46, ZFMISC_1:31; then reconsider f = f as C_Linear_Combination of A by A49, Def4; consider F being FinSequence of the carrier of V such that A50: ( F is one-to-one & rng F = Carrier f ) and A51: Sum (f (#) F) = Sum f by Def6; F = <*v*> by A49, A50, FINSEQ_3:97; then f (#) F = <*((f . v) * v)*> by Th8; then Sum f = a * v by A47, A51, RLVECT_1:44; hence a * v in A by A43; ::_thesis: verum end; hence a * v in A by A44, CLVECT_1:1; ::_thesis: verum 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; ::_thesis: ( v in A & u in A implies v + u in A ) assume that A52: v in A and A53: u in A ; ::_thesis: v + u in A A54: 1r * v = v by CLVECT_1:def_5; A55: 1r * u = u by CLVECT_1:def_5; A56: now__::_thesis:_(_v_<>_u_implies_v_+_u_in_A_) deffunc H1( Element of V) -> Element of COMPLEX = 0c ; assume A57: v <> u ; ::_thesis: v + u in A consider f being Function of the carrier of V,COMPLEX such that A58: ( f . v = 1r & f . u = 1r ) and A59: for w being Element of V st w <> v & w <> u holds f . w = H1(w) from FUNCT_2:sch_7(A57); reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; now__::_thesis:_for_w_being_VECTOR_of_V_st_not_w_in_{v,u}_holds_ f_._w_=_0 let w be VECTOR of V; ::_thesis: ( not w in {v,u} implies f . w = 0 ) assume not w in {v,u} ; ::_thesis: f . w = 0 then ( w <> v & w <> u ) by TARSKI:def_2; hence f . w = 0 by A59; ::_thesis: verum end; then reconsider f = f as C_Linear_Combination of V by Def1; A60: Carrier f = {v,u} proof thus Carrier f c= {v,u} :: according to XBOOLE_0:def_10 ::_thesis: {v,u} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,u} ) assume x in Carrier f ; ::_thesis: x in {v,u} then ex w being VECTOR of V st ( x = w & f . w <> 0c ) ; then ( x = v or x = u ) by A59; hence x in {v,u} by TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v,u} or x in Carrier f ) assume x in {v,u} ; ::_thesis: x in Carrier f then ( x = v or x = u ) by TARSKI:def_2; hence x in Carrier f by A58; ::_thesis: verum end; then Carrier f c= A by A52, A53, ZFMISC_1:32; then reconsider f = f as C_Linear_Combination of A by Def4; consider F being FinSequence of the carrier of V such that A61: ( F is one-to-one & rng F = Carrier f ) and A62: Sum (f (#) F) = Sum f by Def6; ( F = <*v,u*> or F = <*u,v*> ) by A57, A60, A61, FINSEQ_3:99; then ( f (#) F = <*(1r * v),(1r * u)*> or f (#) F = <*(1r * u),(1r * v)*> ) by A58, Th9; then Sum f = v + u by A55, A54, A62, RLVECT_1:45; hence v + u in A by A43; ::_thesis: verum end; v + v = (1r + 1r) * v by A54, CLVECT_1:def_3; hence v + u in A by A45, A52, A56; ::_thesis: verum end; hence A is linearly-closed by A45, CLVECT_1:def_7; ::_thesis: verum end; theorem :: CONVEX4:13 for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct for l being C_Linear_Combination of {} the carrier of V holds Sum l = 0. V proof let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; ::_thesis: for l being C_Linear_Combination of {} the carrier of V holds Sum l = 0. V let l be C_Linear_Combination of {} the carrier of V; ::_thesis: Sum l = 0. V l = ZeroCLC V by Th5; hence Sum l = 0. V by Th11; ::_thesis: verum end; theorem Th14: :: CONVEX4:14 for V being ComplexLinearSpace for v being VECTOR of V for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v proof let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v let v be VECTOR of V; ::_thesis: for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v let l be C_Linear_Combination of {v}; ::_thesis: Sum l = (l . v) * v A1: Carrier l c= {v} by Def4; percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33; suppose Carrier l = {} ; ::_thesis: Sum l = (l . v) * v then A2: l = ZeroCLC V by Def3; hence Sum l = 0. V by Th11 .= 0c * v by CLVECT_1:1 .= (l . v) * v by A2, Th2 ; ::_thesis: verum end; suppose Carrier l = {v} ; ::_thesis: Sum l = (l . v) * v then consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = {v} ) and A4: Sum l = Sum (l (#) F) by Def6; F = <*v*> by A3, FINSEQ_3:97; then l (#) F = <*((l . v) * v)*> by Th8; hence Sum l = (l . v) * v by A4, RLVECT_1:44; ::_thesis: verum end; end; end; theorem Th15: :: CONVEX4:15 for V being ComplexLinearSpace for v1, v2 being VECTOR of V st v1 <> v2 holds for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) proof let V be ComplexLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) ) assume A1: v1 <> v2 ; ::_thesis: for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) let l be C_Linear_Combination of {v1,v2}; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) A2: 0. V = 0c * v1 by CLVECT_1:1; A3: Carrier l c= {v1,v2} by Def4; A4: 0. V = 0c * v2 by CLVECT_1:1; percases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A3, ZFMISC_1:36; suppose Carrier l = {} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then A5: l = ZeroCLC V by Def3; hence Sum l = 0. V by Th11 .= (0. V) + (0. V) by RLVECT_1:4 .= ((l . v1) * v1) + (0c * v2) by A4, A5, Th2, CLVECT_1:1 .= ((l . v1) * v1) + ((l . v2) * v2) by A5, Th2 ; ::_thesis: verum end; supposeA6: Carrier l = {v1} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then reconsider L = l as C_Linear_Combination of {v1} by Def4; Sum L = (l . v1) * v1 by Th14; then A7: Sum l = ((l . v1) * v1) + (0. V) by RLVECT_1:4; not v2 in Carrier l by A1, A6, TARSKI:def_1; hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A4, A7; ::_thesis: verum end; supposeA8: Carrier l = {v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then reconsider L = l as C_Linear_Combination of {v2} by Def4; Sum L = (l . v2) * v2 by Th14; then A9: Sum l = (0. V) + ((l . v2) * v2) by RLVECT_1:4; not v1 in Carrier l by A1, A8, TARSKI:def_1; hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A2, A9; ::_thesis: verum end; suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then consider F being FinSequence of the carrier of V such that A10: ( F is one-to-one & rng F = {v1,v2} ) and A11: Sum l = Sum (l (#) F) by Def6; ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A10, FINSEQ_3:99; then ( l (#) F = <*((l . v1) * v1),((l . v2) * v2)*> or l (#) F = <*((l . v2) * v2),((l . v1) * v1)*> ) by Th9; hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A11, RLVECT_1:45; ::_thesis: verum end; end; end; theorem :: CONVEX4:16 for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct for L being C_Linear_Combination of V st Carrier L = {} holds Sum L = 0. V proof let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; ::_thesis: for L being C_Linear_Combination of V st Carrier L = {} holds Sum L = 0. V let L be C_Linear_Combination of V; ::_thesis: ( Carrier L = {} implies Sum L = 0. V ) assume Carrier L = {} ; ::_thesis: Sum L = 0. V then L = ZeroCLC V by Def3; hence Sum L = 0. V by Th11; ::_thesis: verum end; theorem :: CONVEX4:17 for V being ComplexLinearSpace for L being C_Linear_Combination of V for v being VECTOR of V st Carrier L = {v} holds Sum L = (L . v) * v proof let V be ComplexLinearSpace; ::_thesis: for L being C_Linear_Combination of V for v being VECTOR of V st Carrier L = {v} holds Sum L = (L . v) * v let L be C_Linear_Combination of V; ::_thesis: for v being VECTOR of V st Carrier L = {v} holds Sum L = (L . v) * v let v be VECTOR of V; ::_thesis: ( Carrier L = {v} implies Sum L = (L . v) * v ) assume Carrier L = {v} ; ::_thesis: Sum L = (L . v) * v then L is C_Linear_Combination of {v} by Def4; hence Sum L = (L . v) * v by Th14; ::_thesis: verum end; theorem Th18: :: CONVEX4:18 for V being ComplexLinearSpace for L being C_Linear_Combination of V for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) proof let V be ComplexLinearSpace; ::_thesis: for L being C_Linear_Combination of V for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) let L be C_Linear_Combination of V; ::_thesis: for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) let v1, v2 be VECTOR of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) assume that A1: Carrier L = {v1,v2} and A2: v1 <> v2 ; ::_thesis: Sum L = ((L . v1) * v1) + ((L . v2) * v2) L is C_Linear_Combination of {v1,v2} by A1, Def4; hence Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A2, Th15; ::_thesis: verum end; definition let V be non empty addLoopStr ; let L1, L2 be C_Linear_Combination of V; :: original: = redefine predL1 = L2 means :: CONVEX4:def 7 for v being Element of V holds L1 . v = L2 . v; compatibility ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63; end; :: deftheorem defines = CONVEX4:def_7_:_ for V being non empty addLoopStr for L1, L2 being C_Linear_Combination of V holds ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ); definition let V be non empty addLoopStr ; let L1, L2 be C_Linear_Combination of V; :: original: + redefine funcL1 + L2 -> C_Linear_Combination of V means :Def8: :: CONVEX4:def 8 for v being Element of V holds it . v = (L1 . v) + (L2 . v); coherence L1 + L2 is C_Linear_Combination of V proof reconsider f = L1 + L2 as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_ f_._v_=_0 let v be Element of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0 ) assume A1: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: f . v = 0 then not v in Carrier L2 by XBOOLE_0:def_3; then A2: L2 . v = 0 ; not v in Carrier L1 by A1, XBOOLE_0:def_3; then L1 . v = 0 ; hence f . v = 0 + 0 by A2, VALUED_1:1 .= 0 ; ::_thesis: verum end; hence L1 + L2 is C_Linear_Combination of V by Def1; ::_thesis: verum end; compatibility for b1 being C_Linear_Combination of V holds ( b1 = L1 + L2 iff for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) ) proof let f be C_Linear_Combination of V; ::_thesis: ( f = L1 + L2 iff for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) thus ( f = L1 + L2 implies for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) by VALUED_1:1; ::_thesis: ( ( for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) implies f = L1 + L2 ) assume for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; ::_thesis: f = L1 + L2 then A3: for c being set st c in dom f holds f . c = (L1 . c) + (L2 . c) ; ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:92; then dom f = (dom L1) /\ (dom L2) by FUNCT_2:92; hence f = L1 + L2 by A3, VALUED_1:def_1; ::_thesis: verum end; end; :: deftheorem Def8 defines + CONVEX4:def_8_:_ for V being non empty addLoopStr for L1, L2, b4 being C_Linear_Combination of V holds ( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) ); theorem Th19: :: CONVEX4:19 for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) proof let V be non empty CLSStruct ; ::_thesis: for L1, L2 being C_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be C_Linear_Combination of V; ::_thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) ) assume x in Carrier (L1 + L2) ; ::_thesis: x in (Carrier L1) \/ (Carrier L2) then consider u being VECTOR of V such that A1: x = u and A2: (L1 + L2) . u <> 0c ; (L1 + L2) . u = (L1 . u) + (L2 . u) by Def8; then ( L1 . u <> 0c or L2 . u <> 0c ) by A2; then ( x in Carrier L1 or x in Carrier L2 ) by A1; hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th20: :: CONVEX4:20 for V being non empty CLSStruct for A being Subset of V for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 + L2 is C_Linear_Combination of A proof let V be non empty CLSStruct ; ::_thesis: for A being Subset of V for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 + L2 is C_Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 + L2 is C_Linear_Combination of A let L1, L2 be C_Linear_Combination of V; ::_thesis: ( L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies L1 + L2 is C_Linear_Combination of A ) assume ( L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A ) ; ::_thesis: L1 + L2 is C_Linear_Combination of A then ( Carrier L1 c= A & Carrier L2 c= A ) by Def4; then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8; Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th19; hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to CONVEX4:def_4 ::_thesis: verum end; definition let V be non empty CLSStruct ; let A be Subset of V; let L1, L2 be C_Linear_Combination of A; :: original: + redefine funcL1 + L2 -> C_Linear_Combination of A; coherence L1 + L2 is C_Linear_Combination of A by Th20; end; theorem :: CONVEX4:21 for V being non empty addLoopStr for L1, L2 being C_Linear_Combination of V holds L1 + L2 = L2 + L1 ; theorem Th22: :: CONVEX4:22 for V being non empty CLSStruct for L1, L2, L3 being C_Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 proof let V be non empty CLSStruct ; ::_thesis: for L1, L2, L3 being C_Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 let L1, L2, L3 be C_Linear_Combination of V; ::_thesis: L1 + (L2 + L3) = (L1 + L2) + L3 let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Def8 .= (L1 . v) + ((L2 . v) + (L3 . v)) by Def8 .= ((L1 . v) + (L2 . v)) + (L3 . v) .= ((L1 + L2) . v) + (L3 . v) by Def8 .= ((L1 + L2) + L3) . v by Def8 ; ::_thesis: verum end; theorem Th23: :: CONVEX4:23 for V being non empty CLSStruct for L being C_Linear_Combination of V holds L + (ZeroCLC V) = L proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds L + (ZeroCLC V) = L let L be C_Linear_Combination of V; ::_thesis: L + (ZeroCLC V) = L let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (L + (ZeroCLC V)) . v = L . v thus (L + (ZeroCLC V)) . v = (L . v) + ((ZeroCLC V) . v) by Def8 .= (L . v) + 0c by Th2 .= L . v ; ::_thesis: verum end; definition let V be non empty CLSStruct ; let a be Complex; let L be C_Linear_Combination of V; funca * L -> C_Linear_Combination of V means :Def9: :: CONVEX4:def 9 for v being VECTOR of V holds it . v = a * (L . v); existence ex b1 being C_Linear_Combination of V st for v being VECTOR of V holds b1 . v = a * (L . v) proof reconsider a = a as Element of COMPLEX by XCMPLX_0:def_2; deffunc H1( Element of V) -> Element of COMPLEX = 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 = H1(v) from FUNCT_2:sch_4(); reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8; now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_Carrier_L_holds_ f_._v_=_0c let v be VECTOR of V; ::_thesis: ( not v in Carrier L implies f . v = 0c ) assume not v in Carrier L ; ::_thesis: f . v = 0c then L . v = 0c ; hence f . v = a * 0c by A1 .= 0c ; ::_thesis: verum end; then reconsider f = f as C_Linear_Combination of V by Def1; take f ; ::_thesis: for v being VECTOR of V holds f . v = a * (L . v) let v be VECTOR of V; ::_thesis: f . v = a * (L . v) thus f . v = a * (L . v) by A1; ::_thesis: verum end; uniqueness for b1, b2 being C_Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = a * (L . v) ) & ( for v being VECTOR of V holds b2 . v = a * (L . v) ) holds b1 = b2 proof let L1, L2 be C_Linear_Combination of V; ::_thesis: ( ( for v being VECTOR of V holds L1 . v = a * (L . v) ) & ( for v being VECTOR of V holds L2 . v = a * (L . v) ) implies L1 = L2 ) assume A2: for v being VECTOR of V holds L1 . v = a * (L . v) ; ::_thesis: ( ex v being VECTOR of V st not L2 . v = a * (L . v) or L1 = L2 ) assume A3: for v being VECTOR of V holds L2 . v = a * (L . v) ; ::_thesis: L1 = L2 let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: L1 . v = L2 . v thus L1 . v = a * (L . v) by A2 .= L2 . v by A3 ; ::_thesis: verum end; end; :: deftheorem Def9 defines * CONVEX4:def_9_:_ for V being non empty CLSStruct for a being Complex for L, b4 being C_Linear_Combination of V holds ( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) ); theorem Th24: :: CONVEX4:24 for V being non empty CLSStruct for a being Complex for L being C_Linear_Combination of V st a <> 0c holds Carrier (a * L) = Carrier L proof let V be non empty CLSStruct ; ::_thesis: for a being Complex for L being C_Linear_Combination of V st a <> 0c holds Carrier (a * L) = Carrier L let a be Complex; ::_thesis: for L being C_Linear_Combination of V st a <> 0c holds Carrier (a * L) = Carrier L let L be C_Linear_Combination of V; ::_thesis: ( a <> 0c implies Carrier (a * L) = Carrier L ) set T = { u where u is VECTOR of V : (a * L) . u <> 0c } ; set S = { v where v is VECTOR of V : L . v <> 0c } ; assume A1: a <> 0c ; ::_thesis: Carrier (a * L) = Carrier L { u where u is VECTOR of V : (a * L) . u <> 0c } = { v where v is VECTOR of V : L . v <> 0c } proof thus { u where u is VECTOR of V : (a * L) . u <> 0c } c= { v where v is VECTOR of V : L . v <> 0c } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is VECTOR of V : L . v <> 0c } c= { u where u is VECTOR of V : (a * L) . u <> 0c } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is VECTOR of V : (a * L) . u <> 0c } or x in { v where v is VECTOR of V : L . v <> 0c } ) assume x in { u where u is VECTOR of V : (a * L) . u <> 0c } ; ::_thesis: x in { v where v is VECTOR of V : L . v <> 0c } then consider u being VECTOR of V such that A2: x = u and A3: (a * L) . u <> 0c ; (a * L) . u = a * (L . u) by Def9; then L . u <> 0c by A3; hence x in { v where v is VECTOR of V : L . v <> 0c } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is VECTOR of V : L . v <> 0c } or x in { u where u is VECTOR of V : (a * L) . u <> 0c } ) assume x in { v where v is VECTOR of V : L . v <> 0c } ; ::_thesis: x in { u where u is VECTOR of V : (a * L) . u <> 0c } then consider v being VECTOR of V such that A4: ( x = v & L . v <> 0c ) ; (a * L) . v = a * (L . v) by Def9; hence x in { u where u is VECTOR of V : (a * L) . u <> 0c } by A1, A4; ::_thesis: verum end; hence Carrier (a * L) = Carrier L ; ::_thesis: verum end; theorem Th25: :: CONVEX4:25 for V being non empty CLSStruct for L being C_Linear_Combination of V holds 0c * L = ZeroCLC V proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds 0c * L = ZeroCLC V let L be C_Linear_Combination of V; ::_thesis: 0c * L = ZeroCLC V let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (0c * L) . v = (ZeroCLC V) . v thus (0c * L) . v = 0c * (L . v) by Def9 .= (ZeroCLC V) . v by Th2 ; ::_thesis: verum end; theorem Th26: :: CONVEX4:26 for V being non empty CLSStruct for A being Subset of V for a being Complex for L being C_Linear_Combination of V st L is C_Linear_Combination of A holds a * L is C_Linear_Combination of A proof let V be non empty CLSStruct ; ::_thesis: for A being Subset of V for a being Complex for L being C_Linear_Combination of V st L is C_Linear_Combination of A holds a * L is C_Linear_Combination of A let A be Subset of V; ::_thesis: for a being Complex for L being C_Linear_Combination of V st L is C_Linear_Combination of A holds a * L is C_Linear_Combination of A let a be Complex; ::_thesis: for L being C_Linear_Combination of V st L is C_Linear_Combination of A holds a * L is C_Linear_Combination of A let L be C_Linear_Combination of V; ::_thesis: ( L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A ) assume A1: L is C_Linear_Combination of A ; ::_thesis: a * L is C_Linear_Combination of A A2: now__::_thesis:_(_a_<>_0c_implies_a_*_L_is_C_Linear_Combination_of_A_) assume a <> 0c ; ::_thesis: a * L is C_Linear_Combination of A then Carrier (a * L) = Carrier L by Th24; hence a * L is C_Linear_Combination of A by A1, Def4; ::_thesis: verum end; ( a = 0c implies a * L = ZeroCLC V ) by Th25; hence a * L is C_Linear_Combination of A by A2, Th4; ::_thesis: verum end; theorem Th27: :: CONVEX4:27 for V being non empty CLSStruct for a, b being Complex for L being C_Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) proof let V be non empty CLSStruct ; ::_thesis: for a, b being Complex for L being C_Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let a, b be Complex; ::_thesis: for L being C_Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let L be C_Linear_Combination of V; ::_thesis: (a + b) * L = (a * L) + (b * L) let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: ((a + b) * L) . v = ((a * L) + (b * L)) . v thus ((a + b) * L) . v = (a + b) * (L . v) by Def9 .= (a * (L . v)) + (b * (L . v)) .= ((a * L) . v) + (b * (L . v)) by Def9 .= ((a * L) . v) + ((b * L) . v) by Def9 .= ((a * L) + (b * L)) . v by Def8 ; ::_thesis: verum end; theorem Th28: :: CONVEX4:28 for V being non empty CLSStruct for a being Complex for L1, L2 being C_Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) proof let V be non empty CLSStruct ; ::_thesis: for a being Complex for L1, L2 being C_Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let a be Complex; ::_thesis: for L1, L2 being C_Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let L1, L2 be C_Linear_Combination of V; ::_thesis: a * (L1 + L2) = (a * L1) + (a * L2) let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (a * (L1 + L2)) . v = ((a * L1) + (a * L2)) . v thus (a * (L1 + L2)) . v = a * ((L1 + L2) . v) by Def9 .= a * ((L1 . v) + (L2 . v)) by Def8 .= (a * (L1 . v)) + (a * (L2 . v)) .= ((a * L1) . v) + (a * (L2 . v)) by Def9 .= ((a * L1) . v) + ((a * L2) . v) by Def9 .= ((a * L1) + (a * L2)) . v by Def8 ; ::_thesis: verum end; theorem Th29: :: CONVEX4:29 for V being non empty CLSStruct for a, b being Complex for L being C_Linear_Combination of V holds a * (b * L) = (a * b) * L proof let V be non empty CLSStruct ; ::_thesis: for a, b being Complex for L being C_Linear_Combination of V holds a * (b * L) = (a * b) * L let a, b be Complex; ::_thesis: for L being C_Linear_Combination of V holds a * (b * L) = (a * b) * L let L be C_Linear_Combination of V; ::_thesis: a * (b * L) = (a * b) * L let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (a * (b * L)) . v = ((a * b) * L) . v thus (a * (b * L)) . v = a * ((b * L) . v) by Def9 .= a * (b * (L . v)) by Def9 .= (a * b) * (L . v) .= ((a * b) * L) . v by Def9 ; ::_thesis: verum end; theorem Th30: :: CONVEX4:30 for V being non empty CLSStruct for L being C_Linear_Combination of V holds 1r * L = L proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds 1r * L = L let L be C_Linear_Combination of V; ::_thesis: 1r * L = L let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (1r * L) . v = L . v thus (1r * L) . v = 1r * (L . v) by Def9 .= L . v ; ::_thesis: verum end; definition let V be non empty CLSStruct ; let L be C_Linear_Combination of V; func - L -> C_Linear_Combination of V equals :: CONVEX4:def 10 (- 1r) * L; correctness coherence (- 1r) * L is C_Linear_Combination of V; ; end; :: deftheorem defines - CONVEX4:def_10_:_ for V being non empty CLSStruct for L being C_Linear_Combination of V holds - L = (- 1r) * L; theorem Th31: :: CONVEX4:31 for V being non empty CLSStruct for v being VECTOR of V for L being C_Linear_Combination of V holds (- L) . v = - (L . v) proof let V be non empty CLSStruct ; ::_thesis: for v being VECTOR of V for L being C_Linear_Combination of V holds (- L) . v = - (L . v) let v be VECTOR of V; ::_thesis: for L being C_Linear_Combination of V holds (- L) . v = - (L . v) let L be C_Linear_Combination of V; ::_thesis: (- L) . v = - (L . v) thus (- L) . v = (- 1r) * (L . v) by Def9 .= - (L . v) ; ::_thesis: verum end; theorem :: CONVEX4:32 for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V st L1 + L2 = ZeroCLC V holds L2 = - L1 proof let V be non empty CLSStruct ; ::_thesis: for L1, L2 being C_Linear_Combination of V st L1 + L2 = ZeroCLC V holds L2 = - L1 let L1, L2 be C_Linear_Combination of V; ::_thesis: ( L1 + L2 = ZeroCLC V implies L2 = - L1 ) assume A1: L1 + L2 = ZeroCLC V ; ::_thesis: L2 = - L1 let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: L2 . v = (- L1) . v (L1 . v) + (L2 . v) = (ZeroCLC V) . v by A1, Def8 .= 0c by Th2 ; hence L2 . v = - (L1 . v) .= (- L1) . v by Th31 ; ::_thesis: verum end; theorem :: CONVEX4:33 for V being non empty CLSStruct for L being C_Linear_Combination of V holds - (- L) = L proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds - (- L) = L let L be C_Linear_Combination of V; ::_thesis: - (- L) = L let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (- (- L)) . v = L . v thus (- (- L)) . v = (((- 1r) * (- 1r)) * L) . v by Th29 .= 1r * (L . v) by Def9 .= L . v ; ::_thesis: verum end; definition let V be non empty CLSStruct ; let L1, L2 be C_Linear_Combination of V; funcL1 - L2 -> C_Linear_Combination of V equals :: CONVEX4:def 11 L1 + (- L2); correctness coherence L1 + (- L2) is C_Linear_Combination of V; ; end; :: deftheorem defines - CONVEX4:def_11_:_ for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V holds L1 - L2 = L1 + (- L2); theorem Th34: :: CONVEX4:34 for V being non empty CLSStruct for v being VECTOR of V for L1, L2 being C_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) proof let V be non empty CLSStruct ; ::_thesis: for v being VECTOR of V for L1, L2 being C_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let v be VECTOR of V; ::_thesis: for L1, L2 being C_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let L1, L2 be C_Linear_Combination of V; ::_thesis: (L1 - L2) . v = (L1 . v) - (L2 . v) thus (L1 - L2) . v = (L1 . v) + ((- L2) . v) by Def8 .= (L1 . v) - (L2 . v) by Th31 ; ::_thesis: verum end; theorem :: CONVEX4:35 for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) proof let V be non empty CLSStruct ; ::_thesis: for L1, L2 being C_Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be C_Linear_Combination of V; ::_thesis: Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier (- L2)) by Th19; hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th24; ::_thesis: verum end; theorem :: CONVEX4:36 for V being non empty CLSStruct for A being Subset of V for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 - L2 is C_Linear_Combination of A proof let V be non empty CLSStruct ; ::_thesis: for A being Subset of V for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 - L2 is C_Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds L1 - L2 is C_Linear_Combination of A let L1, L2 be C_Linear_Combination of V; ::_thesis: ( L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies L1 - L2 is C_Linear_Combination of A ) assume that A1: L1 is C_Linear_Combination of A and A2: L2 is C_Linear_Combination of A ; ::_thesis: L1 - L2 is C_Linear_Combination of A - L2 is C_Linear_Combination of A by A2, Th26; hence L1 - L2 is C_Linear_Combination of A by A1, Th20; ::_thesis: verum end; theorem Th37: :: CONVEX4:37 for V being non empty CLSStruct for L being C_Linear_Combination of V holds L - L = ZeroCLC V proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds L - L = ZeroCLC V let L be C_Linear_Combination of V; ::_thesis: L - L = ZeroCLC V let v be VECTOR of V; :: according to CONVEX4:def_7 ::_thesis: (L - L) . v = (ZeroCLC V) . v thus (L - L) . v = (L . v) - (L . v) by Th34 .= (ZeroCLC V) . v by Th2 ; ::_thesis: verum end; definition let V be non empty CLSStruct ; func C_LinComb V -> set means :Def12: :: CONVEX4:def 12 for x being set holds ( x in it iff x is C_Linear_Combination of V ); existence ex b1 being set st for x being set holds ( x in b1 iff x is C_Linear_Combination of V ) proof defpred S1[ set ] means $1 is C_Linear_Combination of V; consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,COMPLEX) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff x is C_Linear_Combination of V ) let x be set ; ::_thesis: ( x in A iff x is C_Linear_Combination of V ) thus ( x in A implies x is C_Linear_Combination of V ) by A1; ::_thesis: ( x is C_Linear_Combination of V implies x in A ) assume x is C_Linear_Combination of V ; ::_thesis: x in A hence x in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is C_Linear_Combination of V ) ) & ( for x being set holds ( x in b2 iff x is C_Linear_Combination of V ) ) holds b1 = b2 proof let D1, D2 be set ; ::_thesis: ( ( for x being set holds ( x in D1 iff x is C_Linear_Combination of V ) ) & ( for x being set holds ( x in D2 iff x is C_Linear_Combination of V ) ) implies D1 = D2 ) assume A2: for x being set holds ( x in D1 iff x is C_Linear_Combination of V ) ; ::_thesis: ( ex x being set st ( ( x in D2 implies x is C_Linear_Combination of V ) implies ( x is C_Linear_Combination of V & not x in D2 ) ) or D1 = D2 ) assume A3: for x being set holds ( x in D2 iff x is C_Linear_Combination of V ) ; ::_thesis: D1 = D2 thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 ) assume x in D1 ; ::_thesis: x in D2 then x is C_Linear_Combination of V by A2; hence x in D2 by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 ) assume x in D2 ; ::_thesis: x in D1 then x is C_Linear_Combination of V by A3; hence x in D1 by A2; ::_thesis: verum end; end; :: deftheorem Def12 defines C_LinComb CONVEX4:def_12_:_ for V being non empty CLSStruct for b2 being set holds ( b2 = C_LinComb V iff for x being set holds ( x in b2 iff x is C_Linear_Combination of V ) ); registration let V be non empty CLSStruct ; cluster C_LinComb V -> non empty ; coherence not C_LinComb V is empty proof set x = the C_Linear_Combination of V; the C_Linear_Combination of V in C_LinComb V by Def12; hence not C_LinComb V is empty ; ::_thesis: verum end; end; definition let V be non empty CLSStruct ; let e be Element of C_LinComb V; func @ e -> C_Linear_Combination of V equals :: CONVEX4:def 13 e; coherence e is C_Linear_Combination of V by Def12; end; :: deftheorem defines @ CONVEX4:def_13_:_ for V being non empty CLSStruct for e being Element of C_LinComb V holds @ e = e; definition let V be non empty CLSStruct ; let L be C_Linear_Combination of V; func @ L -> Element of C_LinComb V equals :: CONVEX4:def 14 L; coherence L is Element of C_LinComb V by Def12; end; :: deftheorem defines @ CONVEX4:def_14_:_ for V being non empty CLSStruct for L being C_Linear_Combination of V holds @ L = L; definition let V be non empty CLSStruct ; func C_LCAdd V -> BinOp of (C_LinComb V) means :Def15: :: CONVEX4:def 15 for e1, e2 being Element of C_LinComb V holds it . (e1,e2) = (@ e1) + (@ e2); existence ex b1 being BinOp of (C_LinComb V) st for e1, e2 being Element of C_LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) proof deffunc H1( Element of C_LinComb V, 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 being Element of C_LinComb V holds o . (e1,e2) = H1(e1,e2) from BINOP_1:sch_4(); take o ; ::_thesis: for e1, e2 being Element of C_LinComb V holds o . (e1,e2) = (@ e1) + (@ e2) let e1, e2 be Element of C_LinComb V; ::_thesis: o . (e1,e2) = (@ e1) + (@ e2) thus o . (e1,e2) = @ ((@ e1) + (@ e2)) by A1 .= (@ e1) + (@ e2) ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (C_LinComb V) st ( for e1, e2 being Element of C_LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of C_LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds b1 = b2 proof let o1, o2 be BinOp of (C_LinComb V); ::_thesis: ( ( for e1, e2 being Element of C_LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of C_LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ) implies o1 = o2 ) assume A2: for e1, e2 being Element of C_LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: ( ex e1, e2 being Element of C_LinComb V st not o2 . (e1,e2) = (@ e1) + (@ e2) or o1 = o2 ) assume A3: for e1, e2 being Element of C_LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: o1 = o2 now__::_thesis:_for_e1,_e2_being_Element_of_C_LinComb_V_holds_o1_._(e1,e2)_=_o2_._(e1,e2) let e1, e2 be Element of C_LinComb V; ::_thesis: o1 . (e1,e2) = o2 . (e1,e2) thus o1 . (e1,e2) = (@ e1) + (@ e2) by A2 .= o2 . (e1,e2) by A3 ; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def15 defines C_LCAdd CONVEX4:def_15_:_ for V being non empty CLSStruct for b2 being BinOp of (C_LinComb V) holds ( b2 = C_LCAdd V iff for e1, e2 being Element of C_LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ); definition let V be non empty CLSStruct ; func C_LCMult V -> Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) means :Def16: :: CONVEX4:def 16 for a being Complex for e being Element of C_LinComb V holds it . [a,e] = a * (@ e); existence ex b1 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st for a being Complex for e being Element of C_LinComb V holds b1 . [a,e] = a * (@ e) proof defpred S1[ Element of COMPLEX , Element of C_LinComb V, set ] means ex a being Complex st ( a = $1 & $3 = a * (@ $2) ); A1: for x being Element of COMPLEX for e1 being Element of C_LinComb V ex e2 being Element of C_LinComb V st S1[x,e1,e2] proof let x be Element of COMPLEX ; ::_thesis: for e1 being Element of C_LinComb V ex e2 being Element of C_LinComb V st S1[x,e1,e2] let e1 be Element of C_LinComb V; ::_thesis: ex e2 being Element of C_LinComb V st S1[x,e1,e2] take @ (x * (@ e1)) ; ::_thesis: S1[x,e1, @ (x * (@ e1))] take x ; ::_thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) ) thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; ::_thesis: verum end; consider g being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) such that A2: for x being Element of COMPLEX for e being Element of C_LinComb V holds S1[x,e,g . (x,e)] from BINOP_1:sch_3(A1); take g ; ::_thesis: for a being Complex for e being Element of C_LinComb V holds g . [a,e] = a * (@ e) let a be Complex; ::_thesis: for e being Element of C_LinComb V holds g . [a,e] = a * (@ e) let e be Element of C_LinComb V; ::_thesis: g . [a,e] = a * (@ e) a in COMPLEX by XCMPLX_0:def_2; then ex b being Complex st ( b = a & g . (a,e) = b * (@ e) ) by A2; hence g . [a,e] = a * (@ e) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st ( for a being Complex for e being Element of C_LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Complex for e being Element of C_LinComb V holds b2 . [a,e] = a * (@ e) ) holds b1 = b2 proof let g1, g2 be Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V); ::_thesis: ( ( for a being Complex for e being Element of C_LinComb V holds g1 . [a,e] = a * (@ e) ) & ( for a being Complex for e being Element of C_LinComb V holds g2 . [a,e] = a * (@ e) ) implies g1 = g2 ) assume A3: for a being Complex for e being Element of C_LinComb V holds g1 . [a,e] = a * (@ e) ; ::_thesis: ( ex a being Complex ex e being Element of C_LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 ) assume A4: for a being Complex for e being Element of C_LinComb V holds g2 . [a,e] = a * (@ e) ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_Element_of_COMPLEX_ for_e_being_Element_of_C_LinComb_V_holds_g1_._(x,e)_=_g2_._(x,e) let x be Element of COMPLEX ; ::_thesis: for e being Element of C_LinComb V holds g1 . (x,e) = g2 . (x,e) let e be Element of C_LinComb V; ::_thesis: g1 . (x,e) = g2 . (x,e) thus g1 . (x,e) = x * (@ e) by A3 .= g2 . (x,e) by A4 ; ::_thesis: verum end; hence g1 = g2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def16 defines C_LCMult CONVEX4:def_16_:_ for V being non empty CLSStruct for b2 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) holds ( b2 = C_LCMult V iff for a being Complex for e being Element of C_LinComb V holds b2 . [a,e] = a * (@ e) ); definition let V be non empty CLSStruct ; func LC_CLSpace V -> ComplexLinearSpace equals :: CONVEX4:def 17 CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); coherence CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace proof set S = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); A1: now__::_thesis:_for_a,_b_being_Complex for_v,_u,_w_being_VECTOR_of_CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#)_holds_ (_v_+_w_=_w_+_v_&_(u_+_v)_+_w_=_u_+_(v_+_w)_&_v_+_(0._CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#))_=_v_&_ex_w_being_VECTOR_of_CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#)_st_v_+_w_=_0._CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#)_&_a_*_(v_+_w)_=_(a_*_v)_+_(a_*_w)_&_(a_+_b)_*_v_=_(a_*_v)_+_(b_*_v)_&_(a_*_b)_*_v_=_a_*_(b_*_v)_&_1r_*_v_=_v_) let a, b be Complex; ::_thesis: for v, u, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds ( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) let v, u, w be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); ::_thesis: ( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def_2; reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a1 * v, az = a1 * w, bx = b1 * v as Element of C_LinComb V ; A2: ( @ z = w & @ yx = u + v ) ; A3: ( @ xz = v + w & @ ax = a * v ) ; A4: ( @ az = a * w & @ bx = b * v ) ; ( @ x = v & @ y = u ) ; 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 by A2, A3, A4; A5: now__::_thesis:_for_v,_u_being_VECTOR_of_CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#) for_K,_L_being_C_Linear_Combination_of_V_st_v_=_K_&_u_=_L_holds_ v_+_u_=_K_+_L let v, u be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); ::_thesis: for K, L being C_Linear_Combination of V st v = K & u = L holds v + u = K + L let K, L be C_Linear_Combination of V; ::_thesis: ( v = K & u = L implies v + u = K + L ) A6: ( @ (@ K) = K & @ (@ L) = L ) ; assume ( v = K & u = L ) ; ::_thesis: v + u = K + L hence v + u = K + L by A6, Def15; ::_thesis: verum end; hence v + w = K + M .= w + v by A5 ; ::_thesis: ( (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) thus (u + v) + w = LK + M by A5 .= (L + K) + M by A5 .= L + (K + M) by Th22 .= L + KM by A5 .= u + (v + w) by A5 ; ::_thesis: ( v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) thus v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = K + (ZeroCLC V) by A5 .= v by Th23 ; ::_thesis: ( ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) - K in the carrier of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by Def12; then - K in CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by STRUCT_0:def_5; then - K = vector (CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #),(- K)) by RLVECT_2:def_1; then v + (vector (CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #),(- K))) = K - K by A5 .= 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by Th37 ; hence ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) ; ::_thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) A7: now__::_thesis:_for_v_being_VECTOR_of_CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#) for_L_being_C_Linear_Combination_of_V for_a_being_Complex_st_v_=_L_holds_ a_*_v_=_a_*_L let v be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); ::_thesis: for L being C_Linear_Combination of V for a being Complex st v = L holds a * v = a * L let L be C_Linear_Combination of V; ::_thesis: for a being Complex st v = L holds a * v = a * L let a be Complex; ::_thesis: ( v = L implies a * v = a * L ) assume v = L ; ::_thesis: a * v = a * L then (C_LCMult V) . [a,v] = a * (@ (@ L)) by Def16; hence a * v = a * L ; ::_thesis: verum end; hence a * (v + w) = a1 * KM .= a1 * (K + M) by A5 .= (a1 * K) + (a1 * M) by Th28 .= aK + (a1 * M) by A7 .= aK + aM by A7 .= (a * v) + (a * w) by A5 ; ::_thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v ) thus (a + b) * v = (a1 + b1) * K by A7 .= (a1 * K) + (b1 * K) by Th27 .= aK + (b * K) by A7 .= aK + bK by A7 .= (a * v) + (b * v) by A5 ; ::_thesis: ( (a * b) * v = a * (b * v) & 1r * v = v ) thus (a * b) * v = (a * b) * K by A7 .= a1 * (b1 * K) by Th29 .= a * bK by A7 .= a * (b * v) by A7 ; ::_thesis: 1r * v = v thus 1r * v = 1r * K by A7 .= v by Th30 ; ::_thesis: verum end; A8: now__::_thesis:_for_v_being_Element_of_CLSStruct(#_(C_LinComb_V),(@_(ZeroCLC_V)),(C_LCAdd_V),(C_LCMult_V)_#)_holds_v_is_right_complementable let v be Element of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); ::_thesis: v is right_complementable ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by A1; hence v is right_complementable by ALGSTR_0:def_11; ::_thesis: verum end; for u, v, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds (u + v) + w = u + (v + w) by A1; hence CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace by A1, A8, ALGSTR_0:def_16, CLVECT_1:def_2, CLVECT_1:def_3, CLVECT_1:def_4, CLVECT_1:def_5, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum end; end; :: deftheorem defines LC_CLSpace CONVEX4:def_17_:_ for V being non empty CLSStruct holds LC_CLSpace V = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); registration let V be non empty CLSStruct ; cluster LC_CLSpace V -> strict ; coherence ( LC_CLSpace V is strict & not LC_CLSpace V is empty ) ; end; theorem Th38: :: CONVEX4:38 for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = L1 + L2 proof let V be non empty CLSStruct ; ::_thesis: for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = L1 + L2 let L1, L2 be C_Linear_Combination of V; ::_thesis: (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = L1 + L2 set v2 = vector ((LC_CLSpace V),L2); A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ; L2 in the carrier of (LC_CLSpace V) by Def12; then A2: L2 in LC_CLSpace V by STRUCT_0:def_5; L1 in the carrier of (LC_CLSpace V) by Def12; then L1 in LC_CLSpace V by STRUCT_0:def_5; hence (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = (C_LCAdd V) . [L1,(vector ((LC_CLSpace V),L2))] by RLVECT_2:def_1 .= (C_LCAdd V) . ((@ L1),(@ L2)) by A2, RLVECT_2:def_1 .= L1 + L2 by A1, Def15 ; ::_thesis: verum end; theorem Th39: :: CONVEX4:39 for V being non empty CLSStruct for a being Complex for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L proof let V be non empty CLSStruct ; ::_thesis: for a being Complex for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L let a be Complex; ::_thesis: for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L let L be C_Linear_Combination of V; ::_thesis: a * (vector ((LC_CLSpace V),L)) = a * L L in the carrier of (LC_CLSpace V) by Def12; 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, Def16; ::_thesis: verum end; theorem Th40: :: CONVEX4:40 for V being non empty CLSStruct for L being C_Linear_Combination of V holds - (vector ((LC_CLSpace V),L)) = - L proof let V be non empty CLSStruct ; ::_thesis: for L being C_Linear_Combination of V holds - (vector ((LC_CLSpace V),L)) = - L let L be C_Linear_Combination of V; ::_thesis: - (vector ((LC_CLSpace V),L)) = - L thus - (vector ((LC_CLSpace V),L)) = (- 1r) * (vector ((LC_CLSpace V),L)) by CLVECT_1:3 .= - L by Th39 ; ::_thesis: verum end; theorem :: CONVEX4:41 for V being non empty CLSStruct for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) - (vector ((LC_CLSpace V),L2)) = L1 - L2 proof let V be non empty CLSStruct ; ::_thesis: for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) - (vector ((LC_CLSpace V),L2)) = L1 - L2 let L1, L2 be C_Linear_Combination of V; ::_thesis: (vector ((LC_CLSpace V),L1)) - (vector ((LC_CLSpace V),L2)) = L1 - L2 - L2 in C_LinComb V by Def12; then A1: - L2 in LC_CLSpace V by STRUCT_0:def_5; - (vector ((LC_CLSpace V),L2)) = - L2 by Th40 .= 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 Th38; ::_thesis: verum end; definition let V be non empty CLSStruct ; let A be Subset of V; func LC_CLSpace A -> strict Subspace of LC_CLSpace V means :: CONVEX4:def 18 the carrier of it = { l where l is C_Linear_Combination of A : verum } ; existence ex b1 being strict Subspace of LC_CLSpace V st the carrier of b1 = { l where l is C_Linear_Combination of A : verum } proof set X = { l where l is C_Linear_Combination of A : verum } ; { l where l is C_Linear_Combination of A : verum } c= the carrier of (LC_CLSpace V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { l where l is C_Linear_Combination of A : verum } or x in the carrier of (LC_CLSpace V) ) assume x in { l where l is C_Linear_Combination of A : verum } ; ::_thesis: x in the carrier of (LC_CLSpace V) then ex l being C_Linear_Combination of A st x = l ; hence x in the carrier of (LC_CLSpace V) by Def12; ::_thesis: verum end; then reconsider X = { l where l is C_Linear_Combination of A : verum } as Subset of (LC_CLSpace V) ; A1: 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); ::_thesis: ( v in X & u in X implies v + u in X ) assume that A2: v in X and A3: u in X ; ::_thesis: v + u in X consider l1 being C_Linear_Combination of A such that A4: v = l1 by A2; consider l2 being C_Linear_Combination of A such that A5: u = l2 by A3; A6: u = vector ((LC_CLSpace V),l2) by A5, RLVECT_2:1; v = vector ((LC_CLSpace V),l1) by A4, RLVECT_2:1; then v + u = l1 + l2 by A6, Th38; hence v + u in X ; ::_thesis: verum end; ZeroCLC V is C_Linear_Combination of A by Th4; then A7: ZeroCLC V in X ; for a being Complex for v being VECTOR of (LC_CLSpace V) st v in X holds a * v in X proof let a be Complex; ::_thesis: for v being VECTOR of (LC_CLSpace V) st v in X holds a * v in X let v be VECTOR of (LC_CLSpace V); ::_thesis: ( v in X implies a * v in X ) assume v in X ; ::_thesis: a * v in X then consider l being C_Linear_Combination of A such that A8: v = l ; a * v = a * (vector ((LC_CLSpace V),l)) by A8, RLVECT_2:1 .= a * l by Th39 ; then a * v is C_Linear_Combination of A by Th26; hence a * v in X ; ::_thesis: verum end; then X is linearly-closed by A1, CLVECT_1:def_7; hence ex b1 being strict Subspace of LC_CLSpace V st the carrier of b1 = { l where l is C_Linear_Combination of A : verum } by A7, CLVECT_1:54; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace of LC_CLSpace V st the carrier of b1 = { l where l is C_Linear_Combination of A : verum } & the carrier of b2 = { l where l is C_Linear_Combination of A : verum } holds b1 = b2 by CLVECT_1:49; end; :: deftheorem defines LC_CLSpace CONVEX4:def_18_:_ for V being non empty CLSStruct for A being Subset of V for b3 being strict Subspace of LC_CLSpace V holds ( b3 = LC_CLSpace A iff the carrier of b3 = { l where l is C_Linear_Combination of A : verum } ); begin definition let V be ComplexLinearSpace; let W be Subspace of V; func Up W -> Subset of V equals :: CONVEX4:def 19 the carrier of W; coherence the carrier of W is Subset of V by CLVECT_1:def_8; end; :: deftheorem defines Up CONVEX4:def_19_:_ for V being ComplexLinearSpace for W being Subspace of V holds Up W = the carrier of W; registration let V be ComplexLinearSpace; let W be Subspace of V; cluster Up W -> non empty ; coherence not Up W is empty ; end; definition let V be non empty CLSStruct ; let S be Subset of V; attrS is Affine means :Def20: :: CONVEX4:def 20 for x, y being VECTOR of V for z being Complex st z is Real & x in S & y in S holds ((1r - z) * x) + (z * y) in S; end; :: deftheorem Def20 defines Affine CONVEX4:def_20_:_ for V being non empty CLSStruct for S being Subset of V holds ( S is Affine iff for x, y being VECTOR of V for z being Complex st z is Real & x in S & y in S holds ((1r - z) * x) + (z * y) in S ); definition let V be ComplexLinearSpace; func (Omega). V -> strict Subspace of V equals :: CONVEX4:def 21 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); coherence CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V proof set W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); A1: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v proof let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + w = w + v reconsider v9 = v, w9 = w as VECTOR of V ; v + w = v9 + w9 ; hence v + w = w9 + v9 .= w + v ; ::_thesis: verum end; A2: for u, v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (u + v) + w = u + (v + w) proof let u, v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (u + v) + w = u + (v + w) reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ; (u9 + v9) + w9 = u9 + (v9 + w9) by RLVECT_1:def_3; hence (u + v) + w = u + (v + w) ; ::_thesis: verum end; A3: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v is right_complementable proof let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v is right_complementable reconsider v9 = v as VECTOR of V ; v9 is right_complementable by ALGSTR_0:def_16; then consider w9 being VECTOR of V such that A4: v9 + w9 = 0. V by ALGSTR_0:def_11; reconsider w = w9 as VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) thus v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A4; ::_thesis: verum end; A5: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v proof let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v reconsider v9 = v as VECTOR of V ; thus v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V) .= v by RLVECT_1:4 ; ::_thesis: verum end; A6: for a, b being Complex for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v) proof let a, b be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v) let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a * b) * v = a * (b * v) reconsider v9 = v as VECTOR of V ; (a * b) * v9 = a * (b * v9) by CLVECT_1:def_4; hence (a * b) * v = a * (b * v) ; ::_thesis: verum end; A7: for a, b being Complex for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v) proof let a, b be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v) let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider v9 = v as VECTOR of V ; (a + b) * v9 = (a * v9) + (b * v9) by CLVECT_1:def_3; hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum end; A8: for a being Complex for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w) proof let a be Complex; ::_thesis: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w) let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider v9 = v, w9 = w as VECTOR of V ; a * (v9 + w9) = (a * v9) + (a * w9) by CLVECT_1:def_2; hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum end; for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1r * v = v proof let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: 1r * v = v reconsider v9 = v as VECTOR of V ; thus 1r * v = 1r * v9 .= v by CLVECT_1:def_5 ; ::_thesis: verum end; then reconsider W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as ComplexLinearSpace by A1, A2, A5, A3, A8, A7, A6, ALGSTR_0:def_16, CLVECT_1:def_2, CLVECT_1:def_3, CLVECT_1:def_4, CLVECT_1:def_5, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; A9: the Mult of W = the Mult of V | [:COMPLEX, the carrier of W:] by RELSET_1:19; ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19; hence CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V by A9, CLVECT_1:def_8; ::_thesis: verum end; end; :: deftheorem defines (Omega). CONVEX4:def_21_:_ for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); registration let V be non empty CLSStruct ; cluster [#] V -> Affine ; coherence [#] V is Affine proof for x, y being VECTOR of V for z being Complex st z is Real & x in [#] V & y in [#] V holds ((1r - z) * x) + (z * y) in [#] V ; hence [#] V is Affine by Def20; ::_thesis: verum end; cluster empty -> Affine for Element of bool the carrier of V; coherence for b1 being Subset of V st b1 is empty holds b1 is Affine proof let S be Subset of V; ::_thesis: ( S is empty implies S is Affine ) assume S is empty ; ::_thesis: S is Affine then for x, y being VECTOR of V for z being Complex st z is Real & x in S & y in S holds ((1r - z) * x) + (z * y) in S ; hence S is Affine by Def20; ::_thesis: verum end; end; registration let V be non empty CLSStruct ; cluster non empty Affine for Element of bool the carrier of V; existence ex b1 being Subset of V st ( not b1 is empty & b1 is Affine ) proof take [#] V ; ::_thesis: ( not [#] V is empty & [#] V is Affine ) thus ( not [#] V is empty & [#] V is Affine ) ; ::_thesis: verum end; cluster empty Affine for Element of bool the carrier of V; existence ex b1 being Subset of V st ( b1 is empty & b1 is Affine ) proof take {} V ; ::_thesis: ( {} V is empty & {} V is Affine ) thus ( {} V is empty & {} V is Affine ) ; ::_thesis: verum end; end; theorem Th42: :: CONVEX4:42 for a being real number for z being complex number holds Re (a * z) = a * (Re z) proof let a be real number ; ::_thesis: for z being complex number holds Re (a * z) = a * (Re z) let z be complex number ; ::_thesis: Re (a * z) = a * (Re z) A1: a in REAL by XREAL_0:def_1; Re (a * z) = ((Re a) * (Re z)) - ((Im a) * (Im z)) by COMPLEX1:9 .= ((Re a) * (Re z)) - (0 * (Im z)) by A1, COMPLEX1:def_2 .= a * (Re z) by A1, COMPLEX1:def_1 ; hence Re (a * z) = a * (Re z) ; ::_thesis: verum end; theorem Th43: :: CONVEX4:43 for a being real number for z being complex number holds Im (a * z) = a * (Im z) proof let a be real number ; ::_thesis: for z being complex number holds Im (a * z) = a * (Im z) let z be complex number ; ::_thesis: Im (a * z) = a * (Im z) A1: a in REAL by XREAL_0:def_1; Im (a * z) = ((Re a) * (Im z)) + ((Re z) * (Im a)) by COMPLEX1:9 .= ((Re a) * (Im z)) + ((Re z) * 0) by A1, COMPLEX1:def_2 .= a * (Im z) by A1, COMPLEX1:def_1 ; hence Im (a * z) = a * (Im z) ; ::_thesis: verum end; theorem Th44: :: CONVEX4:44 for a being real number for 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 ; ::_thesis: for z being complex number st 0 <= a & a <= 1 holds ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) let z be complex number ; ::_thesis: ( 0 <= a & a <= 1 implies ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) ) assume that A1: 0 <= a and A2: a <= 1 ; ::_thesis: ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) A3: |.((1r - a) * z).| = |.(1r - a).| * |.z.| by COMPLEX1:65 .= (1r - a) * |.z.| by A2, COMPLEX1:43, XREAL_1:48 ; |.(a * z).| = |.a.| * |.z.| by COMPLEX1:65 .= a * |.z.| by A1, COMPLEX1:43 ; hence ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) by A3; ::_thesis: verum end; begin definition let V be non empty CLSStruct ; let M be Subset of V; let r be Complex; funcr * M -> Subset of V equals :: CONVEX4:def 22 { (r * v) where v is Element of V : v in M } ; coherence { (r * v) where v is Element of V : v in M } is Subset of V proof deffunc H1( Element of V) -> Element of the carrier of V = r * $1; defpred S1[ set ] means $1 in M; { H1(v) where v is Element of V : S1[v] } is Subset of V from DOMAIN_1:sch_8(); hence { (r * v) where v is Element of V : v in M } is Subset of V ; ::_thesis: verum end; end; :: deftheorem defines * CONVEX4:def_22_:_ for V being non empty CLSStruct for M being Subset of V for r being Complex holds r * M = { (r * v) where v is Element of V : v in M } ; definition let V be non empty CLSStruct ; let M be Subset of V; attrM is convex means :Def23: :: CONVEX4:def 23 for u, v being VECTOR of V for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M holds (z * u) + ((1r - z) * v) in M; end; :: deftheorem Def23 defines convex CONVEX4:def_23_:_ for V being non empty CLSStruct for M being Subset of V holds ( M is convex iff for u, v being VECTOR of V for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M holds (z * u) + ((1r - z) * v) in M ); theorem :: CONVEX4:45 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M being Subset of V for z being Complex st M is convex holds z * M is convex proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M being Subset of V for z being Complex st M is convex holds z * M is convex let M be Subset of V; ::_thesis: for z being Complex st M is convex holds z * M is convex let z be Complex; ::_thesis: ( M is convex implies z * M is convex ) assume A1: M is convex ; ::_thesis: z * M is convex for u, v being VECTOR of V for 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; ::_thesis: for 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 let s be Complex; ::_thesis: ( ex p being Real st ( s = p & 0 < p & p < 1 ) & u in z * M & v in z * M implies (s * u) + ((1r - s) * v) in z * M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: u in z * M and A4: v in z * M ; ::_thesis: (s * u) + ((1r - s) * v) in z * M consider v9 being Element of V such that A5: v = z * v9 and A6: v9 in M by A4; consider u9 being Element of V such that A7: u = z * u9 and A8: u9 in M by A3; A9: (s * u) + ((1r - s) * v) = ((s * z) * u9) + ((1r - s) * (z * v9)) by A7, A5, CLVECT_1:def_4 .= ((z * s) * u9) + ((z * (1r - s)) * v9) by CLVECT_1:def_4 .= (z * (s * u9)) + ((z * (1r - s)) * v9) by CLVECT_1:def_4 .= (z * (s * u9)) + (z * ((1r - s) * v9)) by CLVECT_1:def_4 .= z * ((s * u9) + ((1r - s) * v9)) by CLVECT_1:def_2 ; (s * u9) + ((1r - s) * v9) in M by A1, A2, A8, A6, Def23; hence (s * u) + ((1r - s) * v) in z * M by A9; ::_thesis: verum end; hence z * M is convex by Def23; ::_thesis: verum end; theorem :: CONVEX4:46 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M, N being Subset of V st M is convex & N is convex holds M + N is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds M + N is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M + N is convex ) assume A1: ( M is convex & N is convex ) ; ::_thesis: M + N is convex for u, v being VECTOR of V for 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; ::_thesis: for 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 let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M + N & v in M + N implies (z * u) + ((1r - z) * v) in M + N ) assume that A2: ex r being Real st ( z = r & 0 < r & r < 1 ) and A3: u in M + N and A4: v in M + N ; ::_thesis: (z * u) + ((1r - z) * v) in M + N consider x2, y2 being Element of V such that A5: v = x2 + y2 and A6: ( x2 in M & y2 in N ) by A4; consider x1, y1 being Element of V such that A7: u = x1 + y1 and A8: ( x1 in M & y1 in N ) by A3; A9: (z * u) + ((1r - z) * v) = ((z * x1) + (z * y1)) + ((1r - z) * (x2 + y2)) by A7, 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_3 .= (((z * x1) + ((1r - z) * x2)) + (z * y1)) + ((1r - z) * y2) by RLVECT_1:def_3 .= ((z * x1) + ((1r - z) * x2)) + ((z * y1) + ((1r - z) * y2)) by RLVECT_1:def_3 ; ( (z * x1) + ((1r - z) * x2) in M & (z * y1) + ((1r - z) * y2) in N ) by A1, A2, A8, A6, Def23; hence (z * u) + ((1r - z) * v) in M + N by A9; ::_thesis: verum end; hence M + N is convex by Def23; ::_thesis: verum end; theorem :: CONVEX4:47 for V being ComplexLinearSpace for M, N being Subset of V st M is convex & N is convex holds M - N is convex proof let V be ComplexLinearSpace; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds M - N is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M - N is convex ) assume A1: ( M is convex & N is convex ) ; ::_thesis: M - N is convex for u, v being VECTOR of V for 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; ::_thesis: for 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 let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M - N & v in M - N implies (z * u) + ((1r - z) * v) in M - N ) assume that A2: ex r being Real st ( z = r & 0 < r & r < 1 ) and A3: u in M - N and A4: v in M - N ; ::_thesis: (z * u) + ((1r - z) * v) in M - N consider x2, y2 being Element of V such that A5: v = x2 - y2 and A6: ( x2 in M & y2 in N ) by A4; consider x1, y1 being Element of V such that A7: u = x1 - y1 and A8: ( x1 in M & y1 in N ) by A3; A9: (z * u) + ((1r - z) * v) = ((z * x1) - (z * y1)) + ((1r - z) * (x2 - y2)) by A7, A5, CLVECT_1:9 .= ((z * x1) - (z * y1)) + (((1r - z) * x2) - ((1r - z) * y2)) by CLVECT_1:9 .= (((z * x1) - (z * y1)) + ((1r - z) * x2)) - ((1r - z) * y2) by RLVECT_1:def_3 .= ((z * x1) - ((z * y1) - ((1r - z) * x2))) - ((1r - z) * y2) by RLVECT_1:29 .= ((z * x1) + (((1r - z) * x2) + (- (z * y1)))) - ((1r - z) * y2) by RLVECT_1:33 .= (((z * x1) + ((1r - z) * x2)) + (- (z * y1))) - ((1r - z) * y2) by RLVECT_1:def_3 .= ((z * x1) + ((1r - z) * x2)) + ((- (z * y1)) - ((1r - z) * y2)) by RLVECT_1:def_3 .= ((z * x1) + ((1r - z) * x2)) - ((z * y1) + ((1r - z) * y2)) by RLVECT_1:30 ; ( (z * x1) + ((1r - z) * x2) in M & (z * y1) + ((1r - z) * y2) in N ) by A1, A2, A8, A6, Def23; hence (z * u) + ((1r - z) * v) in M - N by A9; ::_thesis: verum end; hence M - N is convex by Def23; ::_thesis: verum end; theorem Th48: :: CONVEX4:48 for V being non empty CLSStruct for 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 ; ::_thesis: for 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 ) let M be Subset of V; ::_thesis: ( 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 ) 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 ; ::_thesis: 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 z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) implies (z * M) + ((1r - z) * M) c= M ) assume A3: ex r being Real st ( z = r & 0 < r & r < 1 ) ; ::_thesis: (z * M) + ((1r - z) * M) c= M 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; ::_thesis: ( x in (z * M) + ((1r - z) * M) implies x in M ) assume x in (z * M) + ((1r - z) * M) ; ::_thesis: x in M then consider u, v being Element of V such that A4: x = u + v and A5: ( u in z * M & v in (1r - z) * M ) ; ( ex w1 being Element of V st ( u = z * w1 & w1 in M ) & ex w2 being Element of V st ( v = (1r - z) * w2 & w2 in M ) ) by A5; hence x in M by A2, A3, A4, Def23; ::_thesis: verum end; hence (z * M) + ((1r - z) * M) c= M by SUBSET_1:2; ::_thesis: verum 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 A6: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) holds (z * M) + ((1r - z) * M) c= M ; ::_thesis: M is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M holds (z * u) + ((1r - z) * v) in M let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M implies (z * u) + ((1r - z) * v) in M ) assume ex r being Real st ( z = r & 0 < r & r < 1 ) ; ::_thesis: ( not u in M or not v in M or (z * u) + ((1r - z) * v) in M ) then A7: (z * M) + ((1r - z) * M) c= M by A6; assume ( u in M & v in M ) ; ::_thesis: (z * u) + ((1r - z) * 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 (z * u) + ((1r - z) * v) in M by A7; ::_thesis: verum end; hence ( 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 ) by A1; ::_thesis: verum end; theorem :: CONVEX4:49 for V being non empty Abelian CLSStruct for 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 non empty Abelian CLSStruct ; ::_thesis: for 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 let M be Subset of V; ::_thesis: ( M is convex implies for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) holds ((1r - z) * M) + (z * M) c= M ) assume A1: M is convex ; ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) holds ((1r - z) * M) + (z * M) c= M let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) implies ((1r - z) * M) + (z * M) c= M ) assume A2: ex r being Real st ( z = r & 0 < r & r < 1 ) ; ::_thesis: ((1r - z) * M) + (z * M) c= M 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; ::_thesis: ( x in ((1r - z) * M) + (z * M) implies x in M ) assume x in ((1r - z) * M) + (z * M) ; ::_thesis: x in M then consider u, v being Element of V such that A3: x = u + v and A4: ( u in (1r - z) * M & v in z * M ) ; ( ex w1 being Element of V st ( u = (1r - z) * w1 & w1 in M ) & ex w2 being Element of V st ( v = z * w2 & w2 in M ) ) by A4; hence x in M by A1, A2, A3, Def23; ::_thesis: verum end; hence ((1r - z) * M) + (z * M) c= M by SUBSET_1:2; ::_thesis: verum end; theorem :: CONVEX4:50 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M, N being Subset of V st M is convex & N is convex holds for z being Complex holds (z * M) + ((1r - z) * N) is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds for z being Complex holds (z * M) + ((1r - z) * N) is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies for z being Complex holds (z * M) + ((1r - z) * N) is convex ) assume that A1: M is convex and A2: N is convex ; ::_thesis: for z being Complex holds (z * M) + ((1r - z) * N) is convex let z be Complex; ::_thesis: (z * M) + ((1r - z) * N) is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in (z * M) + ((1r - z) * N) & v in (z * M) + ((1r - z) * N) holds (z * u) + ((1r - z) * v) in (z * M) + ((1r - z) * N) let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & u in (z * M) + ((1r - z) * N) & v in (z * M) + ((1r - z) * N) implies (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) ) assume that A3: ex p being Real st ( s = p & 0 < p & p < 1 ) and A4: u in (z * M) + ((1r - z) * N) and A5: v in (z * M) + ((1r - z) * N) ; ::_thesis: (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) consider x2, y2 being VECTOR of V such that A6: v = x2 + y2 and A7: x2 in z * M and A8: y2 in (1r - z) * N by A5; consider x1, y1 being VECTOR of V such that A9: u = x1 + y1 and A10: x1 in z * M and A11: y1 in (1r - z) * N by A4; consider mx2 being VECTOR of V such that A12: x2 = z * mx2 and A13: mx2 in M by A7; consider mx1 being VECTOR of V such that A14: x1 = z * mx1 and A15: mx1 in M by A10; A16: (s * x1) + ((1r - s) * x2) = ((s * z) * mx1) + ((1r - s) * (z * mx2)) by A14, A12, CLVECT_1:def_4 .= ((s * z) * mx1) + (((1r - s) * z) * mx2) by CLVECT_1:def_4 .= (z * (s * mx1)) + (((1r - s) * z) * mx2) by CLVECT_1:def_4 .= (z * (s * mx1)) + (z * ((1r - s) * mx2)) by CLVECT_1:def_4 .= z * ((s * mx1) + ((1r - s) * mx2)) by CLVECT_1:def_2 ; consider ny2 being VECTOR of V such that A17: y2 = (1r - z) * ny2 and A18: ny2 in N by A8; consider ny1 being VECTOR of V such that A19: y1 = (1r - z) * ny1 and A20: ny1 in N by A11; A21: (s * y1) + ((1r - s) * y2) = ((s * (1r - z)) * ny1) + ((1r - s) * ((1r - z) * ny2)) by A19, A17, CLVECT_1:def_4 .= ((s * (1r - z)) * ny1) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def_4 .= ((1r - z) * (s * ny1)) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def_4 .= ((1r - z) * (s * ny1)) + ((1r - z) * ((1r - s) * ny2)) by CLVECT_1:def_4 .= (1r - z) * ((s * ny1) + ((1r - s) * ny2)) by CLVECT_1:def_2 ; (s * ny1) + ((1r - s) * ny2) in N by A2, A3, A20, A18, Def23; then A22: (s * y1) + ((1r - s) * y2) in (1r - z) * N by A21; (s * mx1) + ((1r - s) * mx2) in M by A1, A3, A15, A13, Def23; then A23: (s * x1) + ((1r - s) * x2) in z * M by A16; (s * u) + ((1r - s) * v) = ((s * x1) + (s * y1)) + ((1r - s) * (x2 + y2)) by A9, A6, 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_3 .= (((s * x1) + ((1r - s) * x2)) + (s * y1)) + ((1r - s) * y2) by RLVECT_1:def_3 .= ((s * x1) + ((1r - s) * x2)) + ((s * y1) + ((1r - s) * y2)) by RLVECT_1:def_3 ; hence (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) by A23, A22; ::_thesis: verum end; theorem Th51: :: CONVEX4:51 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M being Subset of V holds 1r * M = M proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M being Subset of V holds 1r * M = M let M be Subset of V; ::_thesis: 1r * M = M for v being Element of V st v in M holds v in 1r * M proof let v be Element of V; ::_thesis: ( v in M implies v in 1r * M ) A1: v = 1r * v by CLVECT_1:def_5; assume v in M ; ::_thesis: v in 1r * M hence v in 1r * M by A1; ::_thesis: verum end; then A2: M c= 1r * M by SUBSET_1:2; for v being Element of V st v in 1r * M holds v in M proof let v be Element of V; ::_thesis: ( v in 1r * M implies v in M ) assume v in 1r * M ; ::_thesis: v in M then ex x being Element of V st ( v = 1r * x & x in M ) ; hence v in M by CLVECT_1:def_5; ::_thesis: verum end; then 1r * M c= M by SUBSET_1:2; hence 1r * M = M by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th52: :: CONVEX4:52 for V being ComplexLinearSpace for M being non empty Subset of V holds 0c * M = {(0. V)} proof let V be ComplexLinearSpace; ::_thesis: for M being non empty Subset of V holds 0c * M = {(0. V)} let M be non empty Subset of V; ::_thesis: 0c * M = {(0. V)} for v being Element of V st v in {(0. V)} holds v in 0c * M proof let v be Element of V; ::_thesis: ( v in {(0. V)} implies v in 0c * M ) consider x being set such that A1: x in M by XBOOLE_0:def_1; reconsider x = x as Element of V by A1; assume v in {(0. V)} ; ::_thesis: v in 0c * M then v = 0. V by TARSKI:def_1; then v = 0c * x by CLVECT_1:1; hence v in 0c * M by A1; ::_thesis: verum end; then A2: {(0. V)} c= 0c * M by SUBSET_1:2; for v being Element of V st v in 0c * M holds v in {(0. V)} proof let v be Element of V; ::_thesis: ( v in 0c * M implies v in {(0. V)} ) assume v in 0c * M ; ::_thesis: v in {(0. V)} then ex x being Element of V st ( v = 0c * x & x in M ) ; then v = 0. V by CLVECT_1:1; hence v in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; then 0c * M c= {(0. V)} by SUBSET_1:2; hence 0c * M = {(0. V)} by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CONVEX4:53 for V being non empty add-associative addLoopStr for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) proof let V be non empty add-associative addLoopStr ; ::_thesis: for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) let M1, M2, M3 be Subset of V; ::_thesis: (M1 + M2) + M3 = M1 + (M2 + M3) 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; ::_thesis: ( x in M1 + (M2 + M3) implies x in (M1 + M2) + M3 ) assume x in M1 + (M2 + M3) ; ::_thesis: x in (M1 + M2) + M3 then consider x1, x9 being Element of V such that A1: ( x = x1 + x9 & x1 in M1 ) and A2: x9 in M2 + M3 ; consider x2, x3 being Element of V such that A3: ( x9 = x2 + x3 & x2 in M2 ) and A4: x3 in M3 by A2; ( x = (x1 + x2) + x3 & x1 + x2 in M1 + M2 ) by A1, A3, RLVECT_1:def_3; hence x in (M1 + M2) + M3 by A4; ::_thesis: verum end; then A5: M1 + (M2 + M3) c= (M1 + M2) + M3 by SUBSET_1:2; 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; ::_thesis: ( x in (M1 + M2) + M3 implies x in M1 + (M2 + M3) ) assume x in (M1 + M2) + M3 ; ::_thesis: x in M1 + (M2 + M3) then consider x9, x3 being Element of V such that A6: x = x9 + x3 and A7: x9 in M1 + M2 and A8: x3 in M3 ; consider x1, x2 being Element of V such that A9: x9 = x1 + x2 and A10: x1 in M1 and A11: x2 in M2 by A7; ( x = x1 + (x2 + x3) & x2 + x3 in M2 + M3 ) by A6, A8, A9, A11, RLVECT_1:def_3; hence x in M1 + (M2 + M3) by A10; ::_thesis: verum end; then (M1 + M2) + M3 c= M1 + (M2 + M3) by SUBSET_1:2; hence (M1 + M2) + M3 = M1 + (M2 + M3) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th54: :: CONVEX4:54 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M being Subset of V for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M being Subset of V for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M let M be Subset of V; ::_thesis: for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M let z1, z2 be Complex; ::_thesis: z1 * (z2 * M) = (z1 * z2) * M 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; ::_thesis: ( x in z1 * (z2 * M) implies x in (z1 * z2) * M ) assume x in z1 * (z2 * M) ; ::_thesis: x in (z1 * z2) * M then consider w1 being VECTOR of V such that A1: x = z1 * w1 and A2: w1 in z2 * M ; consider w2 being VECTOR of V such that A3: w1 = z2 * w2 and A4: w2 in M by A2; x = (z1 * z2) * w2 by A1, A3, CLVECT_1:def_4; hence x in (z1 * z2) * M by A4; ::_thesis: verum end; then A5: z1 * (z2 * M) c= (z1 * z2) * M by SUBSET_1:2; 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; ::_thesis: ( x in (z1 * z2) * M implies x in z1 * (z2 * M) ) assume x in (z1 * z2) * M ; ::_thesis: x in z1 * (z2 * M) then consider w1 being VECTOR of V such that A6: ( x = (z1 * z2) * w1 & w1 in M ) ; ( x = z1 * (z2 * w1) & z2 * w1 in z2 * M ) by A6, CLVECT_1:def_4; hence x in z1 * (z2 * M) ; ::_thesis: verum end; then (z1 * z2) * M c= z1 * (z2 * M) by SUBSET_1:2; hence z1 * (z2 * M) = (z1 * z2) * M by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th55: :: CONVEX4:55 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M1, M2 being Subset of V for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2) proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M1, M2 being Subset of V for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2) let M1, M2 be Subset of V; ::_thesis: for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2) let z be Complex; ::_thesis: z * (M1 + M2) = (z * M1) + (z * M2) 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; ::_thesis: ( x in (z * M1) + (z * M2) implies x in z * (M1 + M2) ) assume x in (z * M1) + (z * M2) ; ::_thesis: x in z * (M1 + M2) then consider w1, w2 being VECTOR of V such that A1: x = w1 + w2 and A2: w1 in z * M1 and A3: w2 in z * M2 ; consider v2 being VECTOR of V such that A4: w2 = z * v2 and A5: v2 in M2 by A3; consider v1 being VECTOR of V such that A6: w1 = z * v1 and A7: v1 in M1 by A2; A8: v1 + v2 in M1 + M2 by A7, A5; x = z * (v1 + v2) by A1, A6, A4, CLVECT_1:def_2; hence x in z * (M1 + M2) by A8; ::_thesis: verum end; then A9: (z * M1) + (z * M2) c= z * (M1 + M2) by SUBSET_1:2; 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; ::_thesis: ( x in z * (M1 + M2) implies x in (z * M1) + (z * M2) ) assume x in z * (M1 + M2) ; ::_thesis: x in (z * M1) + (z * M2) then consider w9 being VECTOR of V such that A10: x = z * w9 and A11: w9 in M1 + M2 ; consider w1, w2 being VECTOR of V such that A12: w9 = w1 + w2 and A13: ( w1 in M1 & w2 in M2 ) by A11; A14: ( z * w1 in z * M1 & z * w2 in z * M2 ) by A13; x = (z * w1) + (z * w2) by A10, A12, CLVECT_1:def_2; hence x in (z * M1) + (z * M2) by A14; ::_thesis: verum end; then z * (M1 + M2) c= (z * M1) + (z * M2) by SUBSET_1:2; hence z * (M1 + M2) = (z * M1) + (z * M2) by A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CONVEX4:56 for V being ComplexLinearSpace for M being Subset of V for v being VECTOR of V holds ( M is convex iff v + M is convex ) proof let V be ComplexLinearSpace; ::_thesis: for M being Subset of V for v being VECTOR of V holds ( M is convex iff v + M is convex ) let M be Subset of V; ::_thesis: for v being VECTOR of V holds ( M is convex iff v + M is convex ) let v be VECTOR of V; ::_thesis: ( M is convex iff v + M is convex ) A1: ( v + M is convex implies M is convex ) proof assume A2: v + M is convex ; ::_thesis: M is convex let w1, w2 be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & w1 in M & w2 in M holds (z * w1) + ((1r - z) * w2) in M let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & w1 in M & w2 in M implies (z * w1) + ((1r - z) * w2) in M ) assume that A3: ex r being Real st ( z = r & 0 < r & r < 1 ) and A4: ( w1 in M & w2 in M ) ; ::_thesis: (z * w1) + ((1r - z) * w2) in M set x1 = v + w1; set x2 = v + w2; ( v + w1 in v + M & v + w2 in { (v + w) where w is VECTOR of V : w in M } ) by A4; then A5: (z * (v + w1)) + ((1r - z) * (v + w2)) in v + M by A2, A3, Def23; (z * (v + w1)) + ((1r - z) * (v + w2)) = ((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_3 .= (((z * v) + ((1r - z) * v)) + (z * w1)) + ((1r - z) * w2) by RLVECT_1:def_3 .= (((z + (1r - z)) * v) + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def_3 .= (v + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def_5 .= v + ((z * w1) + ((1r - z) * w2)) by RLVECT_1:def_3 ; then ex w being VECTOR of V st ( v + ((z * w1) + ((1r - z) * w2)) = v + w & w in M ) by A5; hence (z * w1) + ((1r - z) * w2) in M by RLVECT_1:8; ::_thesis: verum end; ( M is convex implies v + M is convex ) proof assume A6: M is convex ; ::_thesis: v + M is convex let w1, w2 be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & w1 in v + M & w2 in v + M holds (z * w1) + ((1r - z) * w2) in v + M let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & w1 in v + M & w2 in v + M implies (z * w1) + ((1r - z) * w2) in v + M ) assume that A7: ex r being Real st ( z = r & 0 < r & r < 1 ) and A8: w1 in v + M and A9: w2 in v + M ; ::_thesis: (z * w1) + ((1r - z) * w2) in v + M consider x2 being VECTOR of V such that A10: w2 = v + x2 and A11: x2 in M by A9; consider x1 being VECTOR of V such that A12: w1 = v + x1 and A13: x1 in M by A8; A14: (z * w1) + ((1r - z) * w2) = ((z * v) + (z * x1)) + ((1r - z) * (v + x2)) by A12, A10, 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_3 .= (((z * v) + ((1r - z) * v)) + (z * x1)) + ((1r - z) * x2) by RLVECT_1:def_3 .= (((z + (1r - z)) * v) + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def_3 .= (v + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def_5 .= v + ((z * x1) + ((1r - z) * x2)) by RLVECT_1:def_3 ; (z * x1) + ((1r - z) * x2) in M by A6, A7, A13, A11, Def23; hence (z * w1) + ((1r - z) * w2) in v + M by A14; ::_thesis: verum end; hence ( M is convex iff v + M is convex ) by A1; ::_thesis: verum end; theorem :: CONVEX4:57 for V being ComplexLinearSpace holds Up ((0). V) is convex proof let V be ComplexLinearSpace; ::_thesis: Up ((0). V) is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in Up ((0). V) & v in Up ((0). V) holds (z * u) + ((1r - z) * v) in Up ((0). V) let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in Up ((0). V) & v in Up ((0). V) implies (z * u) + ((1r - z) * v) in Up ((0). V) ) assume that ex r being Real st ( z = r & 0 < r & r < 1 ) and A1: u in Up ((0). V) and A2: v in Up ((0). V) ; ::_thesis: (z * u) + ((1r - z) * v) in Up ((0). V) v in {(0. V)} by A2, CLVECT_1:def_9; then A3: v = 0. V by TARSKI:def_1; u in {(0. V)} by A1, CLVECT_1:def_9; then u = 0. V by TARSKI:def_1; then (z * u) + ((1r - z) * v) = (0. V) + ((1r - z) * (0. V)) by A3, CLVECT_1:1 .= (0. V) + (0. V) by CLVECT_1:1 .= 0. V by RLVECT_1:4 ; then (z * u) + ((1r - z) * v) in {(0. V)} by TARSKI:def_1; hence (z * u) + ((1r - z) * v) in Up ((0). V) by CLVECT_1:def_9; ::_thesis: verum end; theorem :: CONVEX4:58 for V being ComplexLinearSpace holds Up ((Omega). V) is convex proof let V be ComplexLinearSpace; ::_thesis: Up ((Omega). V) is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in Up ((Omega). V) & v in Up ((Omega). V) holds (z * u) + ((1r - z) * v) in Up ((Omega). V) thus for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in Up ((Omega). V) & v in Up ((Omega). V) holds (z * u) + ((1r - z) * v) in Up ((Omega). V) ; ::_thesis: verum end; theorem Th59: :: CONVEX4:59 for V being non empty CLSStruct for M being Subset of V st M = {} holds M is convex proof let V be non empty CLSStruct ; ::_thesis: for M being Subset of V st M = {} holds M is convex let M be Subset of V; ::_thesis: ( M = {} implies M is convex ) A1: for u, v being VECTOR of V for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in {} & v in {} holds (z * u) + ((1r - z) * v) in {} ; assume M = {} ; ::_thesis: M is convex hence M is convex by A1, Def23; ::_thesis: verum end; theorem Th60: :: CONVEX4:60 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M1, M2 being Subset of V for z1, z2 being Complex st M1 is convex & M2 is convex holds (z1 * M1) + (z2 * M2) is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M1, M2 being Subset of V for z1, z2 being Complex st M1 is convex & M2 is convex holds (z1 * M1) + (z2 * M2) is convex let M1, M2 be Subset of V; ::_thesis: for z1, z2 being Complex st M1 is convex & M2 is convex holds (z1 * M1) + (z2 * M2) is convex let z1, z2 be Complex; ::_thesis: ( M1 is convex & M2 is convex implies (z1 * M1) + (z2 * M2) is convex ) assume that A1: M1 is convex and A2: M2 is convex ; ::_thesis: (z1 * M1) + (z2 * M2) is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in (z1 * M1) + (z2 * M2) & v in (z1 * M1) + (z2 * M2) holds (z * u) + ((1r - z) * v) in (z1 * M1) + (z2 * M2) let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & u in (z1 * M1) + (z2 * M2) & v in (z1 * M1) + (z2 * M2) implies (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2) ) assume that A3: ex p being Real st ( s = p & 0 < p & p < 1 ) and A4: u in (z1 * M1) + (z2 * M2) and A5: v in (z1 * M1) + (z2 * M2) ; ::_thesis: (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2) consider v1, v2 being VECTOR of V such that A6: v = v1 + v2 and A7: v1 in z1 * M1 and A8: v2 in z2 * M2 by A5; consider u1, u2 being VECTOR of V such that A9: u = u1 + u2 and A10: u1 in z1 * M1 and A11: u2 in z2 * M2 by A4; consider y1 being VECTOR of V such that A12: v1 = z1 * y1 and A13: y1 in M1 by A7; consider x1 being VECTOR of V such that A14: u1 = z1 * x1 and A15: x1 in M1 by A10; A16: (s * u1) + ((1r - s) * v1) = ((z1 * s) * x1) + ((1r - s) * (z1 * y1)) by A14, A12, CLVECT_1:def_4 .= ((z1 * s) * x1) + ((z1 * (1r - s)) * y1) by CLVECT_1:def_4 .= (z1 * (s * x1)) + ((z1 * (1r - s)) * y1) by CLVECT_1:def_4 .= (z1 * (s * x1)) + (z1 * ((1r - s) * y1)) by CLVECT_1:def_4 .= z1 * ((s * x1) + ((1r - s) * y1)) by CLVECT_1:def_2 ; consider y2 being VECTOR of V such that A17: v2 = z2 * y2 and A18: y2 in M2 by A8; consider x2 being VECTOR of V such that A19: u2 = z2 * x2 and A20: x2 in M2 by A11; A21: (s * u2) + ((1r - s) * v2) = ((z2 * s) * x2) + ((1r - s) * (z2 * y2)) by A19, A17, CLVECT_1:def_4 .= ((z2 * s) * x2) + ((z2 * (1r - s)) * y2) by CLVECT_1:def_4 .= (z2 * (s * x2)) + ((z2 * (1r - s)) * y2) by CLVECT_1:def_4 .= (z2 * (s * x2)) + (z2 * ((1r - s) * y2)) by CLVECT_1:def_4 .= z2 * ((s * x2) + ((1r - s) * y2)) by CLVECT_1:def_2 ; (s * x2) + ((1r - s) * y2) in M2 by A2, A3, A20, A18, Def23; then A22: (s * u2) + ((1r - s) * v2) in z2 * M2 by A21; (s * x1) + ((1r - s) * y1) in M1 by A1, A3, A15, A13, Def23; then A23: (s * u1) + ((1r - s) * v1) in z1 * M1 by A16; (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_3 .= (((s * u1) + ((1r - s) * v1)) + (s * u2)) + ((1r - s) * v2) by RLVECT_1:def_3 .= ((s * u1) + ((1r - s) * v1)) + ((s * u2) + ((1r - s) * v2)) by RLVECT_1:def_3 ; hence (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2) by A9, A6, A23, A22; ::_thesis: verum end; theorem Th61: :: CONVEX4:61 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M being Subset of V for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M) proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M being Subset of V for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M) let M be Subset of V; ::_thesis: for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M) let z1, z2 be Complex; ::_thesis: (z1 + z2) * M c= (z1 * M) + (z2 * M) 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; ::_thesis: ( x in (z1 + z2) * M implies x in (z1 * M) + (z2 * M) ) assume x in (z1 + z2) * M ; ::_thesis: x in (z1 * M) + (z2 * M) then consider w being VECTOR of V such that A1: x = (z1 + z2) * w and A2: w in M ; A3: z2 * w in z2 * M by A2; ( x = (z1 * w) + (z2 * w) & z1 * w in z1 * M ) by A1, A2, CLVECT_1:def_3; hence x in (z1 * M) + (z2 * M) by A3; ::_thesis: verum end; hence (z1 + z2) * M c= (z1 * M) + (z2 * M) by SUBSET_1:2; ::_thesis: verum end; theorem Th62: :: CONVEX4:62 for V being non empty CLSStruct for M, N being Subset of V for z being Complex st M c= N holds z * M c= z * N proof let V be non empty CLSStruct ; ::_thesis: for M, N being Subset of V for z being Complex st M c= N holds z * M c= z * N let M, N be Subset of V; ::_thesis: for z being Complex st M c= N holds z * M c= z * N let z be Complex; ::_thesis: ( M c= N implies z * M c= z * N ) assume A1: M c= N ; ::_thesis: z * M c= z * N now__::_thesis:_for_x_being_VECTOR_of_V_st_x_in_z_*_M_holds_ x_in_z_*_N let x be VECTOR of V; ::_thesis: ( x in z * M implies x in z * N ) assume x in z * M ; ::_thesis: x in z * N then ex w being VECTOR of V st ( x = z * w & w in M ) ; hence x in z * N by A1; ::_thesis: verum end; hence z * M c= z * N by SUBSET_1:2; ::_thesis: verum end; theorem Th63: :: CONVEX4:63 for V being non empty CLSStruct for M being empty Subset of V for z being Complex holds z * M = {} proof let V be non empty CLSStruct ; ::_thesis: for M being empty Subset of V for z being Complex holds z * M = {} let M be empty Subset of V; ::_thesis: for z being Complex holds z * M = {} let z be Complex; ::_thesis: z * M = {} now__::_thesis:_for_x_being_VECTOR_of_V_st_x_in_z_*_M_holds_ x_in_{} let x be VECTOR of V; ::_thesis: ( x in z * M implies x in {} ) assume x in z * M ; ::_thesis: x in {} then ex v being VECTOR of V st ( x = z * v & v in {} ) ; hence x in {} ; ::_thesis: verum end; then z * M c= {} by SUBSET_1:2; hence z * M = {} ; ::_thesis: verum end; theorem Th64: :: CONVEX4:64 for V being non empty addLoopStr for M being empty Subset of V for N being Subset of V holds M + N = {} proof let V be non empty addLoopStr ; ::_thesis: for M being empty Subset of V for N being Subset of V holds M + N = {} let M be empty Subset of V; ::_thesis: for N being Subset of V holds M + N = {} let N be Subset of V; ::_thesis: M + N = {} now__::_thesis:_for_x_being_Element_of_V_st_x_in_M_+_N_holds_ x_in_{} let x be Element of V; ::_thesis: ( x in M + N implies x in {} ) assume x in M + N ; ::_thesis: x in {} then ex u, v being Element of V st ( x = u + v & u in {} & v in N ) ; hence x in {} ; ::_thesis: verum end; then M + N c= {} by SUBSET_1:2; hence M + N = {} ; ::_thesis: verum end; theorem Th65: :: CONVEX4:65 for V being non empty right_zeroed addLoopStr for M being Subset of V holds M + {(0. V)} = M proof let V be non empty right_zeroed addLoopStr ; ::_thesis: for M being Subset of V holds M + {(0. V)} = M let M be Subset of V; ::_thesis: M + {(0. V)} = M for x being Element of V st x in M + {(0. V)} holds x in M proof let x be Element of V; ::_thesis: ( x in M + {(0. V)} implies x in M ) assume x in M + {(0. V)} ; ::_thesis: x in M then consider u, v being Element of V such that A1: ( x = u + v & u in M ) and A2: v in {(0. V)} ; v = 0. V by A2, TARSKI:def_1; hence x in M by A1, RLVECT_1:def_4; ::_thesis: verum end; then A3: M + {(0. V)} c= M by SUBSET_1:2; for x being Element of V st x in M holds x in M + {(0. V)} proof let x be Element of V; ::_thesis: ( x in M implies x in M + {(0. V)} ) A4: ( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def_4, TARSKI:def_1; assume x in M ; ::_thesis: x in M + {(0. V)} hence x in M + {(0. V)} by A4; ::_thesis: verum end; then M c= M + {(0. V)} by SUBSET_1:2; hence M + {(0. V)} = M by A3, XBOOLE_0:def_10; ::_thesis: verum end; Lm2: for V being ComplexLinearSpace for M being Subset of V for 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; ::_thesis: for M being Subset of V for 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 let M be Subset of V; ::_thesis: for 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 let z1, z2 be Complex; ::_thesis: ( ex r1, r2 being Real st ( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex implies (z1 * M) + (z2 * M) c= (z1 + z2) * M ) assume that A1: ex r1, r2 being Real st ( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) and A2: M is convex ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M consider r1, r2 being Real such that A3: z1 = r1 and A4: z2 = r2 and A5: r1 >= 0 and A6: r2 >= 0 by A1; percases ( M is empty or not M is empty ) ; suppose M is empty ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M then ( z1 * M = {} & (z1 + z2) * M = {} ) by Th63; hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by Th64; ::_thesis: verum end; supposeA7: not M is empty ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M percases ( z1 = 0 or z2 = 0 or ( z1 <> 0 & z2 <> 0 ) ) ; supposeA8: z1 = 0 ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M then z1 * M = {(0. V)} by A7, Th52; hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A8, Th65; ::_thesis: verum end; supposeA9: z2 = 0 ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M then z2 * M = {(0. V)} by A7, Th52; hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A9, Th65; ::_thesis: verum end; supposeA10: ( z1 <> 0 & z2 <> 0 ) ; ::_thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M then r1 + r2 > r1 by A4, A6, XREAL_1:29; then r1 / (r1 + r2) < 1 by A5, XREAL_1:189; then ((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M) c= M by A2, A3, A4, A5, A6, A10, Th48; then A11: (z1 + z2) * (((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M)) c= (z1 + z2) * M by Th62; 1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A3, A5, A6, A10, XCMPLX_1:60; then 1 - (r1 / (r1 + r2)) = ((r1 + r2) - r1) / (r1 + r2) ; then A12: (z1 + z2) * ((1r - (z1 / (z1 + z2))) * M) = ((z2 / (z1 + z2)) * (z1 + z2)) * M by A3, A4, Th54 .= z2 * M by A3, A4, A5, A6, A10, XCMPLX_1:87 ; (z1 + z2) * ((z1 / (z1 + z2)) * M) = ((z1 / (z1 + z2)) * (z1 + z2)) * M by Th54 .= z1 * M by A3, A4, A5, A6, A10, XCMPLX_1:87 ; hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A11, A12, Th55; ::_thesis: verum end; end; end; end; end; theorem :: CONVEX4:66 for V being ComplexLinearSpace for M being Subset of V for 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; ::_thesis: for M being Subset of V for 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 let M be Subset of V; ::_thesis: for 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 let z1, z2 be Complex; ::_thesis: ( ex r1, r2 being Real st ( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex implies (z1 * M) + (z2 * M) = (z1 + z2) * M ) assume ( ex r1, r2 being Real st ( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex ) ; ::_thesis: (z1 * M) + (z2 * M) = (z1 + z2) * M hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: (z1 + z2) * M c= (z1 * M) + (z2 * M) thus (z1 + z2) * M c= (z1 * M) + (z2 * M) by Th61; ::_thesis: verum end; theorem :: CONVEX4:67 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct for M1, M2, M3 being Subset of V for 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 non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; ::_thesis: for M1, M2, M3 being Subset of V for z1, z2, z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex let M1, M2, M3 be Subset of V; ::_thesis: for z1, z2, z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex let z1, z2, z3 be Complex; ::_thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex ) assume that A1: ( M1 is convex & M2 is convex ) and A2: M3 is convex ; ::_thesis: ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex (z1 * M1) + (z2 * M2) is convex by A1, Th60; then (1r * ((z1 * M1) + (z2 * M2))) + (z3 * M3) is convex by A2, Th60; hence ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex by Th51; ::_thesis: verum end; theorem Th68: :: CONVEX4:68 for V being non empty CLSStruct for 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 ; ::_thesis: for 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 let F be Subset-Family of V; ::_thesis: ( ( for M being Subset of V st M in F holds M is convex ) implies meet F is convex ) assume A1: for M being Subset of V st M in F holds M is convex ; ::_thesis: meet F is convex percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet F is convex then meet F = {} by SETFAM_1:def_1; hence meet F is convex by Th59; ::_thesis: verum end; supposeA2: F <> {} ; ::_thesis: meet F is convex thus meet F is convex ::_thesis: verum proof let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in meet F & v in meet F holds (z * u) + ((1r - z) * v) in meet F let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in meet F & v in meet F implies (z * u) + ((1r - z) * v) in meet F ) assume that A3: ex r being Real st ( z = r & 0 < r & r < 1 ) and A4: u in meet F and A5: v in meet F ; ::_thesis: (z * u) + ((1r - z) * 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 ; ::_thesis: ( M in F implies (z * u) + ((1r - z) * v) in M ) assume A6: M in F ; ::_thesis: (z * u) + ((1r - z) * v) in M then reconsider M = M as Subset of V ; A7: v in M by A5, A6, SETFAM_1:def_1; ( M is convex & u in M ) by A1, A4, A6, SETFAM_1:def_1; hence (z * u) + ((1r - z) * v) in M by A3, A7, Def23; ::_thesis: verum end; hence (z * u) + ((1r - z) * v) in meet F by A2, SETFAM_1:def_1; ::_thesis: verum end; end; end; end; theorem Th69: :: CONVEX4:69 for V being non empty CLSStruct for M being Subset of V st M is Affine holds M is convex proof let V be non empty CLSStruct ; ::_thesis: for M being Subset of V st M is Affine holds M is convex let M be Subset of V; ::_thesis: ( M is Affine implies M is convex ) assume A1: M is Affine ; ::_thesis: M is convex let u, v be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M holds (z * u) + ((1r - z) * v) in M let z be Complex; ::_thesis: ( ex r being Real st ( z = r & 0 < r & r < 1 ) & u in M & v in M implies (z * u) + ((1r - z) * v) in M ) assume that A2: ex r being Real st ( z = r & 0 < r & r < 1 ) and A3: ( u in M & v in M ) ; ::_thesis: (z * u) + ((1r - z) * v) in M set s = 1r - z; consider r being Real such that A4: z = r and 0 < r and r < 1 by A2; 1r - z = 1 - r by A4; then ((1r - (1r - z)) * u) + ((1r - z) * v) in M by A1, A3, Def20; hence (z * u) + ((1r - z) * v) in M ; ::_thesis: verum end; registration let V be non empty CLSStruct ; cluster non empty convex for Element of bool the carrier of V; existence ex b1 being Subset of V st ( not b1 is empty & b1 is convex ) proof set M = the non empty Affine Subset of V; the non empty Affine Subset of V is convex by Th69; hence ex b1 being Subset of V st ( not b1 is empty & b1 is convex ) ; ::_thesis: verum end; end; registration let V be non empty CLSStruct ; cluster empty convex for Element of bool the carrier of V; existence ex b1 being Subset of V st ( b1 is empty & b1 is convex ) proof {} V is convex by Th59; hence ex b1 being Subset of V st ( b1 is empty & b1 is convex ) ; ::_thesis: verum end; end; theorem :: CONVEX4:70 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) >= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Re (u .|. v) >= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Re (u .|. v) >= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Re (u2 .|. v) >= r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Re (y .|. v)) >= (1 - p) * r by A5, XREAL_1:64; ex u1 being VECTOR of V st ( x = u1 & Re (u1 .|. v) >= r ) by A1, A3; then p * (Re (x .|. v)) >= p * r by A7, XREAL_1:64; then A10: (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) >= (p * r) + ((1 - p) * r) by A9, XREAL_1:7; 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:8 .= (p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v))) by A6, Th42 .= (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) by A6, Th42 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:71 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) > r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) > r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) > r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) > r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Re (u .|. v) > r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Re (u .|. v) > r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Re (u2 .|. v) > r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Re (y .|. v)) > (1 - p) * r by A5, XREAL_1:68; ex u1 being VECTOR of V st ( x = u1 & Re (u1 .|. v) > r ) by A1, A3; then p * (Re (x .|. v)) > p * r by A7, XREAL_1:68; then A10: (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) > (p * r) + ((1 - p) * r) by A9, XREAL_1:8; 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:8 .= (p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v))) by A6, Th42 .= (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) by A6, Th42 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:72 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) <= r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) <= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) <= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) <= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Re (u .|. v) <= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Re (u .|. v) <= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Re (u2 .|. v) <= r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Re (y .|. v)) <= (1 - p) * r by A5, XREAL_1:64; ex u1 being VECTOR of V st ( x = u1 & Re (u1 .|. v) <= r ) by A1, A3; then p * (Re (x .|. v)) <= p * r by A7, XREAL_1:64; then A10: (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) <= (p * r) + ((1 - p) * r) by A9, XREAL_1:7; 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:8 .= (p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v))) by A6, Th42 .= (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) by A6, Th42 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:73 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) < r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) < r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) < r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Re (u .|. v) < r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Re (u .|. v) < r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Re (u .|. v) < r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Re (u2 .|. v) < r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Re (y .|. v)) < (1 - p) * r by A5, XREAL_1:68; ex u1 being VECTOR of V st ( x = u1 & Re (u1 .|. v) < r ) by A1, A3; then p * (Re (x .|. v)) < p * r by A7, XREAL_1:68; then A10: (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) < (p * r) + ((1 - p) * r) by A9, XREAL_1:8; 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:8 .= (p * (Re (x .|. v))) + (Re ((1r - s) * (y .|. v))) by A6, Th42 .= (p * (Re (x .|. v))) + ((1 - p) * (Re (y .|. v))) by A6, Th42 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:74 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) >= r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) >= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) >= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) >= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Im (u .|. v) >= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Im (u .|. v) >= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Im (u2 .|. v) >= r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Im (y .|. v)) >= (1 - p) * r by A5, XREAL_1:64; ex u1 being VECTOR of V st ( x = u1 & Im (u1 .|. v) >= r ) by A1, A3; then p * (Im (x .|. v)) >= p * r by A7, XREAL_1:64; then A10: (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) >= (p * r) + ((1 - p) * r) by A9, XREAL_1:7; 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:8 .= (p * (Im (x .|. v))) + (Im ((1r - s) * (y .|. v))) by A6, Th43 .= (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) by A6, Th43 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:75 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) > r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) > r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) > r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) > r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Im (u .|. v) > r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Im (u .|. v) > r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Im (u2 .|. v) > r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Im (y .|. v)) > (1 - p) * r by A5, XREAL_1:68; ex u1 being VECTOR of V st ( x = u1 & Im (u1 .|. v) > r ) by A1, A3; then p * (Im (x .|. v)) > p * r by A7, XREAL_1:68; then A10: (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) > (p * r) + ((1 - p) * r) by A9, XREAL_1:8; 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:8 .= (p * (Im (x .|. v))) + (Im ((1r - s) * (y .|. v))) by A6, Th43 .= (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) by A6, Th43 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:76 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) <= r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) <= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) <= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) <= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Im (u .|. v) <= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Im (u .|. v) <= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Im (u2 .|. v) <= r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Im (y .|. v)) <= (1 - p) * r by A5, XREAL_1:64; ex u1 being VECTOR of V st ( x = u1 & Im (u1 .|. v) <= r ) by A1, A3; then p * (Im (x .|. v)) <= p * r by A7, XREAL_1:64; then A10: (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) <= (p * r) + ((1 - p) * r) by A9, XREAL_1:7; 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:8 .= (p * (Im (x .|. v))) + (Im ((1r - s) * (y .|. v))) by A6, Th43 .= (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) by A6, Th43 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:77 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) < r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) < r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) < r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) < r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : Im (u .|. v) < r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : Im (u .|. v) < r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M A5: ex u2 being VECTOR of V st ( y = u2 & Im (u2 .|. v) < r ) by A1, A4; consider p being Real such that A6: s = p and A7: 0 < p and A8: p < 1 by A2; 1 - p > 0 by A8, XREAL_1:50; then A9: (1 - p) * (Im (y .|. v)) < (1 - p) * r by A5, XREAL_1:68; ex u1 being VECTOR of V st ( x = u1 & Im (u1 .|. v) < r ) by A1, A3; then p * (Im (x .|. v)) < p * r by A7, XREAL_1:68; then A10: (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) < (p * r) + ((1 - p) * r) by A9, XREAL_1:8; 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:8 .= (p * (Im (x .|. v))) + (Im ((1r - s) * (y .|. v))) by A6, Th43 .= (p * (Im (x .|. v))) + ((1 - p) * (Im (y .|. v))) by A6, Th43 ; hence (s * x) + ((1r - s) * y) in M by A1, A10; ::_thesis: verum end; theorem :: CONVEX4:78 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| <= r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| <= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| <= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| <= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : |.(u .|. v).| <= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : |.(u .|. v).| <= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M consider p being Real such that A5: s = p and A6: 0 < p and A7: p < 1 by A2; A8: 1 - p > 0 by A7, XREAL_1:50; ex u2 being VECTOR of V st ( y = u2 & |.(u2 .|. v).| <= r ) by A1, A4; then A9: (1 - p) * |.(y .|. v).| <= (1 - p) * r by A8, XREAL_1:64; ex u1 being VECTOR of V st ( x = u1 & |.(u1 .|. v).| <= r ) by A1, A3; then p * |.(x .|. v).| <= p * r by A6, XREAL_1:64; then A10: (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) <= (p * r) + ((1 - p) * r) by A9, XREAL_1:7; ( |.(s * (x .|. v)).| = p * |.(x .|. v).| & |.((1r - s) * (y .|. v)).| = (1 - p) * |.(y .|. v).| ) by A5, A6, A7, Th44; then A11: |.((s * (x .|. v)) + ((1r - s) * (y .|. v))).| <= (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) by COMPLEX1:56; |.(((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 ; then |.(((s * x) + ((1r - s) * y)) .|. v).| <= r by A11, A10, XXREAL_0:2; hence (s * x) + ((1r - s) * y) in M by A1; ::_thesis: verum end; theorem :: CONVEX4:79 for V being non empty ComplexUnitarySpace-like CUNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| < r } holds M is convex proof let V be non empty ComplexUnitarySpace-like CUNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| < r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| < r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : |.(u .|. v).| < r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : |.(u .|. v).| < r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : |.(u .|. v).| < r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX4:def_23 ::_thesis: for z being Complex st ex r being Real st ( z = r & 0 < r & r < 1 ) & x in M & y in M holds (z * x) + ((1r - z) * y) in M let s be Complex; ::_thesis: ( ex r being Real st ( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M ) assume that A2: ex p being Real st ( s = p & 0 < p & p < 1 ) and A3: x in M and A4: y in M ; ::_thesis: (s * x) + ((1r - s) * y) in M consider p being Real such that A5: s = p and A6: 0 < p and A7: p < 1 by A2; A8: 1 - p > 0 by A7, XREAL_1:50; ex u2 being VECTOR of V st ( y = u2 & |.(u2 .|. v).| < r ) by A1, A4; then A9: (1 - p) * |.(y .|. v).| < (1 - p) * r by A8, XREAL_1:68; ex u1 being VECTOR of V st ( x = u1 & |.(u1 .|. v).| < r ) by A1, A3; then p * |.(x .|. v).| < p * r by A6, XREAL_1:68; then A10: (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) < (p * r) + ((1 - p) * r) by A9, XREAL_1:8; ( |.(s * (x .|. v)).| = p * |.(x .|. v).| & |.((1r - s) * (y .|. v)).| = (1 - p) * |.(y .|. v).| ) by A5, A6, A7, Th44; then A11: |.((s * (x .|. v)) + ((1r - s) * (y .|. v))).| <= (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) by COMPLEX1:56; |.(((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 ; then |.(((s * x) + ((1r - s) * y)) .|. v).| < r by A11, A10, XXREAL_0:2; hence (s * x) + ((1r - s) * y) in M by A1; ::_thesis: verum end; begin definition let V be ComplexLinearSpace; let L be C_Linear_Combination of V; attrL is convex means :Def24: :: CONVEX4:def 24 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; :: deftheorem Def24 defines convex CONVEX4:def_24_:_ for V being ComplexLinearSpace for L being C_Linear_Combination of V holds ( L is convex iff 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 ) ) ) ) ); theorem Th80: :: CONVEX4:80 for V being ComplexLinearSpace for L being C_Linear_Combination of V st L is convex holds Carrier L <> {} proof let V be ComplexLinearSpace; ::_thesis: for L being C_Linear_Combination of V st L is convex holds Carrier L <> {} let L be C_Linear_Combination of V; ::_thesis: ( L is convex implies Carrier L <> {} ) assume L is convex ; ::_thesis: Carrier L <> {} then consider F being FinSequence of the carrier of V such that A1: ( F is one-to-one & rng F = Carrier L ) and A2: 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 Def24; consider f being FinSequence of REAL such that A3: ( 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 A2; assume Carrier L = {} ; ::_thesis: contradiction then len F = 0 by A1, CARD_1:27, FINSEQ_4:62; then f = <*> the carrier of V by A3; hence contradiction by A3, RVSUM_1:72; ::_thesis: verum end; theorem :: CONVEX4:81 for V being ComplexLinearSpace for L being C_Linear_Combination of V for 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; ::_thesis: for L being C_Linear_Combination of V for 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 let L be C_Linear_Combination of V; ::_thesis: for 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 let v be VECTOR of V; ::_thesis: ( L is convex & ex r being Real st ( r = L . v & r <= 0 ) implies not v in Carrier L ) assume that A1: L is convex and A2: ex r being Real st ( r = L . v & r <= 0 ) ; ::_thesis: not v in Carrier L consider r being Real such that A3: r = L . v and A4: r <= 0 by A2; percases ( r = 0 or r < 0 ) by A4; suppose r = 0 ; ::_thesis: not v in Carrier L hence not v in Carrier L by A3, Th1; ::_thesis: verum end; supposeA5: r < 0 ; ::_thesis: not v in Carrier L now__::_thesis:_not_v_in_Carrier_L consider F being FinSequence of the carrier of V such that F is one-to-one and A6: rng F = Carrier L and A7: 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, Def24; assume v in Carrier L ; ::_thesis: contradiction then consider n being set such that A8: n in dom F and A9: F . n = v by A6, FUNCT_1:def_3; reconsider n = n as Element of NAT by A8; consider f being FinSequence of REAL such that A10: len f = len F and Sum f = 1 and A11: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A7; n in Seg (len F) by A8, FINSEQ_1:def_3; then A12: n in dom f by A10, FINSEQ_1:def_3; then L . v = f . n by A11, A9; hence contradiction by A3, A5, A11, A12; ::_thesis: verum end; hence not v in Carrier L ; ::_thesis: verum end; end; end; theorem :: CONVEX4:82 for V being ComplexLinearSpace for L being C_Linear_Combination of V st L is convex holds L <> ZeroCLC V proof let V be ComplexLinearSpace; ::_thesis: for L being C_Linear_Combination of V st L is convex holds L <> ZeroCLC V let L be C_Linear_Combination of V; ::_thesis: ( L is convex implies L <> ZeroCLC V ) assume L is convex ; ::_thesis: L <> ZeroCLC V then A1: Carrier L <> {} by Th80; assume L = ZeroCLC V ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; theorem Th83: :: CONVEX4:83 for V being ComplexLinearSpace for v being VECTOR of V for 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; ::_thesis: for v being VECTOR of V for 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 ) let v be VECTOR of V; ::_thesis: for 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 ) let L be C_Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v} implies ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) ) assume that A1: L is convex and A2: Carrier L = {v} ; ::_thesis: ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) reconsider L = L as C_Linear_Combination of {v} by A2, Def4; consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and A4: 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, Def24; A5: F = <*v*> by A2, A3, FINSEQ_3:97; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A4; reconsider r = f /. 1 as Element of REAL ; card (Carrier L) = 1 by A2, CARD_1:30; then len F = 1 by A3, FINSEQ_4:62; then A9: dom f = Seg 1 by A6, FINSEQ_1:def_3; then A10: 1 in dom f ; then A11: f . 1 = f /. 1 by PARTFUN1:def_6; then A12: f = <*r*> by A9, FINSEQ_1:def_8; f . 1 = L . (F . 1) by A8, A10; then r = L . v by A11, A5, FINSEQ_1:def_8; hence ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) by A7, A12, Th14, FINSOP_1:11; ::_thesis: verum end; theorem Th84: :: CONVEX4:84 for V being ComplexLinearSpace for v1, v2 being VECTOR of V for 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; ::_thesis: for v1, v2 being VECTOR of V for 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) ) let v1, v2 be VECTOR of V; ::_thesis: for 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) ) let L be C_Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2} & v1 <> v2 implies ( 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) ) ) assume that A1: L is convex and A2: Carrier L = {v1,v2} and A3: v1 <> v2 ; ::_thesis: ( 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) ) reconsider L = L as C_Linear_Combination of {v1,v2} by A2, Def4; consider F being FinSequence of the carrier of V such that A4: ( F is one-to-one & rng F = Carrier L ) and A5: 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, Def24; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A5; len F = card {v1,v2} by A2, A4, FINSEQ_4:62; then A9: len f = 2 by A3, A6, CARD_2:57; then A10: dom f = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; then A11: 2 in dom f by TARSKI:def_2; then A12: f . 2 = L . (F . 2) by A8; then f /. 2 = L . (F . 2) by A11, PARTFUN1:def_6; then reconsider r2 = L . (F . 2) as Real ; A13: f . 2 >= 0 by A8, A11; A14: 1 in dom f by A10, TARSKI:def_2; then A15: f . 1 = L . (F . 1) by A8; then f /. 1 = L . (F . 1) by A14, PARTFUN1:def_6; then reconsider r1 = L . (F . 1) as Real ; A16: f = <*r1,r2*> by A9, A15, A12, FINSEQ_1:44; ex c1, c2 being Real st ( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) proof percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99; suppose F = <*v1,v2*> ; ::_thesis: ex c1, c2 being Real st ( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) then A17: ( r1 = L . v1 & r2 = L . v2 ) by FINSEQ_1:44; ( r1 + r2 = 1 & r1 >= 0 ) by A7, A8, A14, A15, A16, RVSUM_1:77; hence ex c1, c2 being Real st ( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) by A12, A13, A17; ::_thesis: verum end; suppose F = <*v2,v1*> ; ::_thesis: ex c1, c2 being Real st ( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) then A18: ( r1 = L . v2 & r2 = L . v1 ) by FINSEQ_1:44; ( r1 + r2 = 1 & r1 >= 0 ) by A7, A8, A14, A15, A16, RVSUM_1:77; hence ex c1, c2 being Real st ( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) by A12, A13, A18; ::_thesis: verum end; end; end; hence ( 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) ) by A3, Th15; ::_thesis: verum end; Lm3: for V being ComplexLinearSpace for v1, v2, v3 being VECTOR of V for 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; ::_thesis: for v1, v2, v3 being VECTOR of V for 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) let v1, v2, v3 be VECTOR of V; ::_thesis: for 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) let L be C_Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 implies Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) assume that A1: v1 <> v2 and A2: v2 <> v3 and A3: v3 <> v1 ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) A4: Carrier L c= {v1,v2,v3} by Def4; percases ( Carrier L = {} or Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v1,v3} or Carrier L = {v2,v3} or Carrier L = {v1,v2,v3} ) by A4, ZFMISC_1:118; suppose Carrier L = {} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A5: L = ZeroCLC V by Def3; then Sum L = 0. V by Th11 .= (0. V) + (0. V) by RLVECT_1:4 .= ((0. V) + (0. V)) + (0. V) by RLVECT_1:4 .= ((0c * v1) + (0. V)) + (0. V) by CLVECT_1:1 .= ((0c * v1) + (0c * v2)) + (0. V) by CLVECT_1:1 .= ((0c * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:1 .= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by A5, Th2 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A5, Th2 .= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A5, Th2 ; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA6: Carrier L = {v1} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = L as C_Linear_Combination of {v1} by Def4; A7: not v2 in Carrier L by A1, A6, TARSKI:def_1; A8: not v3 in Carrier L by A3, A6, TARSKI:def_1; Sum L = (L . v1) * v1 by Th14 .= ((L . v1) * v1) + (0. V) by RLVECT_1:4 .= (((L . v1) * v1) + (0. V)) + (0. V) by RLVECT_1:4 .= (((L . v1) * v1) + (0c * v2)) + (0. V) by CLVECT_1:1 .= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:1 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A7 .= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A8 ; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA9: Carrier L = {v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = L as C_Linear_Combination of {v2} by Def4; A10: not v1 in Carrier L by A1, A9, TARSKI:def_1; A11: not v3 in Carrier L by A2, A9, TARSKI:def_1; Sum L = (L . v2) * v2 by Th14 .= (0. V) + ((L . v2) * v2) by RLVECT_1:4 .= ((0. V) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4 .= ((0c * v1) + ((L . v2) * v2)) + (0. V) by CLVECT_1:1 .= ((0c * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:1 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A10 .= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A11 ; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA12: Carrier L = {v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = L as C_Linear_Combination of {v3} by Def4; A13: not v1 in Carrier L by A3, A12, TARSKI:def_1; A14: not v2 in Carrier L by A2, A12, TARSKI:def_1; Sum L = (L . v3) * v3 by Th14 .= (0. V) + ((L . v3) * v3) by RLVECT_1:4 .= ((0. V) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4 .= ((0c * v1) + (0. V)) + ((L . v3) * v3) by CLVECT_1:1 .= ((0c * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:1 .= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by A13 .= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A14 ; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA15: Carrier L = {v1,v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A16: Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A1, Th18 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:1 ; not v3 in Carrier L by A2, A3, A15, TARSKI:def_2; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A16; ::_thesis: verum end; supposeA17: Carrier L = {v1,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A18: Sum L = ((L . v1) * v1) + ((L . v3) * v3) by A3, Th18 .= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4 .= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:1 ; not v2 in Carrier L by A1, A2, A17, TARSKI:def_2; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A18; ::_thesis: verum end; supposeA19: Carrier L = {v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A20: Sum L = ((L . v2) * v2) + ((L . v3) * v3) by A2, Th18 .= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:4 .= ((0c * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by CLVECT_1:1 ; not v1 in Carrier L by A1, A3, A19, TARSKI:def_2; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A20; ::_thesis: verum end; suppose Carrier L = {v1,v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then consider F being FinSequence of the carrier of V such that A21: ( F is one-to-one & rng F = {v1,v2,v3} ) and A22: Sum L = Sum (L (#) F) by Def6; ( 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, A2, A3, A21, 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 Th10; 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 A22, RLVECT_1:46; hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def_3; ::_thesis: verum end; end; end; theorem Th85: :: CONVEX4:85 for V being ComplexLinearSpace for v1, v2, v3 being VECTOR of V for 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; ::_thesis: for v1, v2, v3 being VECTOR of V for 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) ) let v1, v2, v3 be VECTOR of V; ::_thesis: for 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) ) let L be C_Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( 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) ) ) assume that A1: L is convex and A2: Carrier L = {v1,v2,v3} and A3: ( v1 <> v2 & v2 <> v3 & v3 <> v1 ) ; ::_thesis: ( 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) ) reconsider L = L as C_Linear_Combination of {v1,v2,v3} by A2, Def4; consider F being FinSequence of the carrier of V such that A4: ( F is one-to-one & rng F = Carrier L ) and A5: 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, Def24; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A5; len F = card {v1,v2,v3} by A2, A4, FINSEQ_4:62; then A9: len f = 3 by A3, A6, CARD_2:58; then A10: dom f = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1; then A11: 2 in dom f by ENUMSET1:def_1; then A12: f . 2 = L . (F . 2) by A8; then f /. 2 = L . (F . 2) by A11, PARTFUN1:def_6; then reconsider r2 = L . (F . 2) as Element of REAL ; A13: f . 2 >= 0 by A8, A11; A14: 3 in dom f by A10, ENUMSET1:def_1; then A15: f . 3 = L . (F . 3) by A8; then f /. 3 = L . (F . 3) by A14, PARTFUN1:def_6; then reconsider r3 = L . (F . 3) as Element of REAL ; A16: f . 3 >= 0 by A8, A14; A17: 1 in dom f by A10, ENUMSET1:def_1; then A18: f . 1 = L . (F . 1) by A8; then f /. 1 = L . (F . 1) by A17, PARTFUN1:def_6; then reconsider r1 = L . (F . 1) as Element of REAL ; A19: f = <*r1,r2,r3*> by A9, A18, A12, A15, FINSEQ_1:45; then A20: (r1 + r2) + r3 = 1 by A7, RVSUM_1:78; A21: f . 1 >= 0 by A8, A17; 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 percases ( 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 A2, A3, A4, CONVEX1:31; supposeA22: F = <*v1,v2,v3*> ; ::_thesis: 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 ) then A23: ( r1 = L . v1 & r2 = L . v2 ) by FINSEQ_1:45; A24: r2 >= 0 by A8, A11, A12; A25: r3 = L . v3 by A22, FINSEQ_1:45; ( (r1 + r2) + r3 = 1 & r1 >= 0 ) by A7, A8, A17, A18, A19, RVSUM_1:78; hence 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 ) by A15, A16, A23, A25, A24; ::_thesis: verum end; supposeA26: F = <*v1,v3,v2*> ; ::_thesis: 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 ) then A27: ( r1 = L . v1 & r3 = L . v2 ) by FINSEQ_1:45; A28: r3 >= 0 by A8, A14, A15; A29: r2 = L . v3 by A26, FINSEQ_1:45; ( (r1 + r3) + r2 = 1 & r1 >= 0 ) by A8, A17, A18, A20; hence 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 ) by A12, A13, A27, A29, A28; ::_thesis: verum end; supposeA30: F = <*v2,v1,v3*> ; ::_thesis: 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 ) then A31: ( r2 = L . v1 & r1 = L . v2 ) by FINSEQ_1:45; A32: r1 >= 0 by A8, A17, A18; A33: r3 = L . v3 by A30, FINSEQ_1:45; ( (r2 + r1) + r3 = 1 & r2 >= 0 ) by A7, A8, A11, A12, A19, RVSUM_1:78; hence 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 ) by A15, A16, A31, A33, A32; ::_thesis: verum end; supposeA34: F = <*v2,v3,v1*> ; ::_thesis: 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 ) then A35: ( r3 = L . v1 & r1 = L . v2 ) by FINSEQ_1:45; A36: r1 >= 0 by A8, A17, A18; A37: r2 = L . v3 by A34, FINSEQ_1:45; ( (r3 + r1) + r2 = 1 & r3 >= 0 ) by A8, A14, A15, A20; hence 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 ) by A12, A13, A35, A37, A36; ::_thesis: verum end; supposeA38: F = <*v3,v1,v2*> ; ::_thesis: 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 ) then A39: ( r2 = L . v1 & r3 = L . v2 ) by FINSEQ_1:45; A40: r3 >= 0 by A8, A14, A15; A41: r1 = L . v3 by A38, FINSEQ_1:45; ( (r2 + r3) + r1 = 1 & r2 >= 0 ) by A8, A11, A12, A20; hence 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 ) by A18, A21, A39, A41, A40; ::_thesis: verum end; supposeA42: F = <*v3,v2,v1*> ; ::_thesis: 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 ) then A43: ( r3 = L . v1 & r2 = L . v2 ) by FINSEQ_1:45; A44: r2 >= 0 by A8, A11, A12; A45: r1 = L . v3 by A42, FINSEQ_1:45; ( (r3 + r2) + r1 = 1 & r3 >= 0 ) by A8, A14, A15, A20; hence 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 ) by A18, A21, A43, A45, A44; ::_thesis: verum end; end; end; hence ( 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) ) by A3, Lm3; ::_thesis: verum end; theorem :: CONVEX4:86 for V being ComplexLinearSpace for v being VECTOR of V for 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; ::_thesis: for v being VECTOR of V for 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 ) let v be VECTOR of V; ::_thesis: for 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 ) let L be C_Linear_Combination of {v}; ::_thesis: ( L is convex implies ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) ) Carrier L c= {v} by Def4; then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33; assume L is convex ; ::_thesis: ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) hence ( ex r being Real st ( r = L . v & r = 1 ) & Sum L = (L . v) * v ) by A1, Th80, Th83; ::_thesis: verum end; theorem :: CONVEX4:87 for V being ComplexLinearSpace for v1, v2 being VECTOR of V for 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; ::_thesis: for v1, v2 being VECTOR of V for 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) ) let v1, v2 be VECTOR of V; ::_thesis: for 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) ) let L be C_Linear_Combination of {v1,v2}; ::_thesis: ( v1 <> v2 & L is convex implies ( 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) ) ) assume that A1: v1 <> v2 and A2: L is convex ; ::_thesis: ( 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) ) A3: Carrier L c= {v1,v2} by Def4; A4: Carrier L <> {} by A2, Th80; ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) proof percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v1,v2} ) by A3, A4, ZFMISC_1:36; supposeA5: Carrier L = {v1} ; ::_thesis: ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) then not v2 in Carrier L by A1, TARSKI:def_1; then A6: 0 = L . v2 ; ex r being Real st ( r = L . v1 & r = 1 ) by A2, A5, Th83; hence ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) by A6; ::_thesis: verum end; supposeA7: Carrier L = {v2} ; ::_thesis: ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) then not v1 in Carrier L by A1, TARSKI:def_1; then A8: 0 = L . v1 ; ex r being Real st ( r = L . v2 & r = 1 ) by A2, A7, Th83; hence ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) by A8; ::_thesis: verum end; suppose Carrier L = {v1,v2} ; ::_thesis: ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) then ex r1, r2 being Real st ( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) by A1, A2, Th84; hence ex r1, r2 being real number st ( r1 = L . v1 & r2 = L . v2 & r1 >= 0 & r2 >= 0 ) ; ::_thesis: verum end; end; end; hence ( 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) ) by A1, Th15; ::_thesis: verum end; theorem :: CONVEX4:88 for V being ComplexLinearSpace for v1, v2, v3 being VECTOR of V for 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; ::_thesis: for v1, v2, v3 being VECTOR of V for 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) ) let v1, v2, v3 be VECTOR of V; ::_thesis: for 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) ) let L be C_Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex implies ( 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) ) ) assume that A1: v1 <> v2 and A2: v2 <> v3 and A3: v3 <> v1 and A4: L is convex ; ::_thesis: ( 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) ) A5: Carrier L c= {v1,v2,v3} by Def4; A6: Carrier L <> {} by A4, Th80; 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 percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v2,v3} or Carrier L = {v1,v3} or Carrier L = {v1,v2,v3} ) by A5, A6, ZFMISC_1:118; supposeA7: Carrier L = {v1} ; ::_thesis: 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 ) then not v2 in Carrier L by A1, TARSKI:def_1; then A8: 0 = L . v2 ; A9: (1 + 0) + 0 = 1 ; not v3 in Carrier L by A3, A7, TARSKI:def_1; then A10: 0 = L . v3 ; ex r being Real st ( r = L . v1 & r = 1 ) by A4, A7, Th83; hence 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 ) by A8, A10, A9; ::_thesis: verum end; supposeA11: Carrier L = {v2} ; ::_thesis: 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 ) then not v1 in Carrier L by A1, TARSKI:def_1; then A12: 0 = L . v1 ; A13: (0 + 1) + 0 = 1 ; not v3 in Carrier L by A2, A11, TARSKI:def_1; then A14: 0 = L . v3 ; ex r being Real st ( r = L . v2 & r = 1 ) by A4, A11, Th83; hence 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 ) by A12, A14, A13; ::_thesis: verum end; supposeA15: Carrier L = {v3} ; ::_thesis: 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 ) then not v1 in Carrier L by A3, TARSKI:def_1; then A16: 0 = L . v1 ; A17: (0 + 0) + 1 = 1 ; not v2 in Carrier L by A2, A15, TARSKI:def_1; then A18: 0 = L . v2 ; ex r being Real st ( r = L . v3 & r = 1 ) by A4, A15, Th83; hence 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 ) by A16, A18, A17; ::_thesis: verum end; supposeA19: Carrier L = {v1,v2} ; ::_thesis: 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 ) set r3 = 0 ; not v3 in { v where v is Element of V : L . v <> 0 } by A2, A3, A19, TARSKI:def_2; then A20: 0 = L . v3 ; consider r1, r2 being Real such that A21: ( r1 = L . v1 & r2 = L . v2 ) and A22: r1 + r2 = 1 and A23: ( r1 >= 0 & r2 >= 0 ) by A1, A4, A19, Th84; (r1 + r2) + 0 = 1 by A22; hence 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 ) by A21, A23, A20; ::_thesis: verum end; supposeA24: Carrier L = {v2,v3} ; ::_thesis: 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 ) set r1 = 0 ; not v1 in Carrier L by A1, A3, A24, TARSKI:def_2; then A25: 0 = L . v1 ; consider r2, r3 being Real such that A26: ( r2 = L . v2 & r3 = L . v3 ) and A27: r2 + r3 = 1 and A28: ( r2 >= 0 & r3 >= 0 ) by A2, A4, A24, Th84; (0 + r2) + r3 = 1 by A27; hence 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 ) by A26, A28, A25; ::_thesis: verum end; supposeA29: Carrier L = {v1,v3} ; ::_thesis: 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 ) set r2 = 0 ; not v2 in Carrier L by A1, A2, A29, TARSKI:def_2; then A30: 0 = L . v2 ; consider r1, r3 being Real such that A31: ( r1 = L . v1 & r3 = L . v3 ) and A32: r1 + r3 = 1 and A33: ( r1 >= 0 & r3 >= 0 ) by A3, A4, A29, Th84; (r1 + 0) + r3 = 1 by A32; hence 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 ) by A31, A33, A30; ::_thesis: verum end; suppose Carrier L = {v1,v2,v3} ; ::_thesis: 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 ) hence 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 ) by A1, A2, A3, A4, Th85; ::_thesis: verum end; end; end; hence ( 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) ) by A1, A2, A3, Lm3; ::_thesis: verum end; begin definition let V be non empty CLSStruct ; let M be Subset of V; func Convex-Family M -> Subset-Family of V means :Def25: :: CONVEX4:def 25 for N being Subset of V holds ( N in it iff ( N is convex & M c= N ) ); existence ex b1 being Subset-Family of V st for N being Subset of V holds ( N in b1 iff ( N is convex & M c= N ) ) proof defpred S1[ Subset of V] means ( $1 is convex & M c= $1 ); thus ex F being Subset-Family of V st for N being Subset of V holds ( N in F iff S1[N] ) from SUBSET_1:sch_3(); ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of V st ( for N being Subset of V holds ( N in b1 iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds ( N in b2 iff ( N is convex & M c= N ) ) ) holds b1 = b2 proof let SF, SG be Subset-Family of V; ::_thesis: ( ( for N being Subset of V holds ( N in SF iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds ( N in SG iff ( N is convex & M c= N ) ) ) implies SF = SG ) 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 ) ) ; ::_thesis: SF = SG for Y being Subset of V holds ( Y in SF iff Y in SG ) proof let Y be Subset of V; ::_thesis: ( Y in SF iff Y in SG ) hereby ::_thesis: ( Y in SG implies Y in SF ) assume Y in SF ; ::_thesis: Y in SG then ( Y is convex & M c= Y ) by A1; hence Y in SG by A2; ::_thesis: verum end; assume Y in SG ; ::_thesis: Y in SF then ( Y is convex & M c= Y ) by A2; hence Y in SF by A1; ::_thesis: verum end; hence SF = SG by SETFAM_1:31; ::_thesis: verum end; end; :: deftheorem Def25 defines Convex-Family CONVEX4:def_25_:_ for V being non empty CLSStruct for M being Subset of V for b3 being Subset-Family of V holds ( b3 = Convex-Family M iff for N being Subset of V holds ( N in b3 iff ( N is convex & M c= N ) ) ); definition let V be non empty CLSStruct ; let M be Subset of V; func conv M -> convex Subset of V equals :: CONVEX4:def 26 meet (Convex-Family M); coherence meet (Convex-Family M) is convex Subset of V proof for N being Subset of V st N in Convex-Family M holds N is convex by Def25; hence meet (Convex-Family M) is convex Subset of V by Th68; ::_thesis: verum end; end; :: deftheorem defines conv CONVEX4:def_26_:_ for V being non empty CLSStruct for M being Subset of V holds conv M = meet (Convex-Family M); theorem :: CONVEX4:89 for V being non empty CLSStruct for M being Subset of V for N being convex Subset of V st M c= N holds conv M c= N proof let V be non empty CLSStruct ; ::_thesis: for M being Subset of V for N being convex Subset of V st M c= N holds conv M c= N let M be Subset of V; ::_thesis: for N being convex Subset of V st M c= N holds conv M c= N let N be convex Subset of V; ::_thesis: ( M c= N implies conv M c= N ) assume M c= N ; ::_thesis: conv M c= N then N in Convex-Family M by Def25; hence conv M c= N by SETFAM_1:3; ::_thesis: verum end;