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

definition
let S be 1-sorted ;
let x be set ;
assume A1: x in S ;
func vector S,x -> Element of S equals :Def1: :: RLVECT_2:def 1
x;
coherence
x is Element of S
by A1, RLVECT_1:def 1;
end;

:: deftheorem Def1 defines vector RLVECT_2:def 1 :
for S being 1-sorted
for x being set st x in S holds
vector S,x = x;

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

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

theorem Th3: :: RLVECT_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty 1-sorted
for v being Element of S holds vector S,v = v
proof end;

theorem Th4: :: RLVECT_2:4  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 Abelian add-associative right_zeroed right_complementable LoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
proof end;

theorem :: RLVECT_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a being Real
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proof end;

theorem Th6: :: RLVECT_2:6  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 Abelian add-associative right_zeroed right_complementable LoopStr
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = - (F /. k) ) holds
Sum G = - (Sum F)
proof end;

theorem :: RLVECT_2:7  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 Abelian add-associative right_zeroed right_complementable LoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
proof end;

Lm1: for k, n being Nat st k < n holds
n - 1 is Nat
by NAT_1:60;

theorem Th8: :: RLVECT_2:8  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 Abelian add-associative right_zeroed right_complementable LoopStr
for F, G being FinSequence of the carrier of V
for f being Permutation of dom F st len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
proof end;

theorem :: RLVECT_2:9  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 Abelian add-associative right_zeroed right_complementable LoopStr
for F, G being FinSequence of the carrier of V
for f being Permutation of dom F st G = F * f holds
Sum F = Sum G
proof end;

registration
let V be 1-sorted ;
cluster empty finite Element of bool the carrier of V;
existence
ex b1 being Subset of V st
( b1 is empty & b1 is finite )
proof end;
end;

definition
let V be 1-sorted ;
let S, T be finite Subset of V;
:: original: \/
redefine func S \/ T -> finite Subset of V;
coherence
S \/ T is finite Subset of V
proof end;
:: original: /\
redefine func S /\ T -> finite Subset of V;
coherence
S /\ T is finite Subset of V
proof end;
:: original: \
redefine func S \ T -> finite Subset of V;
coherence
S \ T is finite Subset of V
proof end;
:: original: \+\
redefine func S \+\ T -> finite Subset of V;
coherence
S \+\ T is finite Subset of V
proof end;
end;

definition
let V be non empty LoopStr ;
let T be finite Subset of V;
assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ;
canceled;
canceled;
func Sum T -> Element of V means :Def4: :: RLVECT_2:def 4
ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & it = Sum F );
existence
ex b1 being Element of V ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F )
proof end;
uniqueness
for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b2 = Sum F ) holds
b1 = b2
by A1, RLVECT_1:59;
end;

:: deftheorem RLVECT_2:def 2 :
canceled;

:: deftheorem RLVECT_2:def 3 :
canceled;

:: deftheorem Def4 defines Sum RLVECT_2:def 4 :
for V being non empty LoopStr
for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds
for b3 being Element of V holds
( b3 = Sum T iff ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b3 = Sum F ) );

registration
let V be non empty 1-sorted ;
cluster non empty finite Element of bool the carrier of V;
existence
ex b1 being Subset of V st
( not b1 is empty & b1 is finite )
proof end;
end;

