:: CLVECT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
attr c1 is strict;
struct CLSStruct -> LoopStr ;
aggr CLSStruct(# carrier, Zero, add, Mult #) -> CLSStruct ;
sel Mult c1 -> Function of [:COMPLEX ,the carrier of c1:],the carrier of c1;
end;

registration
cluster non empty CLSStruct ;
existence
not for b1 being CLSStruct holds b1 is empty
proof end;
end;

definition
let V be CLSStruct ;
mode VECTOR of V is Element of V;
end;

definition
let V be non empty CLSStruct ;
let v be VECTOR of V;
let z be Complex;
func z * v -> Element of V equals :: CLVECT_1:def 1
the Mult of V . [z,v];
coherence
the Mult of V . [z,v] is Element of V
;
end;

:: deftheorem defines * CLVECT_1:def 1 :
for V being non empty CLSStruct
for v being VECTOR of V
for z being Complex holds z * v = the Mult of V . [z,v];

registration
let ZS be non empty set ;
let O be Element of ZS;
let F be BinOp of ZS;
let G be Function of [:COMPLEX ,ZS:],ZS;
cluster CLSStruct(# ZS,O,F,G #) -> non empty ;
coherence
not CLSStruct(# ZS,O,F,G #) is empty
by STRUCT_0:def 1;
end;

Lm1: now
take ZS = {0}; :: thesis: ex O being Element of ZS ex F being BinOp of ZS ex G being Function of [:COMPLEX ,ZS:],ZS st
( ( for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x ) & ( for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )

reconsider O = 0 as Element of ZS by TARSKI:def 1;
take O = O; :: thesis: ex F being BinOp of ZS ex G being Function of [:COMPLEX ,ZS:],ZS st
( ( for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x ) & ( for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )

deffunc H1( Element of ZS, Element of ZS) -> Element of ZS = O;
consider F being BinOp of ZS such that
A1: for x, y being Element of ZS holds F . x,y = H1(x,y) from BINOP_1:sch 2( V );
reconsider G = [:COMPLEX ,ZS:] --> O as Function of [:COMPLEX ,ZS:],ZS by FUNCOP_1:57;
A2: for a being Element of COMPLEX
for x being Element of ZS holds G . [a,x] = O
proof
let a be Element of COMPLEX ; :: thesis: for x being Element of ZS holds G . [a,x] = O
let x be Element of ZS; :: thesis: G . [a,x] = O
[a,x] in [:COMPLEX ,ZS:] ;
hence G . [a,x] = O by FUNCOP_1:13; :: thesis: verum
end;
take F = F; :: thesis: ex G being Function of [:COMPLEX ,ZS:],ZS st
( ( for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x ) & ( for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )

take G = G; :: thesis: ( ( for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x ) & ( for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )

set W = CLSStruct(# ZS,O,F,G #);
thus for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x :: thesis: ( ( for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let x, y be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: x + y = y + x
A3: ( x + y = F . x,y & y + x = F . y,x ) ;
reconsider X = x, Y = y as Element of ZS ;
( x + y = H1(X,Y) & y + x = H1(Y,X) ) by A1, A3;
hence x + y = y + x ; :: thesis: verum
end;
thus for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) :: thesis: ( ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let x, y, z be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: (x + y) + z = x + (y + z)
A4: ( (x + y) + z = F . (x + y),z & x + (y + z) = F . x,(y + z) ) ;
reconsider X = x, Y = y, Z = z as Element of ZS ;
( (x + y) + z = H1(H1(X,Y),Z) & x + (y + z) = H1(X,H1(Y,Z)) ) by A1, A4;
hence (x + y) + z = x + (y + z) ; :: thesis: verum
end;
thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x :: thesis: ( ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) ) & ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: x + (0. CLSStruct(# ZS,O,F,G #)) = x
reconsider X = x as Element of ZS ;
x + (0. CLSStruct(# ZS,O,F,G #)) = F . [x,(0. CLSStruct(# ZS,O,F,G #))]
.= F . x,(0. CLSStruct(# ZS,O,F,G #))
.= H1(X,O) by A1 ;
hence x + (0. CLSStruct(# ZS,O,F,G #)) = x by TARSKI:def 1; :: thesis: verum
end;
thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) :: thesis: ( ( for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #)
reconsider y = O as VECTOR of CLSStruct(# ZS,O,F,G #) ;
take y ; :: thesis: x + y = 0. CLSStruct(# ZS,O,F,G #)
thus x + y = F . [x,y]
.= F . x,y
.= the Zero of CLSStruct(# ZS,O,F,G #) by A1
.= 0. CLSStruct(# ZS,O,F,G #) ; :: thesis: verum
end;
thus for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) :: thesis: ( ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) ) & ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let z be Complex; :: thesis: for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y)
let x, y be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: z * (x + y) = (z * x) + (z * y)
reconsider X = x, Y = y as Element of ZS ;
(z * x) + (z * y) = F . [(z * x),(z * y)]
.= F . (z * x),(z * y)
.= H1(O,O) by A1 ;
hence z * (x + y) = (z * x) + (z * y) by A2; :: thesis: verum
end;
thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) :: thesis: ( ( for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) ) & ( for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x ) )
proof
let z1, z2 be Complex; :: thesis: for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x)
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: (z1 + z2) * x = (z1 * x) + (z2 * x)
set c = z1 + z2;
reconsider X = x as Element of ZS ;
A5: (z1 + z2) * x = G . [(z1 + z2),x]
.= O by A2 ;
(z1 * x) + (z2 * x) = F . [(z1 * x),(z2 * x)]
.= F . (z1 * x),(z2 * x)
.= H1(O,O) by A1 ;
hence (z1 + z2) * x = (z1 * x) + (z2 * x) by A5; :: thesis: verum
end;
thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) :: thesis: for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x
proof
let z1, z2 be Complex; :: thesis: for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x)
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: (z1 * z2) * x = z1 * (z2 * x)
set c = z1 * z2;
reconsider X = x as Element of ZS ;
A6: (z1 * z2) * x = G . [(z1 * z2),x]
.= O by A2 ;
z1 * (z2 * x) = G . [z1,(z2 * x)]
.= O by A2 ;
hence (z1 * z2) * x = z1 * (z2 * x) by A6; :: thesis: verum
end;
thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x :: thesis: verum
proof
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis: 1r * x = x
reconsider X = x as Element of ZS ;
reconsider A' = 1 as Element of REAL ;
1r * x = G . [1r ,x]
.= O by A2 ;
hence 1r * x = x by TARSKI:def 1; :: thesis: verum
end;
end;

definition
let IT be non empty CLSStruct ;
attr IT is ComplexLinearSpace-like means :Def2: :: CLVECT_1:def 2
( ( for z being Complex
for v, w being VECTOR of IT holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of IT holds 1r * v = v ) );
end;

:: deftheorem Def2 defines ComplexLinearSpace-like CLVECT_1:def 2 :
for IT being non empty CLSStruct holds
( IT is ComplexLinearSpace-like iff ( ( for z being Complex
for v, w being VECTOR of IT holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of IT holds 1r * v = v ) ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable strict ComplexLinearSpace-like CLSStruct ;
existence
ex b1 being non empty CLSStruct st
( not b1 is empty & b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is ComplexLinearSpace-like )
proof end;
end;

definition
mode ComplexLinearSpace is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like CLSStruct ;
end;

theorem :: CLVECT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty CLSStruct st ( for v, w being VECTOR of V holds v + w = w + v ) & ( for u, v, w being VECTOR of V holds (u + v) + w = u + (v + w) ) & ( for v being VECTOR of V holds v + (0. V) = v ) & ( for v being VECTOR of V ex w being VECTOR of V st v + w = 0. V ) & ( for z being Complex
for v, w being VECTOR of V holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex
for v being VECTOR of V holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of V holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of V holds 1r * v = v ) holds
V is ComplexLinearSpace by Def2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

theorem Th2: :: CLVECT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
proof end;

theorem Th3: :: CLVECT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
proof end;

theorem Th4: :: CLVECT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds - v = (- 1r ) * v
proof end;

theorem Th5: :: CLVECT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V st v = - v holds
v = 0. V
proof end;

theorem :: CLVECT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V st v + v = 0. V holds
v = 0. V
proof end;

theorem Th7: :: CLVECT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds z * (- v) = (- z) * v
proof end;

theorem Th8: :: CLVECT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds z * (- v) = - (z * v)
proof end;

theorem :: CLVECT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds (- z) * (- v) = z * v
proof end;

theorem Th10: :: CLVECT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex holds z * (v - u) = (z * v) - (z * u)
proof end;

theorem Th11: :: CLVECT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)
proof end;

theorem :: CLVECT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex st z <> 0 & z * v = z * u holds
v = u
proof end;

theorem :: CLVECT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
proof end;

Lm2: for V being non empty LoopStr holds Sum (<*> the carrier of V) = 0. V
proof end;

Lm3: for V being non empty LoopStr
for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
proof end;

theorem :: CLVECT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for z being Complex
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
proof end;

theorem :: CLVECT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for z being Complex holds z * (Sum (<*> the carrier of V)) = 0. V
proof end;

theorem :: CLVECT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)
proof end;

theorem :: CLVECT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v1, v2 being VECTOR of V
for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
proof end;

Lm4: 1r + 1r = [*2,0*]
proof end;

theorem Th18: :: CLVECT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*v,v*> = [*2,0*] * v
proof end;

theorem :: CLVECT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = [*(- 2),0*] * v
proof end;

theorem :: CLVECT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*v,v,v*> = [*3,0*] * v
proof end;

definition
let V be ComplexLinearSpace;
let V1 be Subset of V;
attr V1 is lineary-closed means :Def3: :: CLVECT_1:def 3
( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) );
end;

:: deftheorem Def3 defines lineary-closed CLVECT_1:def 3 :
for V being ComplexLinearSpace
for V1 being Subset of V holds
( V1 is lineary-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) ) );

theorem Th21: :: CLVECT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is lineary-closed holds
0. V in V1
proof end;

theorem Th22: :: CLVECT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is lineary-closed holds
for v being VECTOR of V st v in V1 holds
- v in V1
proof end;

theorem :: CLVECT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is lineary-closed holds
for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1
proof end;

theorem Th24: :: CLVECT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace holds {(0. V)} is lineary-closed
proof end;

theorem :: CLVECT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st the carrier of V = V1 holds
V1 is lineary-closed
proof end;

theorem :: CLVECT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1, V2, V3 being Subset of V st V1 is lineary-closed & V2 is lineary-closed & V3 = { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } holds
V3 is lineary-closed
proof end;

theorem :: CLVECT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1, V2 being Subset of V st V1 is lineary-closed & V2 is lineary-closed holds
V1 /\ V2 is lineary-closed
proof end;

definition
let V be ComplexLinearSpace;
mode Subspace of V -> ComplexLinearSpace means :Def4: :: CLVECT_1:def 4
( the carrier of it c= the carrier of V & the Zero of it = the Zero of V & the add of it = the add of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX ,the carrier of it:] );
existence
ex b1 being ComplexLinearSpace st
( the carrier of b1 c= the carrier of V & the Zero of b1 = the Zero of V & the add of b1 = the add of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:COMPLEX ,the carrier of b1:] )
proof end;
end;

:: deftheorem Def4 defines Subspace CLVECT_1:def 4 :
for V, b2 being ComplexLinearSpace holds
( b2 is Subspace of V iff ( the carrier of b2 c= the carrier of V & the Zero of b2 = the Zero of V & the add of b2 = the add of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:COMPLEX ,the carrier of b2:] ) );

theorem :: CLVECT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
proof end;

theorem Th29: :: CLVECT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V
for x being set st x in W holds
x in V
proof end;

theorem Th30: :: CLVECT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
proof end;

theorem Th31: :: CLVECT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds 0. W = 0. V by Def4;

theorem :: CLVECT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2
proof end;

theorem Th33: :: CLVECT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
proof end;

theorem Th34: :: CLVECT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
proof end;

theorem Th35: :: CLVECT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V
for w being VECTOR of W st w = v holds
- v = - w
proof end;

theorem Th36: :: CLVECT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
proof end;

Lm5: for V being ComplexLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is lineary-closed
proof end;

theorem Th37: :: CLVECT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds 0. V in W
proof end;

theorem :: CLVECT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds 0. W1 in W2
proof end;

theorem :: CLVECT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds 0. W in V
proof end;

theorem Th40: :: CLVECT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u + v in W
proof end;

theorem Th41: :: CLVECT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in W
proof end;

theorem Th42: :: CLVECT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V st v in W holds
- v in W
proof end;

theorem Th43: :: CLVECT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u - v in W
proof end;

theorem Th44: :: CLVECT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the add of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
proof end;

theorem Th45: :: CLVECT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace holds V is Subspace of V
proof end;

theorem Th46: :: CLVECT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, X being strict ComplexLinearSpace st V is Subspace of X & X is Subspace of V holds
V = X
proof end;

theorem Th47: :: CLVECT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, X, Y being ComplexLinearSpace st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y
proof end;

theorem Th48: :: CLVECT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
proof end;

theorem :: CLVECT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
proof end;

registration
let V be ComplexLinearSpace;
cluster strict Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof end;
end;

theorem Th50: :: CLVECT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof end;

theorem Th51: :: CLVECT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proof end;

theorem :: CLVECT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict ComplexLinearSpace
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
proof end;

theorem :: CLVECT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict ComplexLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
proof end;

theorem :: CLVECT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is lineary-closed by Lm5;

theorem Th55: :: CLVECT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is lineary-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
proof end;

definition
let V be ComplexLinearSpace;
func (0). V -> strict Subspace of V means :Def5: :: CLVECT_1:def 5
the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Subspace of V st the carrier of b1 = {(0. V)}
;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines (0). CLVECT_1:def 5 :
for V being ComplexLinearSpace
for b2 being strict Subspace of V holds
( b2 = (0). V iff the carrier of b2 = {(0. V)} );

definition
let V be ComplexLinearSpace;
func (Omega). V -> strict Subspace of V equals :: CLVECT_1:def 6
CLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #);
coherence
CLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) is strict Subspace of V
proof end;
end;

:: deftheorem defines (Omega). CLVECT_1:def 6 :
for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #);

theorem Th56: :: CLVECT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds (0). W = (0). V
proof end;

theorem Th57: :: CLVECT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds (0). W1 = (0). W2
proof end;

theorem :: CLVECT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds (0). W is Subspace of V by Th47;

theorem :: CLVECT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds (0). V is Subspace of W
proof end;

theorem :: CLVECT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
proof end;

theorem :: CLVECT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being strict ComplexLinearSpace holds V is Subspace of (Omega). V ;

definition
let V be ComplexLinearSpace;
let v be VECTOR of V;
let W be Subspace of V;
func v + W -> Subset of V equals :: CLVECT_1:def 7
{ (v + u) where u is VECTOR of V : u in W } ;
coherence
{ (v + u) where u is VECTOR of V : u in W } is Subset of V
proof end;
end;

:: deftheorem defines + CLVECT_1:def 7 :
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

Lm6: for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
proof end;

definition
let V be ComplexLinearSpace;
let W be Subspace of V;
mode Coset of W -> Subset of V means :Def8: :: CLVECT_1:def 8
ex v being VECTOR of V st it = v + W;
existence
ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W
proof end;
end;

:: deftheorem Def8 defines Coset CLVECT_1:def 8 :
for V being ComplexLinearSpace
for W being Subspace of V
for b3 being Subset of V holds
( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W );

theorem Th62: :: CLVECT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )
proof end;

theorem Th63: :: CLVECT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v in v + W
proof end;

theorem :: CLVECT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm6;

theorem Th65: :: CLVECT_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds v + ((0). V) = {v}
proof end;

Lm7: for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
proof end;

theorem Th66: :: CLVECT_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
proof end;

theorem Th67: :: CLVECT_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )
proof end;

theorem :: CLVECT_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W ) by Lm7;

theorem Th69: :: CLVECT_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
proof end;

theorem Th70: :: CLVECT_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
proof end;

theorem Th71: :: CLVECT_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff (- v) + W = the carrier of W )
proof end;

theorem Th72: :: CLVECT_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )
proof end;

theorem :: CLVECT_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )
proof end;

theorem Th74: :: CLVECT_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
proof end;

theorem Th75: :: CLVECT_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
proof end;

theorem Th76: :: CLVECT_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
proof end;

theorem :: CLVECT_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
proof end;

theorem Th78: :: CLVECT_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
proof end;

theorem Th79: :: CLVECT_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
proof end;

theorem :: CLVECT_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( - v in v + W iff v in W )
proof end;

theorem Th81: :: CLVECT_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u + v in v + W iff u in W )
proof end;

