:: CONVEX4 semantic presentation

definition
let V be non empty ZeroStr ;
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 end;
end;

:: deftheorem Def1 defines C_Linear_Combination CONVEX4:def 1 :
for V being non empty ZeroStr
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 );

definition
let V be non empty addLoopStr ;
let L be Element of Funcs the carrier of V,COMPLEX ;
func Carrier L -> Subset of V equals :: CONVEX4:def 2
{ v where v is Element of V : L . v <> 0c } ;
coherence
{ v where v is Element of V : L . v <> 0c } is Subset of V
proof 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 L -> finite ;
coherence
Carrier L is finite
proof 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 end;

definition
let V be non empty addLoopStr ;
func ZeroCLC V -> C_Linear_Combination of V means :Def2: :: CONVEX4:def 3
 Carrier it = {} ;
existence
ex b1 being C_Linear_Combination of V st Carrier b1 = {}
proof end;
uniqueness
for b1, b2 being C_Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds
b1 = b2
proof end;
end;

:: deftheorem Def2 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 (ZeroCLC V) -> empty ;
coherence
Carrier (ZeroCLC V) is empty by Def2;
end;

theorem Th30: :: CONVEX4:2
for V being non empty addLoopStr
for v being Element of V holds (ZeroCLC V) . v = 0c
proof end;

definition
let V be non empty addLoopStr ;
let A be Subset of V;
mode C_Linear_Combination of A -> C_Linear_Combination of V means :Def3: :: CONVEX4:def 4
 Carrier it c= A;
existence
ex b1 being C_Linear_Combination of V st Carrier b1 c= A
proof end;
end;

:: deftheorem Def3 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 end;

theorem Th34: :: CONVEX4:4
for V being non empty addLoopStr
for A being Subset of V holds ZeroCLC V is C_Linear_Combination of A
proof end;

theorem Th35: :: CONVEX4:5
for V being non empty addLoopStr
for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V
proof 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 ;
func f (#) F -> FinSequence of the carrier of V means :Def4: :: 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 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 end;
end;

:: deftheorem Def4 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 Th40: :: 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 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 end;

theorem Th42: :: 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 end;

theorem Th43: :: 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 end;

theorem Th44: :: 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 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 :Def5: :: 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 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 end;
end;

:: deftheorem Def5 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 Lm2: :: CONVEX4:11
for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct holds Sum (ZeroCLC V) = 0. V
proof 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 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 end;

theorem Th50: :: 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 end;

theorem Th51: :: 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 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 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 end;

theorem Th54: :: 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 end;

definition
let V be non empty addLoopStr ;
let L1, L2 be C_Linear_Combination of V;
:: original: =
redefine pred L1 = 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:113;
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 func L1 + L2 -> C_Linear_Combination of V means :Def6: :: 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 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 end;
end;

:: deftheorem Def6 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 Th58: :: 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 end;

theorem Th59: :: 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 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 func L1 + L2 -> C_Linear_Combination of A;
coherence
L1 + L2 is C_Linear_Combination of A by Th59;
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 Th61: :: 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 end;

theorem Th62: :: CONVEX4:23
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds L + (ZeroCLC V) = L
proof end;

definition
let V be non empty CLSStruct ;
let a be Complex;
let L be C_Linear_Combination of V;
func a * L -> C_Linear_Combination of V means :Def7: :: 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 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 end;
end;

:: deftheorem Def7 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 Th65: :: 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 end;

theorem Th66: :: CONVEX4:25
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds 0c * L = ZeroCLC V
proof end;

theorem Th67: :: 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 end;

theorem Th68: :: 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 end;

theorem Th69: :: 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 end;

theorem Th70: :: 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 end;

theorem Th71: :: CONVEX4:30
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds 1r * L = L
proof 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 Th73: :: 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 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 end;

theorem :: CONVEX4:33
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds - (- L) = L
proof end;

definition
let V be non empty CLSStruct ;
let L1, L2 be C_Linear_Combination of V;
func L1 - 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 Th79: :: 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 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 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 end;

theorem Th82: :: CONVEX4:37
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds L - L = ZeroCLC V
proof end;

definition
let V be non empty CLSStruct ;
func C_LinComb V -> set means :Def8: :: 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 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 end;
end;

:: deftheorem Def8 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 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 Def8;
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 Def8;
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 :Def9: :: 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 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 end;
end;

:: deftheorem Def9 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