:: by Wojciech A. Trybulec

::

:: Received April 8, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

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

for S being 1-sorted

for x being set st x in S holds

vector (S,x) = x;

theorem :: RLVECT_2:1

theorem Th2: :: RLVECT_2:2

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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)

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

for V being RealLinearSpace

for a being Real

for F, G being FinSequence 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)

for a being Real

for F, G being FinSequence 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 Th4: :: RLVECT_2:4

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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)

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

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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)

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 Th6: :: RLVECT_2:6

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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

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

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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

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;

definition

let V be non empty addLoopStr ;

let T be finite Subset of V;

assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ;

ex b_{1} being Element of V ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & b_{1} = Sum F )

for b_{1}, b_{2} being Element of V st ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & b_{1} = Sum F ) & ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & b_{2} = Sum F ) holds

b_{1} = b_{2}
by A1, RLVECT_1:42;

end;
let T be finite Subset of V;

assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ;

func Sum T -> Element of V means :Def2: :: RLVECT_2:def 2

ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & it = Sum F );

existence ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & it = Sum F );

ex b

( rng F = T & F is one-to-one & b

proof end;

uniqueness for b

( rng F = T & F is one-to-one & b

( rng F = T & F is one-to-one & b

b

:: deftheorem Def2 defines Sum RLVECT_2:def 2 :

for V being non empty addLoopStr

for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds

for b_{3} being Element of V holds

( b_{3} = Sum T iff ex F being FinSequence of the carrier of V st

( rng F = T & F is one-to-one & b_{3} = Sum F ) );

for V being non empty addLoopStr

for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds

for b

( b

( rng F = T & F is one-to-one & b

theorem :: RLVECT_2:9

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v being Element of V holds Sum {v} = v

for v being Element of V holds Sum {v} = v

proof end;

theorem :: RLVECT_2:10

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v1, v2 being Element of V st v1 <> v2 holds

Sum {v1,v2} = v1 + v2

for v1, v2 being Element of V st v1 <> v2 holds

Sum {v1,v2} = v1 + v2

proof end;

theorem :: RLVECT_2:11

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds

Sum {v1,v2,v3} = (v1 + v2) + v3

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 Th12: :: RLVECT_2:12

for V being non empty Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V st T misses S holds

Sum (T \/ S) = (Sum T) + (Sum S)

for S, T being finite Subset of V st T misses S holds

Sum (T \/ S) = (Sum T) + (Sum S)

proof end;

theorem Th13: :: RLVECT_2:13

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))

for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))

proof end;

theorem :: RLVECT_2:14

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))

for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))

proof end;

theorem Th15: :: RLVECT_2:15

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

proof end;

theorem Th16: :: RLVECT_2:16

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))

for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))

proof end;

theorem :: RLVECT_2:17

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))

proof end;

theorem :: RLVECT_2:18

for V being non empty Abelian add-associative right_zeroed addLoopStr

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82;

for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82;

reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

definition

let V be non empty ZeroStr ;

ex b_{1} 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

b_{1} . v = 0

end;
mode Linear_Combination of V -> Element of Funcs ( the carrier of V,REAL) means :Def3: :: RLVECT_2:def 3

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 T being finite Subset of V st

for v being Element of V st not v in T holds

it . v = 0 ;

ex b

for v being Element of V st not v in T holds

b

proof end;

:: deftheorem Def3 defines Linear_Combination RLVECT_2:def 3 :

for V being non empty ZeroStr

for b_{2} being Element of Funcs ( the carrier of V,REAL) holds

( b_{2} 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

b_{2} . v = 0 );

for V being non empty ZeroStr

for b

( b

for v being Element of V st not v in T holds

b

notation

let V be non empty addLoopStr ;

let L be Element of Funcs ( the carrier of V,REAL);

synonym Carrier L for support V;

end;
let L be Element of Funcs ( the carrier of V,REAL);

synonym Carrier L for support V;

Lm1: now :: thesis: for V being non empty addLoopStr

for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V

for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V

let V be non empty addLoopStr ; :: thesis: for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V

let L be Element of Funcs ( the carrier of V,REAL); :: thesis: Carrier c= the carrier of V

A1: support L c= dom L by PRE_POLY:37;

thus Carrier c= the carrier of V :: thesis: verum

end;
let L be Element of Funcs ( the carrier of V,REAL); :: thesis: Carrier c= the carrier of V

A1: support L c= dom L by PRE_POLY:37;

thus Carrier c= the carrier of V :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier or x in the carrier of V )

