:: by Wojciech A. Trybulec

::

:: Received July 27, 1990

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

begin

definition

let GF be Field;

let V be VectSp of GF;

let IT be Subset of V;

end;
let V be VectSp of GF;

let IT be Subset of V;

attr IT is linearly-independent means :Def1: :: VECTSP_7:def 1

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

Carrier l = {} ;

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

Carrier l = {} ;

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

for GF being Field

for V being VectSp of GF

for IT being Subset of V holds

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

Carrier l = {} );

for GF being Field

for V being VectSp of GF

for IT being Subset of V holds

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

Carrier l = {} );

notation

let GF be Field;

let V be VectSp of GF;

let IT be Subset of V;

antonym linearly-dependent IT for linearly-independent ;

end;
let V be VectSp of GF;

let IT be Subset of V;

antonym linearly-dependent IT for linearly-independent ;

theorem :: VECTSP_7:1

for GF being Field

for V being VectSp of GF

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

A is linearly-independent

for V being VectSp of GF

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

A is linearly-independent

proof end;

theorem Th2: :: VECTSP_7:2

for GF being Field

for V being VectSp of GF

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

not 0. V in A

for V being VectSp of GF

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

not 0. V in A

proof end;

registration

let GF be Field;

let V be VectSp of GF;

coherence

for b_{1} being Subset of V st b_{1} is empty holds

b_{1} is linearly-independent

end;
let V be VectSp of GF;

coherence

for b

b

proof end;

registration

let GF be Field;

let V be VectSp of GF;

existence

ex b_{1} being Subset of V st

( b_{1} is finite & b_{1} is linearly-independent )

end;
let V be VectSp of GF;

existence

ex b

( b

proof end;

theorem :: VECTSP_7:3

for GF being Field

for V being VectSp of GF

for v being Vector of V holds

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

for V being VectSp of GF

for v being Vector of V holds

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

proof end;

theorem Th4: :: VECTSP_7:4

for GF being Field

for V being VectSp of GF

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

v1 <> 0. V

for V being VectSp of GF

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

v1 <> 0. V

proof end;

theorem Th5: :: VECTSP_7:5

for GF being Field

for V being VectSp of GF

for v1, v2 being Vector of V holds

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

for V being VectSp of GF

for v1, v2 being Vector of V holds

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

proof end;

theorem :: VECTSP_7:6

for GF being Field

for V being VectSp of GF

for v1, v2 being Vector of V holds

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

( a = 0. GF & b = 0. GF ) )

for V being VectSp of GF

for v1, v2 being Vector of V holds

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

( a = 0. GF & b = 0. GF ) )

proof end;

definition

let GF be Field;

let V be VectSp of GF;

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 VECTSP_4:29;

end;
let V be VectSp of GF;

let A be Subset of V;

func Lin A -> strict Subspace of V means :Def2: :: VECTSP_7: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 VECTSP_7:def 2 :

for GF being Field

for V being VectSp of GF

for A being Subset of V

for b_{4} being strict Subspace of V holds

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

for GF being Field

for V being VectSp of GF

for A being Subset of V

for b

( b

theorem Th7: :: VECTSP_7:7

for x being set

for GF being Field

for V being VectSp of GF

for A being Subset of V holds

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

for GF being Field

for V being VectSp of GF

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;

theorem Th8: :: VECTSP_7:8

for x being set

for GF being Field

for V being VectSp of GF

for A being Subset of V st x in A holds

x in Lin A

for GF being Field

for V being VectSp of GF

for A being Subset of V st x in A holds

x in Lin A

proof end;

theorem :: VECTSP_7:10

for GF being Field

for V being VectSp of GF

for A being Subset of V holds

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

for V being VectSp of GF

for A being Subset of V holds

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

proof end;

theorem Th11: :: VECTSP_7:11

for GF being Field

for V being VectSp of GF

for A being Subset of V

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

Lin A = W

for V being VectSp of GF

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;

theorem :: VECTSP_7:12

for GF being Field

for V being strict VectSp of GF

for A being Subset of V st A = the carrier of V holds

Lin A = V

for V being strict VectSp of GF

for A being Subset of V st A = the carrier of V holds

Lin A = V

proof end;

theorem Th13: :: VECTSP_7:13

for GF being Field

for V being VectSp of GF

for A, B being Subset of V st A c= B holds

Lin A is Subspace of Lin B

for V being VectSp of GF

for A, B being Subset of V st A c= B holds

Lin A is Subspace of Lin B

proof end;

theorem :: VECTSP_7:14

for GF being Field

for V being strict VectSp of GF

for A, B being Subset of V st Lin A = V & A c= B holds

Lin B = V

for V being strict VectSp of GF

for A, B being Subset of V st Lin A = V & A c= B holds

Lin B = V

proof end;

theorem :: VECTSP_7:15

for GF being Field

for V being VectSp of GF

for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)

for V being VectSp of GF

for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)

proof end;

theorem :: VECTSP_7:16

for GF being Field

for V being VectSp of GF

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

for V being VectSp of GF

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

proof end;

theorem Th17: :: VECTSP_7:17

for GF being Field

for V being VectSp of GF

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 = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )

for V being VectSp of GF

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 = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )

proof end;

theorem Th18: :: VECTSP_7:18

for GF being Field

for V being VectSp of GF

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 V being VectSp of GF

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 GF be Field;

let V be VectSp of GF;

ex b_{1} being Subset of V st

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

end;
let V be VectSp of GF;

mode Basis of V -> Subset of V means :Def3: :: VECTSP_7:def 3

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

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

ex b

( b

proof end;

:: deftheorem Def3 defines Basis VECTSP_7:def 3 :

for GF being Field

for V being VectSp of GF

for b_{3} being Subset of V holds

( b_{3} is Basis of V iff ( b_{3} is linearly-independent & Lin b_{3} = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) );

for GF being Field

for V being VectSp of GF

for b

( b

theorem :: VECTSP_7:19

for GF being Field

for V being VectSp of GF

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

ex I being Basis of V st A c= I

for V being VectSp of GF

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

for GF being Field

for V being VectSp of GF

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

ex I being Basis of V st I c= A

for V being VectSp of GF

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

ex I being Basis of V st I c= A

proof end;