:: LMOD_5 semantic presentation

begin


definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let IT be Subset of V;
attrIT is linearly-independent  means :Def1: :: LMOD_5:def 1
 for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} ;
end;

:: deftheorem Def1 defines linearly-independent LMOD_5:def_1_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over 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 non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let IT be Subset of V;
antonym  linearly-dependent IT for  linearly-independent ;
end;

theorem :: LMOD_5:1
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let V be LeftMod of R; ::_thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; ::_thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; ::_thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to LMOD_5:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, VECTSP_6:4;
assume  Sum l = 0. V ; ::_thesis: Carrier l = {}
then  Carrier L = {} by A2, Def1;
hence  Carrier l = {} ; ::_thesis: verum
end;

theorem Th2: :: LMOD_5:2
for R being Ring
for V being LeftMod of R
for A being Subset of V st 0. R <> 1. R & A is linearly-independent holds
not 0. V in A
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A being Subset of V st 0. R <> 1. R & A is linearly-independent holds
not 0. V in A
let V be LeftMod of R; ::_thesis: for A being Subset of V st 0. R <> 1. R & A is linearly-independent holds
not 0. V in A
let A be Subset of V; ::_thesis: ( 0. R <> 1. R & A is linearly-independent implies not 0. V in A )
assume that
A1: 0. R <> 1. R and
A2: A is linearly-independent and
A3: 0. V in A ; ::_thesis: contradiction
deffunc H1( set ) ->  Element of the carrier of R = 0. R;
consider f being Function of the carrier of V, the carrier of R such that
A4: f . (0. V) = 1. R and
A5: for v being Element of V st v <> 0. V holds
f . v = H1(v) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
 ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. R
proof
take T = {(0. V)}; ::_thesis: for v being Vector of V st not v in T holds
f . v = 0. R
let v be Vector of V; ::_thesis: ( not v in T implies f . v = 0. R )
assume  not v in T ; ::_thesis: f . v = 0. R
then  v <> 0. V by TARSKI:def_1;
hence  f . v = 0. R by A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A6: Carrier f = {(0. V)}
proof
thus  Carrier f c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {(0. V)} )
assume  x in Carrier f ; ::_thesis: x in {(0. V)}
then consider v being Vector of V such that
A7: v = x and
A8: f . v <> 0. R ;
 v = 0. V by A5, A8;
hence  x in {(0. V)} by A7, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in Carrier f )
assume  x in {(0. V)} ; ::_thesis: x in Carrier f
then  x = 0. V by TARSKI:def_1;
hence  x in Carrier f by A1, A4; ::_thesis: verum
end;
then  Carrier f c= A by A3, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
Sum f = (f . (0. V)) * (0. V) by A6, VECTSP_6:20
.= 0. V by VECTSP_1:14 ;
hence  contradiction by A2, A6, Def1; ::_thesis: verum
end;

theorem :: LMOD_5:3
for R being Ring
for V being LeftMod of R holds {} the carrier of V is linearly-independent
proof
let R be Ring; ::_thesis: for V being LeftMod of R holds {} the carrier of V is linearly-independent
let V be LeftMod of R; ::_thesis: {} the carrier of V is linearly-independent
let l be Linear_Combination of {} the carrier of V; :: according to LMOD_5:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
 Carrier l c= {} by VECTSP_6:def_4;
hence  ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum
end;

theorem Th4: :: LMOD_5:4
for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st 0. R <> 1. R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for v1, v2 being Vector of V st 0. R <> 1. R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
let V be LeftMod of R; ::_thesis: for v1, v2 being Vector of V st 0. R <> 1. R & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
let v1, v2 be Vector of V; ::_thesis: ( 0. R <> 1. R & {v1,v2} is linearly-independent implies ( v1 <> 0. V & v2 <> 0. V ) )
A1: ( v1 in {v1,v2} & v2 in {v1,v2} ) by TARSKI:def_2;
assume  ( 0. R <> 1. R & {v1,v2} is linearly-independent ) ; ::_thesis: ( v1 <> 0. V & v2 <> 0. V )
hence  ( v1 <> 0. V & v2 <> 0. V ) by A1, Th2; ::_thesis: verum
end;

