:: by Wojciech A. Trybulec

::

:: Received July 10, 1990

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

begin

Lm1: for V being RealLinearSpace

for F, G being FinSequence of the carrier of V

for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

proof end;

theorem Th1: :: RLVECT_3:1

for V being RealLinearSpace

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

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

proof end;

theorem Th2: :: RLVECT_3:2

for a being Real

for V being RealLinearSpace

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

for V being RealLinearSpace

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

proof end;

theorem Th4: :: RLVECT_3:4

for V being RealLinearSpace

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

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

proof end;

definition

let V be RealLinearSpace;

let A be Subset of V;

end;
let A be Subset of V;

attr A is linearly-independent means :Def1: :: RLVECT_3:def 1

for l being Linear_Combination of A st Sum l = 0. V holds

Carrier l = {} ;

for l being Linear_Combination of A st Sum l = 0. V holds

Carrier l = {} ;

:: deftheorem Def1 defines linearly-independent RLVECT_3:def 1 :

for V being RealLinearSpace

for A being Subset of V holds

( A is linearly-independent iff for l being Linear_Combination of A st Sum l = 0. V holds

Carrier l = {} );

for V being RealLinearSpace

for A being Subset of V holds

( A is linearly-independent iff for l being Linear_Combination of A st Sum l = 0. V holds

Carrier l = {} );

notation

let V be RealLinearSpace;

let A be Subset of V;

antonym linearly-dependent A for linearly-independent ;

end;
let A be Subset of V;

antonym linearly-dependent A for linearly-independent ;

theorem :: RLVECT_3:5

for V being RealLinearSpace

for A, B being Subset of V st A c= B & B is linearly-independent holds

A is linearly-independent

for A, B being Subset of V st A c= B & B is linearly-independent holds

A is linearly-independent

proof end;

theorem Th6: :: RLVECT_3:6

for V being RealLinearSpace

for A being Subset of V st A is linearly-independent holds

not 0. V in A

for A being Subset of V st A is linearly-independent holds

not 0. V in A

proof end;

registration

let V be RealLinearSpace;

existence

ex b_{1} being Subset of V st b_{1} is linearly-independent

end;
existence

ex b

proof end;

theorem Th8: :: RLVECT_3:8

for V being RealLinearSpace

for v being VECTOR of V holds

( {v} is linearly-independent iff v <> 0. V )

for v being VECTOR of V holds

( {v} is linearly-independent iff v <> 0. V )

proof end;

theorem Th10: :: RLVECT_3:10

for V being RealLinearSpace

for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds

( v1 <> 0. V & v2 <> 0. V )

for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds

( v1 <> 0. V & v2 <> 0. V )

proof end;

theorem :: RLVECT_3:11

for V being RealLinearSpace

for v being VECTOR of V holds

( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th10;

for v being VECTOR of V holds

( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th10;

theorem Th12: :: RLVECT_3:12

for V being RealLinearSpace

for v1, v2 being VECTOR of V holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )

for v1, v2 being VECTOR of V holds

( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )

proof end;

theorem :: RLVECT_3:13

for V being RealLinearSpace

for v1, v2 being VECTOR of V holds

( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

for v1, v2 being VECTOR of V holds

( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

proof end;

definition

let V be RealLinearSpace;

let A be Subset of V;

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

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b_{2} = { (Sum 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 Lin A -> strict Subspace of V means :Def2: :: RLVECT_3:def 2

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

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

ex b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines Lin RLVECT_3:def 2 :

for V being RealLinearSpace

for A being Subset of V

for b_{3} being strict Subspace of V holds

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

for V being RealLinearSpace

for A being Subset of V

for b

( b

theorem Th14: :: RLVECT_3:14

for x being set

for V being RealLinearSpace

for A being Subset of V holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

for V being RealLinearSpace

for A being Subset of V holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

proof end;

Lm2: for x being set

for V being RealLinearSpace holds

( x in (0). V iff x = 0. V )

proof end;

theorem :: RLVECT_3:17

for V being RealLinearSpace

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

proof end;

theorem Th18: :: RLVECT_3:18

for V being RealLinearSpace

for A being Subset of V

for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

for A being Subset of V

for W being strict Subspace of V st A = the carrier of W holds

Lin A = W

proof end;

Lm3: for V being RealLinearSpace

for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds

W1 /\ W2 is Subspace of W3

proof end;

Lm4: for V being RealLinearSpace

for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds

W1 is Subspace of W2 /\ W3

proof end;

Lm5: for V being RealLinearSpace

for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds

W1 is Subspace of W2 + W3

proof end;

Lm6: for V being RealLinearSpace

for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds

W1 + W2 is Subspace of W3

proof end;

theorem :: RLVECT_3:23

for V being RealLinearSpace

for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

proof end;

Lm7: for M being non empty set

for CF being Choice_Function of M st not {} in M holds

dom CF = M

proof end;

theorem Th24: :: RLVECT_3:24

for V being RealLinearSpace

for A being Subset of V st A is linearly-independent holds

ex B being Subset of V st

( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )

for A being Subset of V st A is linearly-independent holds

ex B being Subset of V st

( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )

proof end;

theorem Th25: :: RLVECT_3:25

for V being RealLinearSpace

for A being Subset of V st Lin A = V holds

ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

for A being Subset of V st Lin A = V holds

ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

proof end;

definition

let V be RealLinearSpace;

ex b_{1} being Subset of V st

( b_{1} is linearly-independent & Lin b_{1} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )

end;
mode Basis of V -> Subset of V means :Def3: :: RLVECT_3:def 3

( it is linearly-independent & Lin it = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) );

existence ( it is linearly-independent & Lin it = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) );

ex b

( b

proof end;

:: deftheorem Def3 defines Basis RLVECT_3:def 3 :

for V being RealLinearSpace

for b_{2} being Subset of V holds

( b_{2} is Basis of V iff ( b_{2} is linearly-independent & Lin b_{2} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) );

for V being RealLinearSpace

for b

( b

theorem :: RLVECT_3:26

for V being strict RealLinearSpace

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

proof end;

theorem :: RLVECT_3:27

for V being RealLinearSpace

for A being Subset of V st Lin A = V holds

ex I being Basis of V st I c= A

for A being Subset of V st Lin A = V holds

ex I being Basis of V st I c= A

proof end;

theorem :: RLVECT_3:28

theorem :: RLVECT_3:29

theorem :: RLVECT_3:30

theorem :: RLVECT_3:31

theorem :: RLVECT_3:32

theorem :: RLVECT_3:33

theorem :: RLVECT_3:34

:: Auxiliary theorems.

::