Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Submodules

**by****Michal Muzalewski**- Received June 19, 1992
- MML identifier: LMOD_6

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_2, RMOD_3, FUNCT_1, RLSUB_1, RELAT_1, RLVECT_1, REALSET1, QC_LANG1, SUBSET_1, RLVECT_3, BOOLE, PARTFUN1, ARYTM_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1, RLVECT_1, STRUCT_0, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, MOD_3, PRE_TOPC; constructors BINOP_1, DOMAIN_1, REALSET1, VECTSP_5, VECTSP_6, MOD_3, PRE_TOPC, VECTSP_2, MEMBERED, XBOOLE_0; clusters VECTSP_1, VECTSP_2, VECTSP_4, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; 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; definition let K, V; redefine func Subspaces(V); synonym Submodules(V); end; theorem :: LMOD_6:1 M1 = the VectSpStr of M2 implies (x in M1 iff x in M2); theorem :: LMOD_6:2 for v being Vector of the VectSpStr of V st a=v holds r*a = r*v; theorem :: LMOD_6:3 the VectSpStr of V is strict Subspace of V; theorem :: LMOD_6:4 V is Subspace of (Omega).V; begin definition let K; redefine canceled; attr K is trivial means :: LMOD_6:def 2 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 VectSpStr 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 3 W; end; canceled; theorem :: LMOD_6:9 for A being Subset of W holds A is Subset of V; definition let K,V,W; let A be Subset of W; canceled; func @A -> Subset of V equals :: LMOD_6:def 5 A; end; definition let K,V,W; let A be non empty Subset of W; cluster @A -> non empty; end; theorem :: LMOD_6:10 x in [#]V iff x in V; theorem :: LMOD_6:11 x in @[#]W iff x in W; theorem :: LMOD_6:12 A c= [#]Lin(A); theorem :: LMOD_6:13 A<>{} & A is lineary-closed implies Sum(l) in A; canceled; theorem :: LMOD_6:15 0.V in A & A is lineary-closed implies A = [#]Lin(A); begin :: :: 2. Cyclic submodule :: definition let K,V,a; redefine func {a} -> Subset of V; end; definition let K,V,a; func <:a:> -> strict Subspace of V equals :: LMOD_6:def 6 Lin({a}); end; begin :: :: 3. Inclusion of left R-modules :: definition let K,M,N; pred M c= N means :: LMOD_6:def 7 M is Subspace of N; reflexivity; end; theorem :: LMOD_6:16 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:17 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:18 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; canceled 2; theorem :: LMOD_6:21 for V,M being strict LeftMod of K holds V c= M & M c= V implies V = M; theorem :: LMOD_6:22 V c= M & M c= N implies V c= N; theorem :: LMOD_6:23 M c= N implies (0).M c= N; theorem :: LMOD_6:24 M c= N implies (0).N c= M; theorem :: LMOD_6:25 M c= N implies M c= (Omega).N; theorem :: LMOD_6:26 W1 c= W1 + W2 & W2 c= W1 + W2; theorem :: LMOD_6:27 W1 /\ W2 c= W1 & W1 /\ W2 c= W2; theorem :: LMOD_6:28 W1 c= W2 implies W1 /\ W3 c= W2 /\ W3; theorem :: LMOD_6:29 W1 c= W3 implies W1 /\ W2 c= W3; theorem :: LMOD_6:30 W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3; theorem :: LMOD_6:31 W1 /\ W2 c= W1 + W2; theorem :: LMOD_6:32 (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3); theorem :: LMOD_6:33 W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3); theorem :: LMOD_6:34 W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3); theorem :: LMOD_6:35 W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3); theorem :: LMOD_6:36 W1 c= W2 implies W1 c= W2 + W3; theorem :: LMOD_6:37 W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3; theorem :: LMOD_6:38 for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B); theorem :: LMOD_6:39 for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B); theorem :: LMOD_6:40 M1 c= M2 implies [#]M1 c= [#]M2; theorem :: LMOD_6:41 W1 c= W2 iff for a st a in W1 holds a in W2; theorem :: LMOD_6:42 W1 c= W2 iff [#]W1 c= [#]W2; theorem :: LMOD_6:43 W1 c= W2 iff @[#]W1 c= @[#]W2; theorem :: LMOD_6:44 (0).W c= V & (0).V c= W & (0).W1 c= W2;

Back to top