assume x in support L ; :: thesis: x in the carrier of V

then x in dom L by A1;

hence x in the carrier of V ; :: thesis: verum

end;
assume x in support L ; :: thesis: x in the carrier of V

then x in dom L by A1;

hence x in the carrier of V ; :: thesis: verum

definition

let V be non empty addLoopStr ;

let L be Element of Funcs ( the carrier of V,REAL);

Carrier is Subset of V by Lm1;

compatibility

for b_{1} being Subset of V holds

( b_{1} = Carrier iff b_{1} = { v where v is Element of V : L . v <> 0 } )

end;
let L be Element of Funcs ( the carrier of V,REAL);

:: original: Carrier

redefine func Carrier L -> Subset of V equals :: RLVECT_2:def 4

{ v where v is Element of V : L . v <> 0 } ;

coherence redefine func Carrier L -> Subset of V equals :: RLVECT_2:def 4

{ v where v is Element of V : L . v <> 0 } ;

Carrier is Subset of V by Lm1;

compatibility

for b

( b

proof end;

:: deftheorem defines Carrier RLVECT_2:def 4 :

for V being non empty addLoopStr

for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L = { v where v is Element of V : L . v <> 0 } ;

for V being non empty addLoopStr

for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L = { v where v is Element of V : L . v <> 0 } ;

registration

let V be non empty addLoopStr ;

let L be Linear_Combination of V;

coherence

Carrier L is finite

end;
let L be Linear_Combination of V;

coherence

Carrier L is finite

proof end;

theorem :: RLVECT_2:19

for V being non empty addLoopStr

for L being Linear_Combination of V

for v being Element of V holds

( L . v = 0 iff not v in Carrier L )

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

existence

ex b_{1} being Linear_Combination of V st Carrier b_{1} = {}

for b_{1}, b_{2} being Linear_Combination of V st Carrier b_{1} = {} & Carrier b_{2} = {} holds

b_{1} = b_{2}

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines ZeroLC RLVECT_2:def 5 :

for V being non empty addLoopStr

for b_{2} being Linear_Combination of V holds

( b_{2} = ZeroLC V iff Carrier b_{2} = {} );

for V being non empty addLoopStr

for b

( b

definition

let V be non empty addLoopStr ;

let A be Subset of V;

ex b_{1} being Linear_Combination of V st Carrier b_{1} c= A

end;
let A be Subset of V;

mode Linear_Combination of A -> Linear_Combination of V means :Def6: :: RLVECT_2:def 6

Carrier it c= A;

existence Carrier it c= A;

ex b

proof end;

:: deftheorem Def6 defines Linear_Combination RLVECT_2:def 6 :

for V being non empty addLoopStr

for A being Subset of V

for b_{3} being Linear_Combination of V holds

( b_{3} is Linear_Combination of A iff Carrier b_{3} c= A );

for V being non empty addLoopStr

for A being Subset of V

for b

( b

theorem :: RLVECT_2:21

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

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 Th23: :: RLVECT_2:23

for V being RealLinearSpace

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

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

let f be Function of the carrier of V,REAL;

ex b_{1} being FinSequence of the carrier of V st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) )

for b_{1}, b_{2} being FinSequence of the carrier of V st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (f . (F /. i)) * (F /. i) ) holds

b_{1} = b_{2}

end;
let F be FinSequence of V;

let f be Function of the carrier of V,REAL;