theorem :: CLVECT_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v - u in v + W iff u in W )
proof end;

theorem Th83: :: CLVECT_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
proof end;

theorem :: CLVECT_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
proof end;

theorem Th85: :: CLVECT_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
proof end;

theorem Th86: :: CLVECT_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
proof end;

theorem Th87: :: CLVECT_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
proof end;

theorem Th88: :: CLVECT_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
proof end;

theorem Th89: :: CLVECT_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
proof end;

theorem :: CLVECT_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V
for C being Coset of W holds
( C is lineary-closed iff C = the carrier of W )
proof end;

theorem :: CLVECT_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
proof end;

theorem :: CLVECT_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v being VECTOR of V holds {v} is Coset of (0). V
proof end;

theorem :: CLVECT_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
proof end;

theorem :: CLVECT_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V holds the carrier of W is Coset of W
proof end;

theorem :: CLVECT_1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace holds the carrier of V is Coset of (Omega). V
proof end;

theorem :: CLVECT_1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof end;

theorem :: CLVECT_1:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof end;

theorem Th98: :: CLVECT_1:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u being VECTOR of V
for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )
proof end;

theorem :: CLVECT_1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
proof end;

theorem :: CLVECT_1:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
proof end;

theorem :: CLVECT_1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
proof end;

