Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Linear Independence in Right Module over Domain

by
Michal Muzalewski, and
Wojciech Skaba

MML identifier: RMOD_5
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCSDOM, VECTSP_2, VECTSP_1, RLVECT_3, RLVECT_2, RLVECT_1, BOOLE,
FUNCT_1, FUNCT_2, FINSET_1, LMOD_4, RLSUB_1;
notation TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, FUNCT_1, FUNCT_2, FRAENKEL,
STRUCT_0, RLVECT_1, RLVECT_2, VECTSP_1, FUNCSDOM, VECTSP_2, RMOD_2,
RMOD_3, RMOD_4;
constructors RLVECT_2, RMOD_3, RMOD_4, MEMBERED, XBOOLE_0;
clusters VECTSP_2, RMOD_2, STRUCT_0, RELSET_1, SUBSET_1, RLVECT_2, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x for set;
reserve R for Ring;
reserve V for RightMod of R;

reserve v,v1,v2 for Vector of V;
reserve A,B for Subset of V;

definition let R; let V;
let IT be Subset of V;
attr IT is linearly-independent means
:: RMOD_5:def 1
for l being Linear_Combination of IT
st Sum(l) = 0.V holds Carrier(l) = {};
antonym IT is linearly-dependent;
end;

canceled;

theorem :: RMOD_5:2
A c= B & B is linearly-independent implies A is linearly-independent;

theorem :: RMOD_5:3
0.R <> 1_ R & A is linearly-independent
implies not 0.V in A;

theorem :: RMOD_5:4
{}(the carrier of V) is linearly-independent;

theorem :: RMOD_5:5
0.R <> 1_ R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;

theorem :: RMOD_5:6
0.R <> 1_ R implies
{v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent;

reserve R for domRing;
reserve V for RightMod of R;
reserve v,u for Vector of V;
reserve A,B for Subset of V;
reserve l for Linear_Combination of A;
reserve f,g for Function of the carrier of V, the carrier of R;

definition let R; let V; let A;
func Lin(A) -> strict Submodule of V means
:: RMOD_5:def 2
the carrier of it = {Sum(l) : not contradiction};
end;

canceled 2;

theorem :: RMOD_5:9
x in Lin(A) iff ex l st x = Sum(l);

theorem :: RMOD_5:10
x in A implies x in Lin(A);

theorem :: RMOD_5:11
Lin({}(the carrier of V)) = (0).V;

theorem :: RMOD_5:12
Lin(A) = (0).V implies A = {} or A = {0.V};

theorem :: RMOD_5:13
for W being strict Submodule of V st 0.R <> 1_ R &
A = the carrier of W
holds Lin(A) = W;

theorem :: RMOD_5:14
for V being strict RightMod of R, A being Subset of V st
0.R <> 1_ R &
A = the carrier of V holds Lin(A) = V;

theorem :: RMOD_5:15
A c= B implies Lin(A) is Submodule of Lin(B);

theorem :: RMOD_5:16
for V being strict RightMod of R, A,B being Subset of V
st Lin(A) = V & A c= B holds Lin(B) = V;

theorem :: RMOD_5:17
Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: RMOD_5:18
Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B);
```