theorem :: LMOD_5:5
for R being Ring
for V being LeftMod of R
for v being Vector of V st 0. R <> 1. R holds
( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th4;

theorem Th6: :: LMOD_5:6
for R being domRing
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
proof
let R be domRing; ::_thesis: for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V
for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
let L be Linear_Combination of V; ::_thesis: for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
let a be Scalar of R; ::_thesis: ( a <> 0. R implies Carrier (a * L) = Carrier L )
set T =  {  u where u is Vector of V : (a * L) . u <> 0. R  }  ;
set S =  {  v where v is Vector of V : L . v <> 0. R  }  ;
assume A1: a <> 0. R ; ::_thesis: Carrier (a * L) = Carrier L
  {  u where u is Vector of V : (a * L) . u <> 0. R  }  =  {  v where v is Vector of V : L . v <> 0. R  }
proof
thus   {  u where u is Vector of V : (a * L) . u <> 0. R  }  c=  {  v where v is Vector of V : L . v <> 0. R  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  v where v is Vector of V : L . v <> 0. R  }  c=  {  u where u is Vector of V : (a * L) . u <> 0. R  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  u where u is Vector of V : (a * L) . u <> 0. R  }  or x in  {  v where v is Vector of V : L . v <> 0. R  }  )
assume  x in  {  u where u is Vector of V : (a * L) . u <> 0. R  }  ; ::_thesis: x in  {  v where v is Vector of V : L . v <> 0. R  }
then consider u being Vector of V such that
A2: x = u and
A3: (a * L) . u <> 0. R ;
 (a * L) . u = a * (L . u) by VECTSP_6:def_9;
then  L . u <> 0. R by A3, VECTSP_1:6;
hence  x in  {  v where v is Vector of V : L . v <> 0. R  }  by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Vector of V : L . v <> 0. R  }  or x in  {  u where u is Vector of V : (a * L) . u <> 0. R  }  )
assume  x in  {  v where v is Vector of V : L . v <> 0. R  }  ; ::_thesis: x in  {  u where u is Vector of V : (a * L) . u <> 0. R  }
then consider v being Vector of V such that
A4: x = v and
A5: L . v <> 0. R ;
 (a * L) . v = a * (L . v) by VECTSP_6:def_9;
then  (a * L) . v <> 0. R by A1, A5, VECTSP_2:def_1;
hence  x in  {  u where u is Vector of V : (a * L) . u <> 0. R  }  by A4; ::_thesis: verum
end;
hence  Carrier (a * L) = Carrier L ; ::_thesis: verum
end;

