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

Lm1: for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
proof end;

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

theorem Th2: :: MOD_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty add-associative right_zeroed right_complementable non degenerated doubleLoopStr holds 0. R <> - (1. R)
proof end;

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

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

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

theorem Th6: :: MOD_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
proof end;

theorem Th7: :: MOD_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
proof end;

definition
let R be Ring;
let V be LeftMod of R;
let A be Subset of V;
func Lin A -> strict Subspace of V means :Def1: :: MOD_3:def 1
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 Def1 defines Lin MOD_3:def 1 :
for R being Ring
for V being LeftMod of R
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 :: MOD_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

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

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

theorem Th11: :: MOD_3:11  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 R being Ring
for V being LeftMod of R
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 Th12: :: MOD_3: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 R being Ring
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
proof end;

theorem Th13: :: MOD_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
proof end;

theorem :: MOD_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof end;

theorem Th15: :: MOD_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
proof end;

theorem :: MOD_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being strict LeftMod of R
for A being Subset of V st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
proof end;

theorem Th17: :: MOD_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof end;

theorem :: MOD_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof end;

theorem :: MOD_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof end;

theorem :: MOD_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof end;

definition
let R be Ring;
let V be LeftMod of R;
let IT be Subset of V;
attr IT is base means :Def2: :: MOD_3:def 2
( IT is linearly-independent & Lin IT = VectSpStr(# the carrier of V,the add of V,the Zero of V,the lmult of V #) );
end;

:: deftheorem Def2 defines base MOD_3:def 2 :
for R being Ring
for V being LeftMod of R
for IT being Subset of V holds
( IT is base iff ( IT is linearly-independent & Lin IT = VectSpStr(# the carrier of V,the add of V,the Zero of V,the lmult of V #) ) );

definition
let R be Ring;
let IT be LeftMod of R;
attr IT is free means :Def3: :: MOD_3:def 3
ex B being Subset of IT st B is base;
end;

:: deftheorem Def3 defines free MOD_3:def 3 :
for R being Ring
for IT being LeftMod of R holds
( IT is free iff ex B being Subset of IT st B is base );

theorem Th21: :: MOD_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Ring
for V being LeftMod of R holds (0). V is free
proof end;

registration
let R be Ring;
cluster strict free VectSpStr of R;
existence
ex b1 being LeftMod of R st
( b1 is strict & b1 is free )
proof end;
end;

Lm2: for R being Skew-Field
for a being Scalar of R
for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a " ) * (a * v) = (1. R) * v & ((a " ) * a) * v = (1. R) * v )
proof end;

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

theorem :: MOD_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
proof end;

theorem Th24: :: MOD_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) )
proof end;

theorem :: MOD_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
proof end;

theorem Th26: :: MOD_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is base )
proof end;

theorem Th27: :: MOD_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
proof end;

Lm3: for R being Skew-Field
for V being LeftMod of R ex B being Subset of V st B is base
proof end;

theorem :: MOD_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R holds V is free
proof end;

definition
let R be Skew-Field;
let V be LeftMod of R;
canceled;
mode Basis of V -> Subset of V means :Def5: :: MOD_3:def 5
it is base;
existence
ex b1 being Subset of V st b1 is base
by Lm3;
end;

:: deftheorem MOD_3:def 4 :
canceled;

:: deftheorem Def5 defines Basis MOD_3:def 5 :
for R being Skew-Field
for V being LeftMod of R
for b3 being Subset of V holds
( b3 is Basis of V iff b3 is base );

theorem :: MOD_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
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 :: MOD_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof end;