func f (#) F -> FinSequence of the carrier of V means :Def7: :: RLVECT_2:def 7

( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

existence ( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines (#) RLVECT_2:def 7 :

for V being RealLinearSpace

for F being FinSequence of V

for f being Function of the carrier of V,REAL

for b_{4} being FinSequence of the carrier of V holds

( b_{4} = f (#) F iff ( len b_{4} = len F & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = (f . (F /. i)) * (F /. i) ) ) );

for V being RealLinearSpace

for F being FinSequence of V

for f being Function of the carrier of V,REAL

for b

( b

b

theorem Th24: :: RLVECT_2:24

for i being Nat

for V being RealLinearSpace

for v being VECTOR of V

for F being FinSequence 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

for V being RealLinearSpace

for v being VECTOR of V

for F being FinSequence 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:25

for V being RealLinearSpace

for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V

for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V

proof end;

theorem Th26: :: RLVECT_2:26

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)*>

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 Th27: :: RLVECT_2:27

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)*>

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

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)*>

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;

ex b_{1} being Element of V ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) )

for b_{1}, b_{2} being Element of V st ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) ) & ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{2} = Sum (L (#) F) ) holds

b_{1} = b_{2}

end;
let L be Linear_Combination of V;

func Sum L -> Element of V means :Def8: :: RLVECT_2:def 8

ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

existence ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

ex b

( F is one-to-one & rng F = Carrier L & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier L & b

( F is one-to-one & rng F = Carrier L & b

b

proof end;

:: deftheorem Def8 defines Sum RLVECT_2:def 8 :

for V being RealLinearSpace

for L being Linear_Combination of V

for b_{3} being Element of V holds

( b_{3} = Sum L iff ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & b_{3} = Sum (L (#) F) ) );

for V being RealLinearSpace

for L being Linear_Combination of V

for b

( b

( F is one-to-one & rng F = Carrier L & b

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

proof end;

theorem :: RLVECT_2:29

for V being RealLinearSpace

for A being Subset of V holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

for A being Subset of V holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

proof end;

theorem :: RLVECT_2:31

for V being RealLinearSpace

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

proof end;

theorem Th32: :: RLVECT_2:32

for V being RealLinearSpace

for v being VECTOR of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v

for v being VECTOR of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v

proof end;

theorem Th33: :: RLVECT_2:33

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)

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

for V being RealLinearSpace

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V

proof end;

theorem :: RLVECT_2:35

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

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

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)

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

let L1, L2 be Linear_Combination of V;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) ;

end;
let L1, L2 be Linear_Combination of V;

:: original: =

redefine pred L1 = L2 means :: RLVECT_2:def 9

for v being Element of V holds L1 . v = L2 . v;

compatibility redefine pred L1 = L2 means :: RLVECT_2:def 9

for v being Element of V holds L1 . v = L2 . v;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) ;

:: deftheorem defines = RLVECT_2:def 9 :

for V being non empty addLoopStr

for L1, L2 being Linear_Combination of V holds

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );

for V being non empty addLoopStr

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

let L1, L2 be Linear_Combination of V;

L1 + L2 is Linear_Combination of V

for b_{1} being Linear_Combination of V holds

( b_{1} = L1 + L2 iff for v being Element of V holds b_{1} . v = (L1 . v) + (L2 . v) )

end;
let L1, L2 be Linear_Combination of V;

:: original: +

redefine func L1 + L2 -> Linear_Combination of V means :Def10: :: RLVECT_2:def 10

for v being Element of V holds it . v = (L1 . v) + (L2 . v);

coherence redefine func L1 + L2 -> Linear_Combination of V means :Def10: :: RLVECT_2:def 10

for v being Element of V holds it . v = (L1 . v) + (L2 . v);

L1 + L2 is Linear_Combination of V

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def10 defines + RLVECT_2:def 10 :

for V being non empty addLoopStr

for L1, L2, b_{4} being Linear_Combination of V holds

( b_{4} = L1 + L2 iff for v being Element of V holds b_{4} . v = (L1 . v) + (L2 . v) );

for V being non empty addLoopStr

for L1, L2, b

( b

theorem Th37: :: RLVECT_2:37

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem Th38: :: RLVECT_2:38

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

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 :: RLVECT_2:39

theorem Th40: :: RLVECT_2:40

for V being RealLinearSpace

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

proof end;

theorem Th41: :: RLVECT_2:41

for V being RealLinearSpace

for L being Linear_Combination of V holds

( L + (ZeroLC V) = L & (ZeroLC V) + L = L )

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;

ex b_{1} being Linear_Combination of V st

for v being VECTOR of V holds b_{1} . v = a * (L . v)

for b_{1}, b_{2} being Linear_Combination of V st ( for v being VECTOR of V holds b_{1} . v = a * (L . v) ) & ( for v being VECTOR of V holds b_{2} . v = a * (L . v) ) holds

b_{1} = b_{2}

end;
let a be Real;

let L be Linear_Combination of V;

func a * L -> Linear_Combination of V means :Def11: :: RLVECT_2:def 11

for v being VECTOR of V holds it . v = a * (L . v);

existence for v being VECTOR of V holds it . v = a * (L . v);

ex b

for v being VECTOR of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines * RLVECT_2:def 11 :

for V being RealLinearSpace

for a being Real

for L, b_{4} being Linear_Combination of V holds

( b_{4} = a * L iff for v being VECTOR of V holds b_{4} . v = a * (L . v) );

for V being RealLinearSpace

for a being Real

for L, b

( b

theorem Th42: :: RLVECT_2:42

for V being RealLinearSpace

for a being Real

for L being Linear_Combination of V st a <> 0 holds

Carrier (a * L) = Carrier L

for a being Real

for L being Linear_Combination of V st a <> 0 holds

Carrier (a * L) = Carrier L

proof end;

theorem Th44: :: RLVECT_2:44

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

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 Th45: :: RLVECT_2:45

for V being RealLinearSpace

for a, b being Real

for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)

for a, b being Real

for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)

proof end;

theorem Th46: :: RLVECT_2:46

for V being RealLinearSpace

for a being Real

for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)

for a being Real

for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)

proof end;

theorem Th47: :: RLVECT_2:47

for V being RealLinearSpace

for a, b being Real

for L being Linear_Combination of V holds a * (b * L) = (a * b) * L

for a, b being Real

for L being Linear_Combination of V holds a * (b * L) = (a * b) * L

proof end;

definition

let V be RealLinearSpace;

let L be Linear_Combination of V;

correctness

coherence

(- 1) * L is Linear_Combination of V;

;

end;
let L be Linear_Combination of V;

correctness

coherence

(- 1) * L is Linear_Combination of V;

;

:: deftheorem defines - RLVECT_2:def 12 :

for V being RealLinearSpace

for L being Linear_Combination of V holds - L = (- 1) * L;

for V being RealLinearSpace

for L being Linear_Combination of V holds - L = (- 1) * L;

theorem Th49: :: RLVECT_2:49

for V being RealLinearSpace

for v being VECTOR of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

for v being VECTOR of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

theorem :: RLVECT_2:50

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1

proof end;

theorem :: RLVECT_2:51

for V being RealLinearSpace

for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th42;

for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th42;

theorem :: RLVECT_2:52

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

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

definition

let V be RealLinearSpace;

let L1, L2 be Linear_Combination of V;

correctness

coherence

L1 + (- L2) is Linear_Combination of V;

;

end;
let L1, L2 be Linear_Combination of V;

correctness

coherence

L1 + (- L2) is Linear_Combination of V;

;

:: deftheorem defines - RLVECT_2:def 13 :

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th54: :: RLVECT_2:54

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)

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

for V being RealLinearSpace

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem :: RLVECT_2:56

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

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;

definition

let V be RealLinearSpace;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Linear_Combination of V )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Linear_Combination of V ) ) & ( for x being set holds

( x in b_{2} iff x is Linear_Combination of V ) ) holds