definition
let V be non empty 1-sorted ;
let v be Element of V;
:: original: {
redefine func {v} -> finite Subset of V;
coherence
{v} is finite Subset of V
proof end;
end;

definition
let V be non empty 1-sorted ;
let v1, v2 be Element of V;
:: original: {
redefine func {v1,v2} -> finite Subset of V;
coherence
{v1,v2} is finite Subset of V
proof end;
end;

definition
let V be non empty 1-sorted ;
let v1, v2, v3 be Element of V;
:: original: {
redefine func {v1,v2,v3} -> finite Subset of V;
coherence
{v1,v2,v3} is finite Subset of V
proof end;
end;

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

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

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

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

theorem Th14: :: RLVECT_2:14  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 Abelian add-associative right_zeroed LoopStr holds Sum ({} V) = 0. V
proof end;

theorem :: RLVECT_2:15  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 Abelian add-associative right_zeroed right_complementable LoopStr
for v being Element of V holds Sum {v} = v
proof end;

theorem :: RLVECT_2:16  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 Abelian add-associative right_zeroed right_complementable LoopStr
for v1, v2 being Element of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
proof end;

theorem :: RLVECT_2:17  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 Abelian add-associative right_zeroed right_complementable LoopStr
for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
proof end;

theorem Th18: :: RLVECT_2:18  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 Abelian add-associative right_zeroed LoopStr
for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
proof end;

theorem Th19: :: RLVECT_2:19  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 Abelian add-associative right_zeroed right_complementable LoopStr
for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
proof end;

theorem :: RLVECT_2:20  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 Abelian add-associative right_zeroed right_complementable LoopStr
for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
proof end;

theorem Th21: :: RLVECT_2:21  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 Abelian add-associative right_zeroed right_complementable LoopStr
for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
proof end;

theorem Th22: :: RLVECT_2:22  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 Abelian add-associative right_zeroed right_complementable LoopStr
for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
proof end;

theorem :: RLVECT_2:23  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 Abelian add-associative right_zeroed right_complementable LoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
proof end;

theorem :: RLVECT_2:24  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 Abelian add-associative right_zeroed LoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T))
proof end;

definition
let V be non empty ZeroStr ;
mode Linear_Combination of V -> Element of Funcs the carrier of V,REAL means :Def5: :: RLVECT_2:def 5
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,REAL 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 Def5 defines Linear_Combination RLVECT_2:def 5 :
for V being non empty ZeroStr
for b2 being Element of Funcs the carrier of V,REAL holds
( b2 is 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 LoopStr ;
let L be Linear_Combination of V;
func Carrier L -> finite Subset of V equals :: RLVECT_2:def 6
{ v where v is Element of V : L . v <> 0 } ;
coherence
{ v where v is Element of V : L . v <> 0 } is finite Subset of V
proof end;
end;

:: deftheorem defines Carrier RLVECT_2:def 6 :
for V being non empty LoopStr
for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0 } ;

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

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

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

theorem :: RLVECT_2:28  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 LoopStr
for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0 iff not v in Carrier L )
proof end;

definition
let V be non empty LoopStr ;
func ZeroLC V -> Linear_Combination of V means :Def7: :: RLVECT_2:def 7
Carrier it = {} ;
existence
ex b1 being Linear_Combination of V st Carrier b1 = {}
proof end;
uniqueness
for b1, b2 being Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines ZeroLC RLVECT_2:def 7 :
for V being non empty LoopStr
for b2 being Linear_Combination of V holds
( b2 = ZeroLC V iff Carrier b2 = {} );

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

theorem Th30: :: RLVECT_2:30  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 LoopStr
for v being Element of V holds (ZeroLC V) . v = 0
proof end;

definition
let V be non empty LoopStr ;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def8: :: RLVECT_2:def 8
Carrier it c= A;
existence
ex b1 being Linear_Combination of V st Carrier b1 c= A
proof end;
end;

:: deftheorem Def8 defines Linear_Combination RLVECT_2:def 8 :
for V being non empty LoopStr
for A being Subset of V
for b3 being Linear_Combination of V holds
( b3 is Linear_Combination of A iff Carrier b3 c= A );

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

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

theorem :: RLVECT_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
proof end;

theorem Th34: :: RLVECT_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proof end;

theorem Th35: :: RLVECT_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proof end;