theorem :: CLVECT_1:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being ComplexLinearSpace
for u being VECTOR of V
for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C
proof end;

definition
attr c1 is strict;
struct CNORMSTR -> CLSStruct ;
aggr CNORMSTR(# carrier, Zero, add, Mult, norm #) -> CNORMSTR ;
sel norm c1 -> Function of the carrier of c1, REAL ;
end;

registration
cluster non empty CNORMSTR ;
existence
not for b1 being CNORMSTR holds b1 is empty
proof end;
end;

deffunc H1( CNORMSTR ) -> Element of the carrier of $1 = 0. $1;

definition
let X be non empty CNORMSTR ;
let x be Point of X;
func ||.x.|| -> Real equals :: CLVECT_1:def 9
the norm of X . x;
coherence
the norm of X . x is Real
;
end;

:: deftheorem defines ||. CLVECT_1:def 9 :
for X being non empty CNORMSTR
for x being Point of X holds ||.x.|| = the norm of X . x;

consider V being ComplexLinearSpace;

Lm8: the carrier of ((0). V) = {(0. V)}
by Def5;

reconsider niltonil = the carrier of ((0). V) --> 0 as Function of the carrier of ((0). V), REAL by FUNCOP_1:57;

0. V is VECTOR of ((0). V)
by Lm8, TARSKI:def 1;

then Lm9: niltonil . (0. V) = 0
by FUNCOP_1:13;

Lm10: for u being VECTOR of ((0). V)
for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)
proof end;