b_{1} = b_{2}

end;
func LinComb V -> set means :Def14: :: RLVECT_2:def 14

for x being set holds

( x in it iff x is Linear_Combination of V );

existence for x being set holds

( x in it iff x is Linear_Combination of V );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def14 defines LinComb RLVECT_2:def 14 :

for V being RealLinearSpace

for b_{2} being set holds

( b_{2} = LinComb V iff for x being set holds

( x in b_{2} iff x is Linear_Combination of V ) );

for V being RealLinearSpace

for b

( b

( x in b

definition

let V be RealLinearSpace;

let e be Element of LinComb V;

coherence

e is Linear_Combination of V by Def14;

end;
let e be Element of LinComb V;

coherence

e is Linear_Combination of V by Def14;

:: deftheorem defines @ RLVECT_2:def 15 :

for V being RealLinearSpace

for e being Element of LinComb V holds @ e = e;

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;

coherence

L is Element of LinComb V by Def14;

end;
let L be Linear_Combination of V;

coherence

L is Element of LinComb V by Def14;

:: deftheorem defines @ RLVECT_2:def 16 :

for V being RealLinearSpace

for L being Linear_Combination of V holds @ L = L;

for V being RealLinearSpace

for L being Linear_Combination of V holds @ L = L;

definition

let V be RealLinearSpace;

ex b_{1} being BinOp of (LinComb V) st

for e1, e2 being Element of LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2)

for b_{1}, b_{2} being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) ) holds

b_{1} = b_{2}

end;
func LCAdd V -> BinOp of (LinComb V) means :Def17: :: RLVECT_2:def 17

for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);

existence for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);

ex b