definition
let V be RealLinearSpace;
let F be FinSequence of the carrier of V;
let f be Function of the carrier of V, REAL ;
func f (#) F -> FinSequence of the carrier of V means :Def9: :: RLVECT_2:def 9
( 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 Def9 defines (#) RLVECT_2:def 9 :
for V being RealLinearSpace
for F being FinSequence of the carrier of V
for f being Function of the carrier of V, REAL
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 :: RLVECT_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

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

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

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

theorem Th40: :: RLVECT_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for V being RealLinearSpace
for v being VECTOR of V
for F being FinSequence of the carrier of V
for f being Function of the carrier of V, REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
proof end;

theorem :: RLVECT_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for f being Function of the carrier of V, REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V
proof end;

theorem Th42: :: RLVECT_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V
for f being Function of the carrier of V, REAL holds f (#) <*v*> = <*((f . v) * v)*>
proof end;

theorem Th43: :: RLVECT_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for f being Function of the carrier of V, REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proof end;

theorem :: RLVECT_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V, REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proof end;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func Sum L -> Element of V means :Def10: :: RLVECT_2:def 10
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 Def10 defines Sum RLVECT_2:def 10 :
for V being RealLinearSpace
for L being 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) ) );

Lm2: for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V
proof end;

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

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

theorem :: RLVECT_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A being Subset of V holds
( ( A <> {} & A is lineary-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proof end;

theorem :: RLVECT_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V by Lm2;

theorem :: RLVECT_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proof end;

theorem Th50: :: RLVECT_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
proof end;

theorem Th51: :: RLVECT_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
proof end;

theorem :: RLVECT_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proof end;

theorem :: RLVECT_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
proof end;

theorem :: RLVECT_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination 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 LoopStr ;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine pred L1 = L2 means :: RLVECT_2:def 11
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 = RLVECT_2:def 11 :
for V being non empty LoopStr
for L1, L2 being 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 LoopStr ;
let L1, L2 be Linear_Combination of V;
func L1 + L2 -> Linear_Combination of V means :Def12: :: RLVECT_2:def 12
for v being Element of V holds it . v = (L1 . v) + (L2 . v);
existence
ex b1 being Linear_Combination of V st
for v being Element of V holds b1 . v = (L1 . v) + (L2 . v)
proof end;
uniqueness
for b1, b2 being Linear_Combination of V st ( for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) ) & ( for v being Element of V holds b2 . v = (L1 . v) + (L2 . v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines + RLVECT_2:def 12 :
for V being non empty LoopStr
for L1, L2, b4 being Linear_Combination of V holds
( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) );

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

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

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

theorem Th58: :: RLVECT_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proof end;

theorem Th59: :: RLVECT_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
proof end;

theorem Th60: :: RLVECT_2:60  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 LoopStr
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
proof end;

theorem Th61: :: RLVECT_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proof end;

theorem Th62: :: RLVECT_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
proof end;

definition
let V be RealLinearSpace;
let a be Real;
let L be Linear_Combination of V;
func a * L -> Linear_Combination of V means :Def13: :: RLVECT_2:def 13
for v being VECTOR of V holds it . v = a * (L . v);
existence
ex b1 being Linear_Combination of V st
for v being VECTOR of V holds b1 . v = a * (L . v)
proof end;
uniqueness
for b1, b2 being 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 Def13 defines * RLVECT_2:def 13 :
for V being RealLinearSpace
for a being Real
for L, b4 being Linear_Combination of V holds
( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) );

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

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

theorem Th65: :: RLVECT_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V st a <> 0 holds
Carrier (a * L) = Carrier L
proof end;

theorem Th66: :: RLVECT_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds 0 * L = ZeroLC V
proof end;

theorem Th67: :: RLVECT_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a being Real
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
proof end;

theorem Th68: :: RLVECT_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proof end;

theorem Th69: :: RLVECT_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a being Real
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proof end;

theorem Th70: :: RLVECT_2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
proof end;

theorem Th71: :: RLVECT_2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds 1 * L = L
proof end;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: RLVECT_2:def 14
(- 1) * L;
correctness
coherence
(- 1) * L is Linear_Combination of V
;
;
end;

:: deftheorem defines - RLVECT_2:def 14 :
for V being RealLinearSpace
for L being Linear_Combination of V holds - L = (- 1) * L;

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

theorem Th73: :: RLVECT_2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proof end;

theorem :: RLVECT_2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proof end;

theorem Th75: :: RLVECT_2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th65;

theorem Th76: :: RLVECT_2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by Th67;

theorem :: RLVECT_2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds - (- L) = L
proof end;

definition
let V be RealLinearSpace;
let L1, L2 be Linear_Combination of V;
func L1 - L2 -> Linear_Combination of V equals :: RLVECT_2:def 15
L1 + (- L2);
correctness
coherence
L1 + (- L2) is Linear_Combination of V
;
;
end;

:: deftheorem defines - RLVECT_2:def 15 :
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

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

theorem Th79: :: RLVECT_2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proof end;

theorem :: RLVECT_2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proof end;

theorem :: RLVECT_2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
proof end;

theorem Th82: :: RLVECT_2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds L - L = ZeroLC V
proof end;

definition
let V be RealLinearSpace;
func LinComb V -> set means :Def16: :: RLVECT_2:def 16
for x being set holds
( x in it iff x is Linear_Combination of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Linear_Combination of V )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in b2 iff x is Linear_Combination of V ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines LinComb RLVECT_2:def 16 :
for V being RealLinearSpace
for b2 being set holds
( b2 = LinComb V iff for x being set holds
( x in b2 iff x is Linear_Combination of V ) );

registration
let V be RealLinearSpace;
cluster LinComb V -> non empty ;
coherence
not LinComb V is empty
proof end;
end;

definition
let V be RealLinearSpace;
let e be Element of LinComb V;
func @ e -> Linear_Combination of V equals :: RLVECT_2:def 17
e;
coherence
e is Linear_Combination of V
by Def16;
end;

:: deftheorem defines @ RLVECT_2:def 17 :
for V being RealLinearSpace
for e being Element of LinComb V holds @ e = e;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func @ L -> Element of LinComb V equals :: RLVECT_2:def 18
L;
coherence
L is Element of LinComb V
by Def16;
end;

:: deftheorem defines @ RLVECT_2:def 18 :
for V being RealLinearSpace
for L being Linear_Combination of V holds @ L = L;

definition
let V be RealLinearSpace;
func LCAdd V -> BinOp of LinComb V means :Def19: :: RLVECT_2:def 19
for e1, e2 being Element of LinComb V holds it . e1,e2 = (@ e1) + (@ e2);
existence
ex b1 being BinOp of LinComb V st
for e1, e2 being Element of LinComb V holds b1 . e1,e2 = (@ e1) + (@ e2)
proof end;
uniqueness
for b1, b2 being BinOp of LinComb V st ( for e1, e2 being Element of LinComb V holds b1 . e1,e2 = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b2 . e1,e2 = (@ e1) + (@ e2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines LCAdd RLVECT_2:def 19 :
for V being RealLinearSpace
for b2 being BinOp of LinComb V holds
( b2 = LCAdd V iff for e1, e2 being Element of LinComb V holds b2 . e1,e2 = (@ e1) + (@ e2) );

definition
let V be RealLinearSpace;
func LCMult V -> Function of [:REAL ,(LinComb V):], LinComb V means :Def20: :: RLVECT_2:def 20
for a being Real
for e being Element of LinComb V holds it . [a,e] = a * (@ e);
existence
ex b1 being Function of [:REAL ,(LinComb V):], LinComb V st
for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
proof end;
uniqueness
for b1, b2 being Function of [:REAL ,(LinComb V):], LinComb V st ( for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines LCMult RLVECT_2:def 20 :
for V being RealLinearSpace
for b2 being Function of [:REAL ,(LinComb V):], LinComb V holds
( b2 = LCMult V iff for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) );

definition
let V be RealLinearSpace;
func LC_RLSpace V -> RealLinearSpace equals :: RLVECT_2:def 21
RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);
coherence
RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #) is RealLinearSpace
proof end;
end;

:: deftheorem defines LC_RLSpace RLVECT_2:def 21 :
for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

registration
let V be RealLinearSpace;
cluster LC_RLSpace V -> strict ;
coherence
( LC_RLSpace V is strict & not LC_RLSpace V is empty )
;
end;

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

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

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

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

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

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

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

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

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

theorem :: RLVECT_2:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the carrier of (LC_RLSpace V) = LinComb V ;

theorem :: RLVECT_2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the Zero of (LC_RLSpace V) = ZeroLC V ;

theorem :: RLVECT_2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the add of (LC_RLSpace V) = LCAdd V ;

theorem :: RLVECT_2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the Mult of (LC_RLSpace V) = LCMult V ;

theorem Th96: :: RLVECT_2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector (LC_RLSpace V),L1) + (vector (LC_RLSpace V),L2) = L1 + L2
proof end;

theorem Th97: :: RLVECT_2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V holds a * (vector (LC_RLSpace V),L) = a * L
proof end;

theorem Th98: :: RLVECT_2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being Linear_Combination of V holds - (vector (LC_RLSpace V),L) = - L
proof end;

theorem :: RLVECT_2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector (LC_RLSpace V),L1) - (vector (LC_RLSpace V),L2) = L1 - L2
proof end;

definition
let V be RealLinearSpace;
let A be Subset of V;
func LC_RLSpace A -> strict Subspace of LC_RLSpace V means :: RLVECT_2:def 22
the carrier of it = { l where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum }
proof end;
uniqueness
for b1, b2 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } & the carrier of b2 = { l where l is Linear_Combination of A : verum } holds
b1 = b2
by RLSUB_1:38;
end;

:: deftheorem defines LC_RLSpace RLVECT_2:def 22 :
for V being RealLinearSpace
for A being Subset of V
for b3 being strict Subspace of LC_RLSpace V holds
( b3 = LC_RLSpace A iff the carrier of b3 = { l where l is Linear_Combination of A : verum } );