Lm11: for u, v being VECTOR of ((0). V) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
proof end;

reconsider X = CNORMSTR(# the carrier of ((0). V),the Zero of ((0). V),the add of ((0). V),the Mult of ((0). V),niltonil #) as non empty CNORMSTR by STRUCT_0:def 1;

Lm12: now
let x, y be Point of X; :: thesis: for z being Complex holds
( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let z be Complex; :: thesis: ( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider u = x, w = y as VECTOR of ((0). V) ;
thus ( ||.x.|| = 0 iff x = H1(X) ) :: thesis: ( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
proof
H1(X) = the Zero of X
.= 0. ((0). V)
.= 0. V by Th31 ;
hence ( ||.x.|| = 0 iff x = H1(X) ) by Lm8, Lm9, TARSKI:def 1; :: thesis: verum
end;
z * x = the Mult of X . [z,u]
.= z * u ;
hence ||.(z * x).|| = |.z.| * ||.x.|| by Lm10; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
x + y = the add of X . [x,y]
.= u + w ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm11; :: thesis: verum
end;

definition
let IT be non empty CNORMSTR ;
attr IT is ComplexNormSpace-like means :Def10: :: CLVECT_1:def 10
for x, y being Point of IT
for z being Complex holds
( ( ||.x.|| = 0 implies x = 0. IT ) & ( x = 0. IT implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| );
end;

:: deftheorem Def10 defines ComplexNormSpace-like CLVECT_1:def 10 :
for IT being non empty CNORMSTR holds
( IT is ComplexNormSpace-like iff for x, y being Point of IT
for z being Complex holds
( ( ||.x.|| = 0 implies x = 0. IT ) & ( x = 0. IT implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like strict ComplexNormSpace-like CNORMSTR ;
existence
ex b1 being non empty CNORMSTR st
( b1 is ComplexNormSpace-like & b1 is ComplexLinearSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition
mode ComplexNormSpace is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like CNORMSTR ;
end;

theorem :: CLVECT_1:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace holds ||.(0. CNS).|| = 0 by Def10;

theorem Th104: :: CLVECT_1:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x being Point of CNS holds ||.(- x).|| = ||.x.||
proof end;

theorem Th105: :: CLVECT_1:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
proof end;

theorem Th106: :: CLVECT_1:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x being Point of CNS holds 0 <= ||.x.||
proof end;

theorem :: CLVECT_1:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Complex
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
proof end;

theorem Th108: :: CLVECT_1:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS holds
( ||.(x - y).|| = 0 iff x = y )
proof end;

theorem Th109: :: CLVECT_1:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.(x - y).|| = ||.(y - x).||
proof end;

theorem Th110: :: CLVECT_1:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proof end;

theorem Th111: :: CLVECT_1:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proof end;

theorem Th112: :: CLVECT_1:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, w, y being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
proof end;

theorem :: CLVECT_1:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x, y being Point of CNS st x <> y holds
||.(x - y).|| <> 0 by Th108;

definition
let CNS be ComplexLinearSpace;
let S1, S2 be sequence of CNS;
func S1 + S2 -> sequence of CNS means :Def11: :: CLVECT_1:def 11
for n being Nat holds it . n = (S1 . n) + (S2 . n);
existence
ex b1 being sequence of CNS st
for n being Nat holds b1 . n = (S1 . n) + (S2 . n)
proof end;
uniqueness
for b1, b2 being sequence of CNS st ( for n being Nat holds b1 . n = (S1 . n) + (S2 . n) ) & ( for n being Nat holds b2 . n = (S1 . n) + (S2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines + CLVECT_1:def 11 :
for CNS being ComplexLinearSpace
for S1, S2, b4 being sequence of CNS holds
( b4 = S1 + S2 iff for n being Nat holds b4 . n = (S1 . n) + (S2 . n) );

definition
let CNS be ComplexLinearSpace;
let S1, S2 be sequence of CNS;
func S1 - S2 -> sequence of CNS means :Def12: :: CLVECT_1:def 12
for n being Nat holds it . n = (S1 . n) - (S2 . n);
existence
ex b1 being sequence of CNS st
for n being Nat holds b1 . n = (S1 . n) - (S2 . n)
proof end;
uniqueness
for b1, b2 being sequence of CNS st ( for n being Nat holds b1 . n = (S1 . n) - (S2 . n) ) & ( for n being Nat holds b2 . n = (S1 . n) - (S2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines - CLVECT_1:def 12 :
for CNS being ComplexLinearSpace
for S1, S2, b4 being sequence of CNS holds
( b4 = S1 - S2 iff for n being Nat holds b4 . n = (S1 . n) - (S2 . n) );

definition
let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let x be Element of CNS;
func S - x -> sequence of CNS means :Def13: :: CLVECT_1:def 13
for n being Nat holds it . n = (S . n) - x;
existence
ex b1 being sequence of CNS st
for n being Nat holds b1 . n = (S . n) - x
proof end;
uniqueness
for b1, b2 being sequence of CNS st ( for n being Nat holds b1 . n = (S . n) - x ) & ( for n being Nat holds b2 . n = (S . n) - x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines - CLVECT_1:def 13 :
for CNS being ComplexLinearSpace
for S being sequence of CNS
for x being Element of CNS
for b4 being sequence of CNS holds
( b4 = S - x iff for n being Nat holds b4 . n = (S . n) - x );

definition
let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let z be Complex;
func z * S -> sequence of CNS means :Def14: :: CLVECT_1:def 14
for n being Nat holds it . n = z * (S . n);
existence
ex b1 being sequence of CNS st
for n being Nat holds b1 . n = z * (S . n)
proof end;
uniqueness
for b1, b2 being sequence of CNS st ( for n being Nat holds b1 . n = z * (S . n) ) & ( for n being Nat holds b2 . n = z * (S . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines * CLVECT_1:def 14 :
for CNS being ComplexLinearSpace
for S being sequence of CNS
for z being Complex
for b4 being sequence of CNS holds
( b4 = z * S iff for n being Nat holds b4 . n = z * (S . n) );

definition
let CNS be ComplexNormSpace;
let S be sequence of CNS;
attr S is convergent means :Def15: :: CLVECT_1:def 15
ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r;
end;

:: deftheorem Def15 defines convergent CLVECT_1:def 15 :
for CNS being ComplexNormSpace
for S being sequence of CNS holds
( S is convergent iff ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r );

theorem :: CLVECT_1:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th115: :: CLVECT_1:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
proof end;

theorem Th116: :: CLVECT_1:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent
proof end;

theorem Th117: :: CLVECT_1:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
S - x is convergent
proof end;

theorem Th118: :: CLVECT_1:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Complex
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
z * S is convergent
proof end;

definition
let CNS be ComplexNormSpace;
let S be sequence of CNS;
func ||.S.|| -> Real_Sequence means :Def16: :: CLVECT_1:def 16
for n being Nat holds it . n = ||.(S . n).||;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = ||.(S . n).||
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ||.(S . n).|| ) & ( for n being Nat holds b2 . n = ||.(S . n).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines ||. CLVECT_1:def 16 :
for CNS being ComplexNormSpace
for S being sequence of CNS
for b3 being Real_Sequence holds
( b3 = ||.S.|| iff for n being Nat holds b3 . n = ||.(S . n).|| );

theorem Th119: :: CLVECT_1:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
||.S.|| is convergent
proof end;

definition
let CNS be ComplexNormSpace;
let S be sequence of CNS;
assume A1: S is convergent ;
func lim S -> Point of CNS means :Def17: :: CLVECT_1:def 17
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - it).|| < r;
existence
ex b1 being Point of CNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b1).|| < r
by A1, Def15;
uniqueness
for b1, b2 being Point of CNS st ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines lim CLVECT_1:def 17 :
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
for b3 being Point of CNS holds
( b3 = lim S iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - b3).|| < r );

theorem :: CLVECT_1:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for g being Point of CNS
for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
proof end;

theorem :: CLVECT_1:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
proof end;

theorem :: CLVECT_1:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
proof end;

theorem :: CLVECT_1:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
proof end;

theorem :: CLVECT_1:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Complex
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
proof end;