for e1, e2 being Element of LinComb V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 defines LCAdd RLVECT_2:def 17 :

for V being RealLinearSpace

for b_{2} being BinOp of (LinComb V) holds

( b_{2} = LCAdd V iff for e1, e2 being Element of LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) );

for V being RealLinearSpace

for b

( b

definition

let V be RealLinearSpace;

ex b_{1} being Function of [:REAL,(LinComb V):],(LinComb V) st

for a being Real

for e being Element of LinComb V holds b_{1} . [a,e] = a * (@ e)

for b_{1}, b_{2} being Function of [:REAL,(LinComb V):],(LinComb V) st ( for a being Real

for e being Element of LinComb V holds b_{1} . [a,e] = a * (@ e) ) & ( for a being Real

for e being Element of LinComb V holds b_{2} . [a,e] = a * (@ e) ) holds

b_{1} = b_{2}

end;
func LCMult V -> Function of [:REAL,(LinComb V):],(LinComb V) means :Def18: :: RLVECT_2:def 18

for a being Real

for e being Element of LinComb V holds it . [a,e] = a * (@ e);

existence for a being Real

for e being Element of LinComb V holds it . [a,e] = a * (@ e);

ex b

for a being Real

for e being Element of LinComb V holds b

proof end;

uniqueness for b

for e being Element of LinComb V holds b

for e being Element of LinComb V holds b

b

proof end;

:: deftheorem Def18 defines LCMult RLVECT_2:def 18 :

for V being RealLinearSpace

for b_{2} being Function of [:REAL,(LinComb V):],(LinComb V) holds

( b_{2} = LCMult V iff for a being Real

for e being Element of LinComb V holds b_{2} . [a,e] = a * (@ e) );

for V being RealLinearSpace

for b

( b

for e being Element of LinComb V holds b

definition

let V be RealLinearSpace;

RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #) is RLSStruct ;

end;
func LC_RLSpace V -> RLSStruct equals :: RLVECT_2:def 19

RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

coherence RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #) is RLSStruct ;

:: deftheorem defines LC_RLSpace RLVECT_2:def 19 :

for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

registration
end;

registration

let V be RealLinearSpace;

( LC_RLSpace V is Abelian & LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

end;
cluster LC_RLSpace V -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( LC_RLSpace V is Abelian & LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

proof end;

theorem :: RLVECT_2:58

theorem Th62: :: RLVECT_2:62

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

for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2

proof end;

theorem Th63: :: RLVECT_2:63

for V being RealLinearSpace

for a being Real

for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

for a being Real

for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

proof end;

theorem Th64: :: RLVECT_2:64

for V being RealLinearSpace

for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L

for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L

proof end;

theorem :: RLVECT_2:65

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

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;

ex b_{1} being strict Subspace of LC_RLSpace V st the carrier of b_{1} = { l where l is Linear_Combination of A : verum }

for b_{1}, b_{2} being strict Subspace of LC_RLSpace V st the carrier of b_{1} = { l where l is Linear_Combination of A : verum } & the carrier of b_{2} = { l where l is Linear_Combination of A : verum } holds

b_{1} = b_{2}
by RLSUB_1:30;

end;
let A be Subset of V;

func LC_RLSpace A -> strict Subspace of LC_RLSpace V means :: RLVECT_2:def 20

the carrier of it = { l where l is Linear_Combination of A : verum } ;

existence the carrier of it = { l where l is Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem defines LC_RLSpace RLVECT_2:def 20 :

for V being RealLinearSpace

for A being Subset of V

for b_{3} being strict Subspace of LC_RLSpace V holds

( b_{3} = LC_RLSpace A iff the carrier of b_{3} = { l where l is Linear_Combination of A : verum } );

for V being RealLinearSpace

for A being Subset of V

for b

( b

theorem Th66: :: RLVECT_2:66

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

proof end;

theorem :: RLVECT_2:67

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence 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)

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for F, G being FinSequence 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 :: RLVECT_2:68

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being non empty right_complementable Abelian add-associative right_zeroed ModuleStr over R

for F, G, H being FinSequence 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)

for V being non empty right_complementable Abelian add-associative right_zeroed ModuleStr over R

for F, G, H being FinSequence 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:69

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R holds a * (Sum (<*> the carrier of V)) = 0. V

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R holds a * (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: RLVECT_2:70

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

proof end;

theorem :: RLVECT_2:71

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

for a being Element of R

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R

for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

proof end;