:: Linear Combinations in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
proofend;

theorem Th1: :: RMOD_4:1
for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
proofend;

Lm2:  for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
proofend;

theorem :: RMOD_4:2
for R being Ring
for V being RightMod of R
for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
proofend;

theorem :: RMOD_4:3
for R being Ring
for V being RightMod of R
for a being Scalar of R
for v, u being Vector of V holds (Sum <*v,u*>) * a = (v * a) + (u * a)
proofend;

theorem :: RMOD_4:4
for R being Ring
for V being RightMod of R
for a being Scalar of R
for v, u, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
proofend;

definition
let R be Ring;
let V be RightMod of R;
let T be finite Subset of V;
func Sum T ->  Vector of V means :Def1: :: RMOD_4:def 1
 ex F being FinSequence of V st
( rng F = T &amp; F is one-to-one &amp; it = Sum F );
existence
 ex b1 being Vector of V ex F being FinSequence of V st
( rng F = T &amp; F is one-to-one &amp; b1 = Sum F )
proofend;
uniqueness
 for b1, b2 being Vector of V st ex F being FinSequence of V st
( rng F = T &amp; F is one-to-one &amp; b1 = Sum F ) &amp; ex F being FinSequence of V st
( rng F = T &amp; F is one-to-one &amp; b2 = Sum F ) holds
b1 = b2 by RLVECT_1:42;
end;

:: deftheorem Def1 defines Sum RMOD_4:def_1_:_
 for R being Ring
for V being RightMod of R
for T being finite Subset of V
for b4 being Vector of V holds
( b4 = Sum T iff ex F being FinSequence of V st
( rng F = T &amp; F is one-to-one &amp; b4 = Sum F ) );

theorem Th5: :: RMOD_4:5
for R being Ring
for V being RightMod of R holds Sum ({} V) = 0. V
proofend;

theorem :: RMOD_4:6
for R being Ring
for V being RightMod of R
for v being Vector of V holds Sum {v} = v
proofend;

theorem :: RMOD_4:7
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
proofend;

theorem :: RMOD_4:8
for R being Ring
for V being RightMod of R
for v1, v2, v3 being Vector of V st v1 <> v2 &amp; v2 <> v3 &amp; v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
proofend;

theorem Th9: :: RMOD_4:9
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
proofend;

theorem Th10: :: RMOD_4:10
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
proofend;

theorem :: RMOD_4:11
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S))
proofend;

theorem Th12: :: RMOD_4:12
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)
proofend;

theorem Th13: :: RMOD_4:13
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
proofend;

theorem :: RMOD_4:14
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
proofend;

theorem :: RMOD_4:15
for R being Ring
for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th9, XBOOLE_1:82;

definition
let R be Ring;
let V be RightMod of R;
mode Linear_Combination of V ->  Element of Funcs ( the carrier of V, the carrier of R) means :Def2: :: RMOD_4:def 2
 ex T being finite Subset of V st
for v being Vector of V st not v in T holds
it . v = 0. R;
existence
 ex b1 being Element of Funcs ( the carrier of V, the carrier of R) ex T being finite Subset of V st
for v being Vector of V st not v in T holds
b1 . v = 0. R
proofend;
end;

:: deftheorem Def2 defines Linear_Combination RMOD_4:def_2_:_
 for R being Ring
for V being RightMod of R
for b3 being Element of Funcs ( the carrier of V, the carrier of R) holds
( b3 is Linear_Combination of V iff ex T being finite Subset of V st
for v being Vector of V st not v in T holds
b3 . v = 0. R );

definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func Carrier L ->  finite Subset of V equals :: RMOD_4:def 3
 {  v where v is Vector of V : L . v <> 0. R  }  ;
coherence
  {  v where v is Vector of V : L . v <> 0. R  }  is finite Subset of V
proofend;
end;

:: deftheorem  defines Carrier RMOD_4:def_3_:_
 for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds Carrier L =  {  v where v is Vector of V : L . v <> 0. R  }  ;

theorem :: RMOD_4:16
for R being Ring
for V being RightMod of R
for x being set
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Vector of V st
( x = v &amp; L . v <> 0. R ) ) ;

theorem :: RMOD_4:17
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds
( L . v = 0. R iff not v in Carrier L )
proofend;

definition
let R be Ring;
let V be RightMod of R;
func ZeroLC V ->  Linear_Combination of V means :Def4: :: RMOD_4:def 4
 Carrier it = {} ;
