:: Submodules
:: by Micha{\l} Muzalewski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCSDOM, VECTSP_1, VECTSP_2, SUBSET_1, RLVECT_2, RLSUB_1,
RMOD_3, RLSUB_2, STRUCT_0, RELAT_1, FUNCT_1, SUPINF_2, ZFMISC_1,
ALGSTR_0, REALSET1, GROUP_1, QC_LANG1, TARSKI, XBOOLE_0, RLVECT_3,
CARD_3, PARTFUN1, ARYTM_3, ARYTM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1,
DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4,
VECTSP_5, VECTSP_6, VECTSP_7;
constructors BINOP_1, REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, RELSET_1;
registrations RELSET_1, STRUCT_0, VECTSP_1, VECTSP_4, VECTSP_7;
requirements SUBSET, BOOLE;
begin
reserve x for set,
K for Ring,
r for Scalar of K,
V, M, M1, M2, N for LeftMod of K,
a for Vector of V,
m, m1, m2 for Vector of M,
n, n1, n2 for Vector of N,
A for Subset of V,
l for Linear_Combination of A,
W, W1, W2, W3 for Subspace of V;
notation
let K, V;
synonym Submodules(V) for Subspaces(V);
end;
theorem :: LMOD_6:1
M1 = the ModuleStr of M2 implies (x in M1 iff x in M2);
theorem :: LMOD_6:2
for v being Vector of the ModuleStr of V st a=v holds r*a = r*v;
theorem :: LMOD_6:3
the ModuleStr of V is strict Subspace of V;
theorem :: LMOD_6:4
V is Subspace of (Omega).V;
begin
definition
let K;
redefine attr K is trivial means
:: LMOD_6:def 1
0.K = 1_K;
end;
theorem :: LMOD_6:5
K is trivial implies (for r holds r = 0.K) & for a holds a = 0.V;
theorem :: LMOD_6:6
K is trivial implies V is trivial;
theorem :: LMOD_6:7
V is trivial iff the ModuleStr of V = (0).V;
begin :: 1. Submodules and subsets
definition
let K,V;
let W be strict Subspace of V;
func @W -> Element of Submodules(V) equals
:: LMOD_6:def 2
W;
end;
theorem :: LMOD_6:8
for A being Subset of W holds A is Subset of V;
definition
let K,V,W;
let A be Subset of W;
func @A -> Subset of V equals
:: LMOD_6:def 3
A;
end;
registration
let K,V,W;
let A be non empty Subset of W;
cluster @A -> non empty;
end;
theorem :: LMOD_6:9
x in [#]V iff x in V;
theorem :: LMOD_6:10
x in @[#]W iff x in W;
theorem :: LMOD_6:11
A c= [#]Lin(A);
theorem :: LMOD_6:12
A<>{} & A is linearly-closed implies Sum(l) in A;
theorem :: LMOD_6:13
0.V in A & A is linearly-closed implies A = [#]Lin(A);
begin :: 2. Cyclic submodule
definition
let K,V,a;
func <:a:> -> strict Subspace of V equals
:: LMOD_6:def 4
Lin({a});
end;
begin :: 3. Inclusion of left R-modules
definition
let K,M,N;
pred M c= N means
:: LMOD_6:def 5
M is Subspace of N;
reflexivity;
end;
theorem :: LMOD_6:14
for x being object holds
M c= N implies (x in M implies x in N) & (x is Vector of M
implies x is Vector of N);
theorem :: LMOD_6:15
M c= N implies 0.M = 0.N & (m1 = n1 & m2 = n2 implies m1 + m2 = n1 +
n2) & (m = n implies r * m = r * n) & (m = n implies - n = - m) & (m1 = n1 & m2
= n2 implies m1 - m2 = n1 - n2) & 0.N in M & 0.M in N & (n1 in M & n2 in M
implies n1 + n2 in M) & (n in M implies r * n in M) & (n in M implies - n in M)
& (n1 in M & n2 in M implies n1 - n2 in M);
theorem :: LMOD_6:16
M1 c= N & M2 c= N implies 0.M1 = 0.M2 & 0.M1 in M2 & (the carrier of
M1 c= the carrier of M2 implies M1 c= M2) & ((for n st n in M1 holds n in M2)
implies M1 c= M2) & (the carrier of M1 = the carrier of M2 & M1 is strict & M2
is strict implies M1 = M2) & (0).M1 c= M2;
theorem :: LMOD_6:17
for V,M being strict LeftMod of K holds V c= M & M c= V implies V = M;
theorem :: LMOD_6:18
V c= M & M c= N implies V c= N;
theorem :: LMOD_6:19
M c= N implies (0).M c= N;
theorem :: LMOD_6:20
M c= N implies (0).N c= M;
theorem :: LMOD_6:21
M c= N implies M c= (Omega).N;
theorem :: LMOD_6:22
W1 c= W1 + W2 & W2 c= W1 + W2;
theorem :: LMOD_6:23
W1 /\ W2 c= W1 & W1 /\ W2 c= W2;
theorem :: LMOD_6:24
W1 c= W2 implies W1 /\ W3 c= W2 /\ W3;
theorem :: LMOD_6:25
W1 c= W3 implies W1 /\ W2 c= W3;
theorem :: LMOD_6:26
W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3;
theorem :: LMOD_6:27
W1 /\ W2 c= W1 + W2;
theorem :: LMOD_6:28
(W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3);
theorem :: LMOD_6:29
W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);
theorem :: LMOD_6:30
W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3);
theorem :: LMOD_6:31
W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);
theorem :: LMOD_6:32
W1 c= W2 implies W1 c= W2 + W3;
theorem :: LMOD_6:33
W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3;
theorem :: LMOD_6:34
for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B);
theorem :: LMOD_6:35
for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B);
theorem :: LMOD_6:36
M1 c= M2 implies [#]M1 c= [#]M2;
theorem :: LMOD_6:37
W1 c= W2 iff for a st a in W1 holds a in W2;
theorem :: LMOD_6:38
W1 c= W2 iff [#]W1 c= [#]W2;
theorem :: LMOD_6:39
W1 c= W2 iff @[#]W1 c= @[#]W2;
theorem :: LMOD_6:40
(0).W c= V & (0).V c= W & (0).W1 c= W2;