:: Submodules :: by Micha{\l} Muzalewski :: :: Received June 19, 1992 :: Copyright (c) 1992-2021 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; 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;