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