:: by Michal Muzalewski

::

:: Received October 18, 1991

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

begin

Lm1: for R being Ring

for a being Scalar of R st - a = 0. R holds

a = 0. R

proof end;

theorem Th1: :: MOD_3:1

for R being non empty non degenerated right_complementable add-associative right_zeroed doubleLoopStr holds 0. R <> - (1. R)

proof end;

theorem Th2: :: MOD_3:2

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

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

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)

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;

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 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 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: 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 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 R being Ring

for V being LeftMod of R

for A being Subset of V

for b

( b

theorem Th4: :: MOD_3:4

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 )

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

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

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

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

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 Th8: :: MOD_3:8

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

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

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

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 Th10: :: MOD_3:10

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

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

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

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

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)

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

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)

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;

:: 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 addF of V, the ZeroF of V, the lmult of V #) ) );

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 addF of V, the ZeroF of V, the lmult of V #) ) );

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

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

registration

let R be Ring;

ex b_{1} being LeftMod of R st

( b_{1} is strict & b_{1} is free )

end;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free for VectSpStr over R;

existence ex b

( b

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

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 )

for V being LeftMod of R

for v being Vector of V holds

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

proof end;

theorem Th16: :: MOD_3:16

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

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

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

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 Th18: :: MOD_3:18

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 )

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 Th19: :: MOD_3:19

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 )

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;

definition

let R be Skew-Field;

let V be LeftMod of R;

existence

ex b_{1} being Subset of V st b_{1} is base
by Lm3;

end;
let V be LeftMod of R;

existence

ex b

:: deftheorem Def4 defines Basis MOD_3:def 4 :

for R being Skew-Field

for V being LeftMod of R

for b_{3} being Subset of V holds

( b_{3} is Basis of V iff b_{3} is base );

for R being Skew-Field

for V being LeftMod of R

for b

( b

theorem :: MOD_3:21

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

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

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

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;