:: Free Modules
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users


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 :: 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) ) by VECTSP_7:21;

theorem :: 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) by VECTSP_7:22;

theorem Th4: :: MOD_3:4
for x being object
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 ) by VECTSP_7:7;

theorem Th5: :: MOD_3:5
for x being object
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 by VECTSP_7:8;

theorem Th6: :: MOD_3:6
for R being Ring
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V by VECTSP_7:9;

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)} ) by VECTSP_7:10;

theorem Th8: :: MOD_3:8
for R being non degenerated Ring
for V being LeftMod of R
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 :: MOD_3:9
for R being non degenerated Ring
for V being strict LeftMod of R
for A being Subset of V st 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 by VECTSP_7:13;

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
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) by VECTSP_7:15;

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) by VECTSP_7:16;

theorem Th14: :: MOD_3:14
for R being Ring
for V being LeftMod of R holds (0). V is free
proof end;

registration
let R be Ring;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free for ModuleStr over 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: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 )
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 ) ) )
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 ) )
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 )
proof end;

theorem Th19: :: MOD_3:19
for R being non degenerated almost_left_invertible Ring
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 non degenerated almost_left_invertible Ring
for V being LeftMod of R ex B being Subset of V st B is base

proof end;

registration
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R;
cluster base for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is base
proof end;
end;

theorem :: MOD_3:20
for R being Skew-Field
for V being LeftMod of R holds V is free by Lm3;

registration
let R be Skew-Field;
cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed -> free for ModuleStr over R;
coherence
for b1 being LeftMod of R holds b1 is free
by Lm3;
end;

theorem :: MOD_3:21
for R being non degenerated almost_left_invertible Ring
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
proof end;