:: Submodules
:: by Micha{\l} Muzalewski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

notation
let K be Ring;
let V be LeftMod of K;
synonym  Submodules V for  Subspaces V;
end;

theorem :: LMOD_6:1
for x being set
for K being Ring
for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
proofend;

theorem :: LMOD_6:2
for K being Ring
for r being Scalar of K
for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
proofend;

theorem Th3: :: LMOD_6:3
for K being Ring
for V being LeftMod of K holds VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
proofend;

theorem Th4: :: LMOD_6:4
for K being Ring
for V being LeftMod of K holds V is Subspace of (Omega). V
proofend;

begin

definition
let K be Ring;
redefine attr K is trivial  means :Def1: :: LMOD_6:def 1
 0. K = 1_ K;
compatibility
 ( K is trivial iff 0. K = 1_ K )
proofend;
end;

:: deftheorem Def1 defines trivial LMOD_6:def_1_:_
 for K being Ring holds
( K is trivial iff 0. K = 1_ K );

theorem Th5: :: LMOD_6:5
for K being Ring
for V being LeftMod of K st K is trivial holds
( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
proofend;

theorem :: LMOD_6:6
for K being Ring
for V being LeftMod of K st K is trivial holds
V is trivial
proofend;

theorem :: LMOD_6:7
for K being Ring
for V being LeftMod of K holds
( V is trivial iff VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
proofend;

begin

definition
let K be Ring;
let V be LeftMod of K;
let W be strict Subspace of V;
func @ W ->  Element of Submodules V equals :: LMOD_6:def 2
W;
coherence
 W is Element of Submodules V by VECTSP_5:def_3;
end;

:: deftheorem  defines @ LMOD_6:def_2_:_
 for K being Ring
for V being LeftMod of K
for W being strict Subspace of V holds @ W = W;

theorem Th8: :: LMOD_6:8
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds A is Subset of V
proofend;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let A be Subset of W;
func @ A ->  Subset of V equals :: LMOD_6:def 3
A;
coherence
 A is Subset of V by Th8;
end;

:: deftheorem  defines @ LMOD_6:def_3_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds @ A = A;

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let A be non empty Subset of W;
cluster @ A ->  non empty ;
coherence
 not @ A is empty ;
end;

theorem :: LMOD_6:9
for x being set
for K being Ring
for V being LeftMod of K holds
( x in [#] V iff x in V ) by STRUCT_0:def_5;

theorem :: LMOD_6:10
for x being set
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( x in @ ([#] W) iff x in W ) by STRUCT_0:def_5;

theorem Th11: :: LMOD_6:11
for K being Ring
for V being LeftMod of K
for A being Subset of V holds A c= [#] (Lin A)
proofend;

theorem Th12: :: LMOD_6:12
for K being Ring
for V being LeftMod of K
for A being Subset of V
for l being Linear_Combination of A st A <> {} &amp; A is linearly-closed holds
Sum l in A
proofend;

theorem :: LMOD_6:13
for K being Ring
for V being LeftMod of K
for A being Subset of V st 0. V in A &amp; A is linearly-closed holds
A = [#] (Lin A)
proofend;

begin

definition
let K be Ring;
let V be LeftMod of K;
let a be Vector of V;
func<:a:> ->  strict Subspace of V equals :: LMOD_6:def 4
 Lin {a};
correctness
coherence
Lin {a} is strict Subspace of V;
;
end;

:: deftheorem  defines <: LMOD_6:def_4_:_
 for K being Ring
for V being LeftMod of K
for a being Vector of V holds <:a:> = Lin {a};

begin

definition
let K be Ring;
let M, N be LeftMod of K;
predM c= N means :Def5: :: LMOD_6:def 5
M is Subspace of N;
reflexivity
 for M being LeftMod of K holds M is Subspace of M by VECTSP_4:24;
end;

:: deftheorem Def5 defines c= LMOD_6:def_5_:_
 for K being Ring
for M, N being LeftMod of K holds
( M c= N iff M is Subspace of N );

theorem Th14: :: LMOD_6:14
for x being set
for K being Ring
for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) &amp; ( x is Vector of M implies x is Vector of N ) )
proofend;

theorem :: LMOD_6:15
for K being Ring
for r being Scalar of K
for M, N being LeftMod of K
for m1, m2, m being Vector of M
for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N &amp; ( m1 = n1 &amp; m2 = n2 implies m1 + m2 = n1 + n2 ) &amp; ( m = n implies r * m = r * n ) &amp; ( m = n implies - n = - m ) &amp; ( m1 = n1 &amp; m2 = n2 implies m1 - m2 = n1 - n2 ) &amp; 0. N in M &amp; 0. M in N &amp; ( n1 in M &amp; n2 in M implies n1 + n2 in M ) &amp; ( n in M implies r * n in M ) &amp; ( n in M implies - n in M ) &amp; ( n1 in M &amp; n2 in M implies n1 - n2 in M ) )
proofend;

theorem :: LMOD_6:16
for K being Ring
for M1, N, M2 being LeftMod of K st M1 c= N &amp; M2 c= N holds
( 0. M1 = 0. M2 &amp; 0. M1 in M2 &amp; ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) &amp; ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) &amp; ( the carrier of M1 = the carrier of M2 &amp; M1 is strict &amp; M2 is strict implies M1 = M2 ) &amp; (0). M1 c= M2 )
proofend;

theorem :: LMOD_6:17
for K being Ring
for V, M being strict LeftMod of K st V c= M &amp; M c= V holds
V = M
proofend;

theorem :: LMOD_6:18
for K being Ring
for V, M, N being LeftMod of K st V c= M &amp; M c= N holds
V c= N
proofend;

theorem :: LMOD_6:19
for K being Ring
for M, N being LeftMod of K st M c= N holds
(0). M c= N
proofend;

theorem :: LMOD_6:20
for K being Ring
for M, N being LeftMod of K st M c= N holds
(0). N c= M
proofend;

theorem :: LMOD_6:21
for K being Ring
for M, N being LeftMod of K st M c= N holds
M c= (Omega). N
proofend;

theorem :: LMOD_6:22
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W1 + W2 &amp; W2 c= W1 + W2 )
proofend;

theorem :: LMOD_6:23
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 /\ W2 c= W1 &amp; W1 /\ W2 c= W2 )
proofend;

theorem :: LMOD_6:24
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 /\ W3 c= W2 /\ W3
proofend;

theorem :: LMOD_6:25
for K being Ring
for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 holds
W1 /\ W2 c= W3
proofend;

theorem :: LMOD_6:26
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 &amp; W1 c= W3 holds
W1 c= W2 /\ W3
proofend;

theorem :: LMOD_6:27
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds W1 /\ W2 c= W1 + W2
proofend;

theorem :: LMOD_6:28
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
proofend;

theorem :: LMOD_6:29
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
proofend;

theorem :: LMOD_6:30
for K being Ring
for V being LeftMod of K
for W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
proofend;

theorem :: LMOD_6:31
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
proofend;

theorem :: LMOD_6:32
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 c= W2 + W3
proofend;

theorem :: LMOD_6:33
for K being Ring
for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 &amp; W2 c= W3 holds
W1 + W2 c= W3
proofend;

theorem :: LMOD_6:34
for K being Ring
for V being LeftMod of K
for A, B being Subset of V st A c= B holds
Lin A c= Lin B
proofend;

theorem :: LMOD_6:35
for K being Ring
for V being LeftMod of K
for A, B being Subset of V holds Lin (A /\ B) c= (Lin A) /\ (Lin B)
proofend;

theorem Th36: :: LMOD_6:36
for K being Ring
for M1, M2 being LeftMod of K st M1 c= M2 holds
[#] M1 c= [#] M2
proofend;

theorem Th37: :: LMOD_6:37
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 )
proofend;

theorem Th38: :: LMOD_6:38
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff [#] W1 c= [#] W2 )
proofend;

theorem :: LMOD_6:39
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff @ ([#] W1) c= @ ([#] W2) ) by Th38;

theorem :: LMOD_6:40
for K being Ring
for V being LeftMod of K
for W, W1, W2 being Subspace of V holds
( (0). W c= V &amp; (0). V c= W &amp; (0). W1 c= W2 )
proofend;