theorem Th7: :: LMOD_5:7
for R being domRing
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
let R be domRing; ::_thesis: 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)
let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; ::_thesis: for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let a be Scalar of R; ::_thesis: Sum (a * L) = a * (Sum L)
percases ( a <> 0. R or a = 0. R ) ;
supposeA1: a <> 0. R ; ::_thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
A2: Carrier (a * L) = Carrier L by A1, Th6;
consider G being FinSequence of the carrier of V such that
A3: G is one-to-one and
A4: rng G = Carrier L and
A5: Sum L = Sum (L (#) G) by VECTSP_6:def_6;
set g = L (#) G;
consider F being FinSequence of the carrier of V such that
A6: F is one-to-one and
A7: rng F = Carrier (a * L) and
A8: Sum (a * L) = Sum ((a * L) (#) F) by VECTSP_6:def_6;
A9: len G = len F by A1, A6, A7, A3, A4, Th6, FINSEQ_1:48;
set f = (a * L) (#) F;
deffunc H1( Nat) ->  set = F <- (G . $1);
consider P being FinSequence such that
A10: len P = len F and
A11: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A12: ( Seg (len F) = dom F & dom P = dom F ) by A10, FINSEQ_1:def_3, FINSEQ_3:29;
A13: now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_
G_._x_=_F_._(P_._x)
let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) )
assume A14: x in dom G ; ::_thesis: G . x = F . (P . x)
then reconsider n = x as Element of NAT ;
 G . n in rng F by A7, A4, A2, A14, FUNCT_1:def_3;
then A15: F just_once_values G . n by A6, FINSEQ_4:8;
 n in Seg (len F) by A9, A14, FINSEQ_1:def_3;
then F . (P . n) = F . (F <- (G . n)) by A11, A12
.= G . n by A15, FINSEQ_4:def_3 ;
hence  G . x = F . (P . x) ; ::_thesis: verum
end;
A16: rng P c= dom F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom F )
assume  x in rng P ; ::_thesis: x in dom F
then consider y being set  such that
A17: y in dom P and
A18: P . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A17;
 y in dom G by A10, A9, A17, FINSEQ_3:29;
then  G . y in rng F by A7, A4, A2, FUNCT_1:def_3;
then A19: F just_once_values G . y by A6, FINSEQ_4:8;
 P . y = F <- (G . y) by A11, A17;
hence  x in dom F by A18, A19, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_)
let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) )
thus  ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G )
proof
assume  x in dom G ; ::_thesis: ( x in dom P & P . x in dom F )
hence  x in dom P by A10, A9, FINSEQ_3:29; ::_thesis: P . x in dom F
then  P . x in rng P by FUNCT_1:def_3;
hence  P . x in dom F by A16; ::_thesis: verum
end;
assume that
A20: x in dom P and
 P . x in dom F ; ::_thesis: x in dom G
thus  x in dom G by A10, A9, A20, FINSEQ_3:29; ::_thesis: verum
end;
then A21: G = F * P by A13, FUNCT_1:10;
 dom F c= rng P
