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

definition
let GF be Field;
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 = {} ;
end;

:: 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 = {} );

notation
let GF be Field;
let V be VectSp of GF;
let IT be Subset of V;
antonym linearly-dependent IT for linearly-independent IT;
end;

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

theorem :: VECTSP_7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th3: :: VECTSP_7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: VECTSP_7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GF being Field
for V being VectSp of GF holds {} the carrier of V is linearly-independent
proof end;

registration
let GF be Field;
let V be VectSp of GF;
cluster linearly-independent Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is linearly-independent
proof end;
end;

theorem :: VECTSP_7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th6: :: VECTSP_7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & v2 <> 0. V )
proof end;

theorem :: VECTSP_7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GF being Field
for V being VectSp of GF
for v being Vector of V holds
( not {v,(0. V)} is linearly-independent & not {(0. V),v} is linearly-independent ) by Th6;

theorem Th8: :: VECTSP_7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: VECTSP_7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

definition
let GF be Field;
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
ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2
by VECTSP_4:37;
end;

:: 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 b4 being strict Subspace of V holds
( b4 = Lin A iff the carrier of b4 = { (Sum l) where l is Linear_Combination of A : verum } );

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

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

theorem Th12: :: VECTSP_7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th13: :: VECTSP_7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: VECTSP_7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GF being Field
for V being VectSp of GF holds Lin ({} the carrier of V) = (0). V
proof end;

theorem :: VECTSP_7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)} )
proof end;

theorem Th16: :: VECTSP_7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: VECTSP_7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th18: :: VECTSP_7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: VECTSP_7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: VECTSP_7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: VECTSP_7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th22: :: VECTSP_7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 add of V,the Zero of V,the lmult of V #) )
proof end;

theorem Th23: :: VECTSP_7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let GF be Field;
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 add of V,the Zero of V,the lmult of V #) );
existence
ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = VectSpStr(# the carrier of V,the add of V,the Zero of V,the lmult of V #) )
proof end;
end;

:: deftheorem Def3 defines Basis VECTSP_7:def 3 :
for GF being Field
for V being VectSp of GF
for b3 being Subset of V holds
( b3 is Basis of V iff ( b3 is linearly-independent & Lin b3 = VectSpStr(# the carrier of V,the add of V,the Zero of V,the lmult of V #) ) );

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

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

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

theorem :: VECTSP_7:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: VECTSP_7:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;