existence
 ex b1 being Linear_Combination of V st Carrier b1 = {}
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st Carrier b1 = {} &amp; Carrier b2 = {} holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines ZeroLC RMOD_4:def_4_:_
 for R being Ring
for V being RightMod of R
for b3 being Linear_Combination of V holds
( b3 = ZeroLC V iff Carrier b3 = {} );

theorem Th18: :: RMOD_4:18
for R being Ring
for V being RightMod of R
for v being Vector of V holds (ZeroLC V) . v = 0. R
proofend;

definition
let R be Ring;
let V be RightMod of R;
let A be Subset of V;
mode Linear_Combination of A ->  Linear_Combination of V means :Def5: :: RMOD_4:def 5
 Carrier it c= A;
existence
 ex b1 being Linear_Combination of V st Carrier b1 c= A
proofend;
end;

:: deftheorem Def5 defines Linear_Combination RMOD_4:def_5_:_
 for R being Ring
for V being RightMod of R
for A being Subset of V
for b4 being Linear_Combination of V holds
( b4 is Linear_Combination of A iff Carrier b4 c= A );

theorem Th19: :: RMOD_4:19
for R being Ring
for V being RightMod of R
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
proofend;

theorem Th20: :: RMOD_4:20
for R being Ring
for V being RightMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proofend;

theorem Th21: :: RMOD_4:21
for R being Ring
for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proofend;

theorem :: RMOD_4:22
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def5;

