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

Received October 22, 1990

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