proof
set f = (F ") * G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in rng P )
assume A22: x in dom F ; ::_thesis: x in rng P
 dom (F ") = rng G by A6, A7, A4, A2, FUNCT_1:33;
then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28
.= dom F by A6, FUNCT_1:33 ;
(F ") * G = ((F ") * F) * P by A21, RELAT_1:36
.= (id (dom F)) * P by A6, FUNCT_1:39
.= P by A16, RELAT_1:53 ;
hence  x in rng P by A22, A23; ::_thesis: verum
end;
then A24: dom F = rng P by A16, XBOOLE_0:def_10;
A25: dom P = dom F by A10, FINSEQ_3:29;
then A26: P is one-to-one by A24, FINSEQ_4:60;
reconsider P = P as Function of (dom F),(dom F) by A16, A25, FUNCT_2:2;
A27: len ((a * L) (#) F) = len F by VECTSP_6:def_5;
then A28: dom ((a * L) (#) F) = dom F by FINSEQ_3:29;
then reconsider P = P as Function of (dom ((a * L) (#) F)),(dom ((a * L) (#) F)) ;
reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;
reconsider P = P as Permutation of (dom ((a * L) (#) F)) by A24, A26, A28, FUNCT_2:57;
A29: Fp = ((a * L) (#) F) * P ;
then A30: len Fp = len ((a * L) (#) F) by FINSEQ_2:44;
then A31: len Fp = len (L (#) G) by A9, A27, VECTSP_6:def_5;
A32: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Vector_of_V_st_k_in_dom_Fp_&_v_=_(L_(#)_G)_._k_holds_
Fp_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being Vector of V st k in dom Fp & v = (L (#) G) . k holds
Fp . k = a * v
let v be Vector of V; ::_thesis: ( k in dom Fp & v = (L (#) G) . k implies Fp . k = a * v )
assume that
A33: k in dom Fp and
A34: v = (L (#) G) . k ; ::_thesis: Fp . k = a * v
A35: k in Seg (len (L (#) G)) by A31, A33, FINSEQ_1:def_3;
then A36: k in dom P by A10, A27, A30, A31, FINSEQ_1:def_3;
A37: k in dom G by A9, A27, A30, A31, A35, FINSEQ_1:def_3;
then  G . k in rng G by FUNCT_1:def_3;
then  F just_once_values G . k by A6, A7, A4, A2, FINSEQ_4:8;
then A38: F <- (G . k) in dom F by FINSEQ_4:def_3;
then reconsider i = F <- (G . k) as Element of NAT ;
A39: G /. k = G . k by A37, PARTFUN1:def_6
.= F . (P . k) by A21, A36, FUNCT_1:13
.= F . i by A11, A12, A27, A30, A31, A35
.= F /. i by A38, PARTFUN1:def_6 ;
A40: k in dom (L (#) G) by A35, FINSEQ_1:def_3;
 i in Seg (len ((a * L) (#) F)) by A27, A38, FINSEQ_1:def_3;
then A41: i in dom ((a * L) (#) F) by FINSEQ_1:def_3;
thus Fp . k = ((a * L) (#) F) . (P . k) by A36, FUNCT_1:13
.= ((a * L) (#) F) . (F <- (G . k)) by A11, A12, A27, A30, A31, A35
.= ((a * L) . (F /. i)) * (F /. i) by A41, VECTSP_6:def_5
.= (a * (L . (F /. i))) * (F /. i) by VECTSP_6:def_9
.= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def_16
.= a * v by A34, A40, A39, VECTSP_6:def_5 ; ::_thesis: verum
end;
 Sum Fp = Sum ((a * L) (#) F) by A29, RLVECT_2:7;
hence  Sum (a * L) = a * (Sum L) by A8, A5, A31, A32, RLVECT_2:66; ::_thesis: verum
end;
supposeA42: a = 0. R ; ::_thesis: Sum (a * L) = a * (Sum L)
hence  Sum (a * L) = Sum (ZeroLC V) by VECTSP_6:30
.= 0. V by VECTSP_6:15
.= a * (Sum L) by A42, VECTSP_1:14 ;
::_thesis: verum
end;
end;
end;


definition
let R be domRing;
let V be LeftMod of R;
let A be Subset of V;
func Lin A ->  strict Subspace of V means :Def2: :: LMOD_5:def 2
 the carrier of it =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }
proof
set A1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
  {  (Sum l) where l is Linear_Combination of A : verum  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Sum l) where l is Linear_Combination of A : verum  }  or x in the carrier of V )
assume  x in  {  (Sum l) where l is Linear_Combination of A : verum  }  ; ::_thesis: x in the carrier of V
then  ex l being Linear_Combination of A st x = Sum l ;
hence  x in the carrier of V ; ::_thesis: verum
end;
then reconsider A1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  as Subset of V ;
reconsider l = ZeroLC V as Linear_Combination of A by VECTSP_6:5;
A1: A1 is linearly-closed
proof
thus  for v, u being Vector of V st v in A1 & u in A1 holds
v + u in A1 :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A1 or b1 * b2 in A1 )
proof
let v, u be Vector of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; ::_thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by VECTSP_6:24;
 v + u = Sum f by A4, A5, VECTSP_6:44;
hence  v + u in A1 ; ::_thesis: verum
end;
let a be Scalar of R; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or a * b1 in A1 )
let v be Vector of V; ::_thesis: ( not v in A1 or a * v in A1 )
assume  v in A1 ; ::_thesis: a * v in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = a * l as Linear_Combination of A by VECTSP_6:31;
 a * v = Sum f by A6, Th7;
hence  a * v in A1 ; ::_thesis: verum
end;
 Sum l = 0. V by VECTSP_6:15;
then  0. V in A1 ;
hence  ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  by A1, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  & the carrier of b2 =  {  (Sum l) where l is Linear_Combination of A : verum  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def2 defines Lin LMOD_5:def_2_:_
 for R being domRing
for V being LeftMod of R
for A being Subset of V
for b4 being strict Subspace of V holds
( b4 = Lin A iff the carrier of b4 =  {  (Sum l) where l is Linear_Combination of A : verum  }  );

theorem Th8: :: LMOD_5:8
for x being set
for R being domRing
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
let x be set ; ::_thesis: for R being domRing
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 )
let R be domRing; ::_thesis: 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 )
let V be LeftMod of R; ::_thesis: for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus  ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )
proof
assume  x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l
then  x in the carrier of (Lin A) by STRUCT_0:def_5;
then  x in  {  (Sum l) where l is Linear_Combination of A : verum  }  by Def2;
hence  ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum
end;
given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A
 x in  {  (Sum l) where l is Linear_Combination of A : verum  }  by A1;
then  x in the carrier of (Lin A) by Def2;
hence  x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th9: :: LMOD_5:9
for x being set
for R being domRing
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
proof
let x be set ; ::_thesis: for R being domRing
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
let R be domRing; ::_thesis: for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
let V be LeftMod of R; ::_thesis: for A being Subset of V st x in A holds
x in Lin A
let A be Subset of V; ::_thesis: ( x in A implies x in Lin A )
deffunc H1( set ) ->  Element of the carrier of R = 0. R;
assume A1: x in A ; ::_thesis: x in Lin A
then reconsider v = x as Vector of V ;
consider f being Function of the carrier of V, the carrier of R such that
A2: f . v = 1. R and
A3: for u being Vector of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
 ex T being finite Subset of V st
for u being Vector of V st not u in T holds
f . u = 0. R
proof
take T = {v}; ::_thesis: for u being Vector of V st not u in T holds
f . u = 0. R
let u be Vector of V; ::_thesis: ( not u in T implies f . u = 0. R )
assume  not u in T ; ::_thesis: f . u = 0. R
then  u <> v by TARSKI:def_1;
hence  f . u = 0. R by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume  x in Carrier f ; ::_thesis: x in {v}
then consider u being Vector of V such that
A5: x = u and
A6: f . u <> 0. R ;
 u = v by A3, A6;
hence  x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by VECTSP_6:def_4;
A7: Sum f = (1. R) * v by A2, VECTSP_6:17
.= v by VECTSP_1:def_17 ;
 {v} c= A by A1, ZFMISC_1:31;
then  Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
 Sum f = v by A7;
hence  x in Lin A by Th8; ::_thesis: verum
end;

theorem :: LMOD_5:10
for R being domRing
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
proof
let R be domRing; ::_thesis: for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
let V be LeftMod of R; ::_thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus  ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )
proof
assume  v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5;
 the carrier of (Lin ({} the carrier of V)) =  {  (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum  }  by Def2;
then  ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then  v = 0. V by VECTSP_6:16;
hence  v in (0). V by VECTSP_4:35; ::_thesis: verum
end;
assume  v in (0). V ; ::_thesis: v in Lin ({} the carrier of V)
then  v = 0. V by VECTSP_4:35;
hence  v in Lin ({} the carrier of V) by VECTSP_4:17; ::_thesis: verum
end;
hence  Lin ({} the carrier of V) = (0). V by VECTSP_4:30; ::_thesis: verum
end;

theorem :: LMOD_5:11
for R being domRing
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
let R be domRing; ::_thesis: for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let V be LeftMod of R; ::_thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; ::_thesis: A = {(0. V)}
thus  A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} )
assume  x in A ; ::_thesis: x in {(0. V)}
then  x in Lin A by Th9;
then  x = 0. V by A1, VECTSP_4:35;
hence  x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
set y = the Element of A;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A )
assume  x in {(0. V)} ; ::_thesis: x in A
then A3: x = 0. V by TARSKI:def_1;
 ( the Element of A in A & the Element of A in Lin A ) by A2, Th9;
hence  x in A by A1, A3, VECTSP_4:35; ::_thesis: verum
end;

theorem Th12: :: LMOD_5:12
for R being domRing
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
let R be domRing; ::_thesis: 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
let V be LeftMod of R; ::_thesis: 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
let A be Subset of V; ::_thesis: for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; ::_thesis: ( 0. R <> 1. R & A = the carrier of W implies Lin A = W )
assume that
A1: 0. R <> 1. R and
A2: A = the carrier of W ; ::_thesis: Lin A = W
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
thus  ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A )
proof
assume  v in Lin A ; ::_thesis: v in W
then A3: ex l being Linear_Combination of A st v = Sum l by Th8;
 A is linearly-closed by A2, VECTSP_4:33;
then  v in the carrier of W by A1, A2, A3, VECTSP_6:14;
hence  v in W by STRUCT_0:def_5; ::_thesis: verum
end;
 ( v in W iff v in the carrier of W ) by STRUCT_0:def_5;
hence  ( v in W implies v in Lin A ) by A2, Th9; ::_thesis: verum
end;
hence  Lin A = W by VECTSP_4:30; ::_thesis: verum
end;

theorem :: LMOD_5:13
for R being domRing
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
let R be domRing; ::_thesis: 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
let V be strict LeftMod of R; ::_thesis: for A being Subset of V st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( 0. R <> 1. R & A = the carrier of V implies Lin A = V )
assume A1: 0. R <> 1. R ; ::_thesis: ( not A = the carrier of V or Lin A = V )
assume A2: A = the carrier of V ; ::_thesis: Lin A = V
 (Omega). V = V ;
hence  Lin A = V by A1, A2, Th12; ::_thesis: verum
end;

theorem Th14: :: LMOD_5:14
for R being domRing
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
let R be domRing; ::_thesis: 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
let V be LeftMod of R; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B )
assume A1: A c= B ; ::_thesis: Lin A is Subspace of Lin B
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
let v be Vector of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume  v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th8;
reconsider l = l as Linear_Combination of B by A1, VECTSP_6:4;
 Sum l = v by A2;
hence  v in Lin B by Th8; ::_thesis: verum
end;
hence  Lin A is Subspace of Lin B by VECTSP_4:28; ::_thesis: verum
end;

theorem :: LMOD_5:15
for R being domRing
for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let R be domRing; ::_thesis: for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be strict LeftMod of R; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V )
assume  ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V
then  V is Subspace of Lin B by Th14;
hence  Lin B = V by VECTSP_4:25; ::_thesis: verum
end;

theorem :: LMOD_5:16
for R being domRing
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let R be domRing; ::_thesis: for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let V be LeftMod of R; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B)
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_(A_\/_B)_holds_
v_in_(Lin_A)_+_(Lin_B)
deffunc H1( set ) ->  Element of the carrier of R = 0. R;
let v be Vector of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume  v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum l by Th8;
deffunc H2( set ) ->  set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_S1[x]_implies_H2(x)_in_the_carrier_of_R_)_&_(_not_S1[x]_implies_H1(x)_in_the_carrier_of_R_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
 for f being Function of the carrier of V, the carrier of R holds f . v in the carrier of R ;
hence  ( S1[x] implies H2(x) in the carrier of R ) ; ::_thesis: ( not S1[x] implies H1(x) in the carrier of R )
assume  not S1[x] ; ::_thesis: H1(x) in the carrier of R
thus  H1(x) in the carrier of R ; ::_thesis: verum
end;
A3: (Carrier l) \ A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ A or x in B )
assume  x in (Carrier l) \ A ; ::_thesis: x in B
then A4: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5;
 Carrier l c= A \/ B by VECTSP_6:def_4;
hence  x in B by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
consider f being Function of the carrier of V, the carrier of R such that
A5: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
 for u being Vector of V st not u in (Carrier l) /\ A holds
f . u = 0. R by A5;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A6: Carrier f c= (Carrier l) /\ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) /\ A )
assume  x in Carrier f ; ::_thesis: x in (Carrier l) /\ A
then A7: ex u being Vector of V st
( x = u & f . u <> 0. R ) ;
assume  not x in (Carrier l) /\ A ; ::_thesis: contradiction
hence  contradiction by A5, A7; ::_thesis: verum
end;
 (Carrier l) /\ A c= A by XBOOLE_1:17;
then  Carrier f c= A by A6, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
defpred S2[ set ] means $1 in (Carrier l) \ A;
A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_S2[x]_implies_H2(x)_in_the_carrier_of_R_)_&_(_not_S2[x]_implies_H1(x)_in_the_carrier_of_R_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
 for g being Function of the carrier of V, the carrier of R holds g . v in the carrier of R ;
hence  ( S2[x] implies H2(x) in the carrier of R ) ; ::_thesis: ( not S2[x] implies H1(x) in the carrier of R )
assume  not S2[x] ; ::_thesis: H1(x) in the carrier of R
thus  H1(x) in the carrier of R ; ::_thesis: verum
end;
consider g being Function of the carrier of V, the carrier of R such that
A9: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A8);
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
 for u being Vector of V st not u in (Carrier l) \ A holds
g . u = 0. R by A9;
then reconsider g = g as Linear_Combination of V by VECTSP_6:def_1;
 Carrier g c= (Carrier l) \ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in (Carrier l) \ A )
assume  x in Carrier g ; ::_thesis: x in (Carrier l) \ A
then A10: ex u being Vector of V st
( x = u & g . u <> 0. R ) ;
assume  not x in (Carrier l) \ A ; ::_thesis: contradiction
hence  contradiction by A9, A10; ::_thesis: verum
end;
then  Carrier g c= B by A3, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by VECTSP_6:def_4;
 l = f + g
proof
let v be Vector of V; :: according to VECTSP_6:def_7 ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in (Carrier l) /\ A or not v in (Carrier l) /\ A ) ;
supposeA11: v in (Carrier l) /\ A ; ::_thesis: (f + g) . v = l . v
A12: now__::_thesis:_not_v_in_(Carrier_l)_\_A
assume  v in (Carrier l) \ A ; ::_thesis: contradiction
then  not v in A by XBOOLE_0:def_5;
hence  contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (l . v) + (g . v) by A5, A11
.= (l . v) + (0. R) by A9, A12
.= l . v by RLVECT_1:4 ; ::_thesis: verum
end;
supposeA13: not v in (Carrier l) /\ A ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A15: now__::_thesis:_v_in_(Carrier_l)_\_A
assume  not v in (Carrier l) \ A ; ::_thesis: contradiction
then  ( not v in Carrier l or v in A ) by XBOOLE_0:def_5;
hence  contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (0. R) + (g . v) by A5, A13
.= g . v by RLVECT_1:4
.= l . v by A9, A15 ; ::_thesis: verum
end;
supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v
then A17: not v in (Carrier l) \ A by XBOOLE_0:def_5;
A18: not v in (Carrier l) /\ A by A16, XBOOLE_0:def_4;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (0. R) + (g . v) by A5, A18
.= (0. R) + (0. R) by A9, A17
.= 0. R by RLVECT_1:4
.= l . v by A16 ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
end;
then A19: v = (Sum f) + (Sum g) by A1, VECTSP_6:44;
 ( Sum f in Lin A & Sum g in Lin B ) by Th8;
hence  v in (Lin A) + (Lin B) by A19, VECTSP_5:1; ::_thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by VECTSP_4:28;
 ( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th14, XBOOLE_1:7;
then  (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by VECTSP_5:34;
hence  Lin (A \/ B) = (Lin A) + (Lin B) by A20, VECTSP_4:25; ::_thesis: verum
end;

theorem :: LMOD_5:17
for R being domRing
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
let R be domRing; ::_thesis: for V being LeftMod of R
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let V be LeftMod of R; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
 ( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th14, XBOOLE_1:17;
hence  Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by VECTSP_5:19; ::_thesis: verum
end;