definition
let R be Ring;
let V be RightMod of R;
let F be FinSequence of V;
let f be Function of V,R;
funcf (#) F ->  FinSequence of V means :Def6: :: RMOD_4:def 6
( len it = len F &amp; ( for i being Nat st i in dom it holds
it . i = (F /. i) * (f . (F /. i)) ) );
existence
 ex b1 being FinSequence of V st
( len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (F /. i) * (f . (F /. i)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of V st len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (F /. i) * (f . (F /. i)) ) &amp; len b2 = len F &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (F /. i) * (f . (F /. i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines (#) RMOD_4:def_6_:_
 for R being Ring
for V being RightMod of R
for F being FinSequence of V
for f being Function of V,R
for b5 being FinSequence of V holds
( b5 = f (#) F iff ( len b5 = len F &amp; ( for i being Nat st i in dom b5 holds
b5 . i = (F /. i) * (f . (F /. i)) ) ) );

theorem Th23: :: RMOD_4:23
for R being Ring
for V being RightMod of R
for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F &amp; v = F . i holds
(f (#) F) . i = v * (f . v)
proofend;

theorem :: RMOD_4:24
for R being Ring
for V being RightMod of R
for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V
proofend;

theorem Th25: :: RMOD_4:25
for R being Ring
for V being RightMod of R
for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
proofend;

theorem Th26: :: RMOD_4:26
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2*> = <*(v1 * (f . v1)),(v2 * (f . v2))*>
proofend;

theorem :: RMOD_4:27
for R being Ring
for V being RightMod of R
for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
proofend;

theorem Th28: :: RMOD_4:28
for R being Ring
for V being RightMod of R
for F, G being FinSequence of V
for f being Function of V,R holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proofend;

definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func Sum L ->  Vector of V means :Def7: :: RMOD_4:def 7
 ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; it = Sum (L (#) F) );
existence
 ex b1 being Vector of V ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) )
proofend;
uniqueness
 for b1, b2 being Vector of V st ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) ) &amp; ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b2 = Sum (L (#) F) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Sum RMOD_4:def_7_:_
 for R being Ring
for V being RightMod of R
for L being Linear_Combination of V
for b4 being Vector of V holds
( b4 = Sum L iff ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b4 = Sum (L (#) F) ) );

Lm3:  for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V
proofend;

theorem Th29: :: RMOD_4:29
for R being Ring
for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R holds
( ( A <> {} &amp; A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proofend;

theorem :: RMOD_4:30
for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V by Lm3;

theorem Th31: :: RMOD_4:31
for R being Ring
for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proofend;

theorem Th32: :: RMOD_4:32
for R being Ring
for V being RightMod of R
for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
proofend;

theorem Th33: :: RMOD_4:33
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
proofend;

theorem :: RMOD_4:34
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proofend;

theorem Th35: :: RMOD_4:35
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = v * (L . v)
proofend;

theorem :: RMOD_4:36
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V
for L being Linear_Combination of V st Carrier L = {v1,v2} &amp; v1 <> v2 holds
Sum L = (v1 * (L . v1)) + (v2 * (L . v2))
proofend;

definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
:: original:=
redefine predL1 = L2 means :: RMOD_4:def 8
 for v being Vector of V holds L1 . v = L2 . v;
compatibility
 ( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;

:: deftheorem  defines = RMOD_4:def_8_:_
 for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Vector of V holds L1 . v = L2 . v );

definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
funcL1 + L2 ->  Linear_Combination of V means :Def9: :: RMOD_4:def 9
 for v being Vector of V holds it . v = (L1 . v) + (L2 . v);
existence
 ex b1 being Linear_Combination of V st
for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v)
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L1 . v) + (L2 . v) ) &amp; ( for v being Vector of V holds b2 . v = (L1 . v) + (L2 . v) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines + RMOD_4:def_9_:_
 for R being Ring
for V being RightMod of R
for L1, L2, b5 being Linear_Combination of V holds
( b5 = L1 + L2 iff for v being Vector of V holds b5 . v = (L1 . v) + (L2 . v) );

theorem Th37: :: RMOD_4:37
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem Th38: :: RMOD_4:38
for R being Ring
for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A &amp; L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
proofend;

theorem Th39: :: RMOD_4:39
for R being comRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
proofend;

theorem :: RMOD_4:40
for R being Ring
for V being RightMod of R
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proofend;

theorem :: RMOD_4:41
for R being comRing
for V being RightMod of R
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L &amp; (ZeroLC V) + L = L )
proofend;

definition
let R be Ring;
let V be RightMod of R;
let a be Scalar of R;
let L be Linear_Combination of V;
funcL * a ->  Linear_Combination of V means :Def10: :: RMOD_4:def 10
 for v being Vector of V holds it . v = (L . v) * a;
existence
 ex b1 being Linear_Combination of V st
for v being Vector of V holds b1 . v = (L . v) * a
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being Vector of V holds b1 . v = (L . v) * a ) &amp; ( for v being Vector of V holds b2 . v = (L . v) * a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines * RMOD_4:def_10_:_
 for R being Ring
for V being RightMod of R
for a being Scalar of R
for L, b5 being Linear_Combination of V holds
( b5 = L * a iff for v being Vector of V holds b5 . v = (L . v) * a );

theorem Th42: :: RMOD_4:42
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L being Linear_Combination of V holds Carrier (L * a) c= Carrier L
proofend;

theorem Th43: :: RMOD_4:43
for RR being domRing
for VV being RightMod of RR
for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
proofend;

theorem Th44: :: RMOD_4:44
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L * (0. R) = ZeroLC V
proofend;

theorem Th45: :: RMOD_4:45
for R being Ring
for V being RightMod of R
for a being Scalar of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A
proofend;

theorem :: RMOD_4:46
for R being Ring
for V being RightMod of R
for a, b being Scalar of R
for L being Linear_Combination of V holds L * (a + b) = (L * a) + (L * b)
proofend;

theorem :: RMOD_4:47
for R being Ring
for V being RightMod of R
for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
proofend;

theorem Th48: :: RMOD_4:48
for R being Ring
for V being RightMod of R
for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
proofend;

theorem :: RMOD_4:49
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L * (1_ R) = L
proofend;

definition
let R be Ring;
let V be RightMod of R;
let L be Linear_Combination of V;
func - L ->  Linear_Combination of V equals :: RMOD_4:def 11
L * (- (1_ R));
correctness
coherence
L * (- (1_ R)) is Linear_Combination of V;
;
involutiveness
 for b1, b2 being Linear_Combination of V st b1 = b2 * (- (1_ R)) holds
b2 = b1 * (- (1_ R))
proofend;
end;

:: deftheorem  defines - RMOD_4:def_11_:_
 for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds - L = L * (- (1_ R));

theorem Th50: :: RMOD_4:50
for R being Ring
for V being RightMod of R
for v being Vector of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proofend;

theorem :: RMOD_4:51
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proofend;

theorem Th52: :: RMOD_4:52
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
proofend;

theorem :: RMOD_4:53
for R being Ring
for V being RightMod of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by Th45;

definition
let R be Ring;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 ->  Linear_Combination of V equals :: RMOD_4:def 12
L1 + (- L2);
correctness
coherence
L1 + (- L2) is Linear_Combination of V;
;
end;

:: deftheorem  defines - RMOD_4:def_12_:_
 for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th54: :: RMOD_4:54
for R being Ring
for V being RightMod of R
for v being Vector of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proofend;

theorem :: RMOD_4:55
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem :: RMOD_4:56
for R being Ring
for V being RightMod of R
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A &amp; L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
proofend;

theorem :: RMOD_4:57
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds L - L = ZeroLC V
proofend;

theorem Th58: :: RMOD_4:58
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proofend;

theorem Th59: :: RMOD_4:59
for R being domRing
for V being RightMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (L * a) = (Sum L) * a
proofend;

theorem Th60: :: RMOD_4:60
for R being domRing
for V being RightMod of R
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proofend;

theorem :: RMOD_4:61
for R being domRing
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proofend;

begin

definition
let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
attrIT is linearly-independent  means :Def13: :: RMOD_4:def 13
 for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} ;
end;

:: deftheorem Def13 defines linearly-independent RMOD_4:def_13_:_
 for R being Ring
for V being RightMod of R
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );

notation
let R be Ring;
let V be RightMod of R;
let IT be Subset of V;
antonym  linearly-dependent IT for  linearly-independent ;
end;

theorem :: RMOD_4:62
for R being Ring
for V being RightMod of R
for A, B being Subset of V st A c= B &amp; B is linearly-independent holds
A is linearly-independent
proofend;

theorem Th63: :: RMOD_4:63
for R being Ring
for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R &amp; A is linearly-independent holds
not 0. V in A
proofend;

theorem :: RMOD_4:64
for R being Ring
for V being RightMod of R holds {} the carrier of V is linearly-independent
proofend;

theorem Th65: :: RMOD_4:65
for R being Ring
for V being RightMod of R
for v1, v2 being Vector of V st 0. R <> 1_ R &amp; {v1,v2} is linearly-independent holds
( v1 <> 0. V &amp; v2 <> 0. V )
proofend;

theorem :: RMOD_4:66
for R being Ring
for V being RightMod of R
for v being Vector of V st 0. R <> 1_ R holds
( {v,(0. V)} is linearly-dependent &amp; {(0. V),v} is linearly-dependent ) by Th65;

definition
let R be domRing;
let V be RightMod of R;
let A be Subset of V;
func Lin A ->  strict Submodule of V means :Def14: :: RMOD_4:def 14
 the carrier of it =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Submodule of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }
proofend;
uniqueness
 for b1, b2 being strict Submodule of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  &amp; the carrier of b2 =  {  (Sum l) where l is Linear_Combination of A : verum  }  holds
b1 = b2 by RMOD_2:29;
end;

:: deftheorem Def14 defines Lin RMOD_4:def_14_:_
 for R being domRing
for V being RightMod of R
for A being Subset of V
for b4 being strict Submodule of V holds
( b4 = Lin A iff the carrier of b4 =  {  (Sum l) where l is Linear_Combination of A : verum  }  );

theorem Th67: :: RMOD_4:67
for x being set
for R being domRing
for V being RightMod 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 )
proofend;

theorem Th68: :: RMOD_4:68
for x being set
for R being domRing
for V being RightMod of R
for A being Subset of V st x in A holds
x in Lin A
proofend;

theorem :: RMOD_4:69
for R being domRing
for V being RightMod of R holds Lin ({} the carrier of V) = (0). V
proofend;

theorem :: RMOD_4:70
for R being domRing
for V being RightMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proofend;

theorem Th71: :: RMOD_4:71
for R being domRing
for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R &amp; A = the carrier of W holds
Lin A = W
proofend;

theorem :: RMOD_4:72
for R being domRing
for V being strict RightMod of R
for A being Subset of V st 0. R <> 1_ R &amp; A = the carrier of V holds
Lin A = V
proofend;

theorem Th73: :: RMOD_4:73
for R being domRing
for V being RightMod of R
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
proofend;

theorem :: RMOD_4:74
for R being domRing
for V being strict RightMod of R
for A, B being Subset of V st Lin A = V &amp; A c= B holds
Lin B = V
proofend;

theorem :: RMOD_4:75
for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proofend;

theorem :: RMOD_4:76
for R being domRing
for V being RightMod of R
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B)
proofend;