### The Mizar article:

### Submodules

**by****Michal Muzalewski**

- Received June 19, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: LMOD_6
- [ 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; definitions TARSKI, XBOOLE_0; theorems FUNCT_2, MOD_3, TARSKI, VECTSP_1, VECTSP_2, RLVECT_1, ANPROJ_1, VECTSP_4, VECTSP_5, VECTSP_6, PRE_TOPC, XBOOLE_1, RELAT_1; 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 M1 = the VectSpStr of M2 implies (x in M1 iff x in M2) proof assume A1: M1 = the VectSpStr of M2; x in M1 iff x in the carrier of M1 by RLVECT_1:def 1; hence thesis by A1,RLVECT_1:def 1; end; theorem for v being Vector of the VectSpStr of V st a=v holds r*a = r*v proof let v be Vector of (the VectSpStr of V) such that A1: a=v; thus r*a = (the lmult of V).(r,a) by VECTSP_1:def 24 .= r*v by A1,VECTSP_1:def 24; end; theorem Th3: the VectSpStr of V is strict Subspace of V proof (Omega).V = the VectSpStr of V by VECTSP_4:def 4;hence thesis;end; theorem Th4: V is Subspace of (Omega).V proof set W=(Omega).V; A1: W = the VectSpStr of V by VECTSP_4:def 4; A2: dom(the add of W) = [:the carrier of W,the carrier of W:] by FUNCT_2:def 1; dom(the lmult of W) = [:the carrier of K, the carrier of W:] by FUNCT_2:def 1; then the carrier of V c= the carrier of W & the Zero of V = the Zero of W & the add of V = (the add of W) | [:the carrier of V,the carrier of V:] & the lmult of V = (the lmult of W) | [:the carrier of K, the carrier of V:] by A1,A2,RELAT_1:97; hence thesis by VECTSP_4:def 2; end; begin definition let K; redefine canceled; attr K is trivial means :Def2: 0.K = 1_ K; compatibility proof thus K is trivial implies 0.K = 1_ K by ANPROJ_1:def 8; assume A1: 0.K = 1_ K; now let x be Scalar of K; thus x = x*(1_ K) by VECTSP_2:def 2 .= 0.K by A1,VECTSP_1:36; end; hence K is trivial by ANPROJ_1:def 8; end; end; theorem Th5: K is trivial implies (for r holds r = 0.K) & (for a holds a = 0.V) proof assume K is trivial; then A1: 0.K = 1_ K by Def2; A2: now let r; thus r = r*1_ K by VECTSP_2:def 2 .= 0.K by A1,VECTSP_1:36;end; now let a; thus a = 1_ K*a by VECTSP_1:def 26 .= 0.V by A1,VECTSP_1:59; end; hence thesis by A2; end; theorem K is trivial implies V is trivial proof assume A1: K is trivial & V is non trivial; then ex a st a <> 0.V by ANPROJ_1:def 8; hence contradiction by A1,Th5; end; theorem V is trivial iff the VectSpStr of V = (0).V proof reconsider W = the VectSpStr of V as strict Subspace of V by Th3; reconsider Z=(0).V as Subspace of W by VECTSP_4:50; set X = the carrier of (0).V; A1: now assume V is non trivial; then consider a such that A2: a <> 0.V by ANPROJ_1:def 8; not a in {0.V} by A2,TARSKI:def 1; then not a in X by VECTSP_4:def 3; hence W <> (0).V;end; now assume W <> Z; then consider a such that A3: not a in Z by VECTSP_4:40; not a in X by A3,RLVECT_1:def 1; then not a in {0.V} by VECTSP_4:def 3; then a <> 0.V by TARSKI:def 1; hence V is non trivial by ANPROJ_1:def 8;end; hence thesis by A1; end; begin :: :: 1. Submodules and subsets :: definition let K,V; let W be strict Subspace of V; func @W -> Element of Submodules(V) equals W; coherence by VECTSP_5:def 3; end; canceled; theorem Th9: for A being Subset of W holds A is Subset of V proof let A be Subset of W; the carrier of W c= the carrier of V by VECTSP_4:def 2; then A is Subset of V by XBOOLE_1:1; hence thesis; end; definition let K,V,W; let A be Subset of W; canceled; func @A -> Subset of V equals :Def5: A; coherence by Th9; end; definition let K,V,W; let A be non empty Subset of W; cluster @A -> non empty; coherence by Def5; end; theorem Th10: x in [#]V iff x in V proof [#]V = the carrier of V by PRE_TOPC:12; hence thesis by RLVECT_1:def 1; end; theorem x in @[#]W iff x in W proof @[#]W = [#]W by Def5; hence thesis by Th10; end; theorem Th12: A c= [#]Lin(A) proof let x; assume x in A; then x in Lin(A) by MOD_3:12; hence thesis by Th10; end; theorem Th13: A<>{} & A is lineary-closed implies Sum(l) in A proof assume A1: A<>{} & A is lineary-closed; now per cases; suppose 0.K<>1_ K; hence thesis by A1,VECTSP_6:40; suppose 0.K=1_ K; then K is trivial by Def2; then Sum(l) = 0.V by Th5; hence thesis by A1,VECTSP_4:4;end; hence thesis; end; canceled; theorem 0.V in A & A is lineary-closed implies A = [#]Lin(A) proof assume A1: 0.V in A & A is lineary-closed; thus A c= [#]Lin(A) by Th12; let x; assume x in [#]Lin(A); then x in Lin(A) by Th10; then ex l st x = Sum(l) by MOD_3:11; hence thesis by A1,Th13; end; begin :: :: 2. Cyclic submodule :: definition let K,V,a; redefine func {a} -> Subset of V; coherence proof thus {a} is Subset of V; end; end; definition let K,V,a; func <:a:> -> strict Subspace of V equals Lin({a}); correctness; end; begin :: :: 3. Inclusion of left R-modules :: definition let K,M,N; pred M c= N means :Def7: M is Subspace of N; reflexivity by VECTSP_4:32; end; theorem Th16: M c= N implies (x in M implies x in N) & (x is Vector of M implies x is Vector of N) proof assume A1: M c= N; thus x in M implies x in N proof assume A2: x in M; reconsider M' = M as Subspace of N by A1,Def7; x in M' by A2; hence thesis by VECTSP_4:17; end; thus x is Vector of M implies x is Vector of N proof assume A3: x is Vector of M; reconsider M' = M as Subspace of N by A1,Def7; x is Vector of M' by A3; hence thesis by VECTSP_4:18; end; end; theorem 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) proof assume A1: M c= N; thus 0.M = 0.N proof reconsider M' = M as Subspace of N by A1,Def7; 0.M' = 0.N by VECTSP_4:19; hence thesis; end; thus m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 proof assume A2: m1 = n1 & m2 = n2; reconsider M' = M as Subspace of N by A1,Def7; reconsider m1'=m1, m2'=m2 as Vector of M'; m1' = n1 & m2' = n2 by A2; hence thesis by VECTSP_4:21; end; thus m = n implies r * m = r * n proof assume A3: m = n; reconsider M' = M as Subspace of N by A1,Def7; reconsider m'=m as Vector of M'; m' = n by A3; hence thesis by VECTSP_4:22; end; thus m = n implies - n = - m proof assume A4: m = n; reconsider M' = M as Subspace of N by A1,Def7; reconsider m'=m as Vector of M'; m' = n by A4; hence thesis by VECTSP_4:23; end; thus m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 proof assume A5: m1 = n1 & m2 = n2; reconsider M' = M as Subspace of N by A1,Def7; reconsider m1'=m1, m2'=m2 as Vector of M'; m1' = n1 & m2' = n2 by A5; hence thesis by VECTSP_4:24; end; thus 0.N in M proof reconsider M' = M as Subspace of N by A1,Def7; 0.N in M' by VECTSP_4:25; hence thesis; end; thus 0.M in N proof reconsider M' = M as Subspace of N by A1,Def7; 0.M' in N by VECTSP_4:27; hence thesis; end; thus n1 in M & n2 in M implies n1 + n2 in M proof assume A6: n1 in M & n2 in M; reconsider M' = M as Subspace of N by A1,Def7; n1 in M' & n2 in M' by A6; hence thesis by VECTSP_4:28; end; thus n in M implies r * n in M proof assume A7: n in M; reconsider M' = M as Subspace of N by A1,Def7; n in M' by A7; hence thesis by VECTSP_4:29; end; thus n in M implies - n in M proof assume A8: n in M; reconsider M' = M as Subspace of N by A1,Def7; n in M' by A8; hence thesis by VECTSP_4:30; end; thus n1 in M & n2 in M implies n1 - n2 in M proof assume A9: n1 in M & n2 in M; reconsider M' = M as Subspace of N by A1,Def7; n1 in M' & n2 in M' by A9; hence thesis by VECTSP_4:31; end; end; theorem 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 proof assume A1: M1 c= N & M2 c= N; thus 0.M1 = 0.M2 proof reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7; 0.M1' = 0.M2' by VECTSP_4:20; hence thesis; end; thus 0.M1 in M2 proof reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7; 0.M1' in M2' by VECTSP_4:26; hence thesis; end; thus the carrier of M1 c= the carrier of M2 implies M1 c= M2 proof assume A2: the carrier of M1 c= the carrier of M2; reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7; M1' is Subspace of M2' by A2,VECTSP_4:35; hence thesis by Def7; end; thus (for n st n in M1 holds n in M2) implies M1 c= M2 proof assume A3: for n st n in M1 holds n in M2; reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7; M1' is Subspace of M2' by A3,VECTSP_4:36; hence thesis by Def7; end; thus the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 proof assume that A4: the carrier of M1 = the carrier of M2 and A5: M1 is strict & M2 is strict; reconsider M1'=M1 as strict Subspace of N by A1,A5,Def7; reconsider M2'=M2 as strict Subspace of N by A1,A5,Def7; M1' = M2' by A4,VECTSP_4:37; hence thesis; end; thus (0).M1 c= M2 proof reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7; (0).M1' is Subspace of M2' by VECTSP_4:51; hence thesis by Def7; end; end; canceled 2; theorem for V,M being strict LeftMod of K holds V c= M & M c= V implies V = M proof let V,M be strict LeftMod of K such that A1: V c= M and A2: M c= V; A3: V is Subspace of M by A1,Def7; M is Subspace of V by A2,Def7; hence thesis by A3,VECTSP_4:33; end; theorem V c= M & M c= N implies V c= N proof assume V c= M & M c= N; then V is Subspace of M & M is Subspace of N by Def7; then V is Subspace of N by VECTSP_4:34; hence thesis by Def7; end; theorem M c= N implies (0).M c= N proof assume M c= N; then reconsider M' = M as Subspace of N by Def7; (0).M' is Subspace of N by VECTSP_4:49; hence thesis by Def7; end; theorem M c= N implies (0).N c= M proof assume M c= N; then reconsider M' = M as Subspace of N by Def7; (0).N is Subspace of M' by VECTSP_4:50; hence thesis by Def7; end; theorem M c= N implies M c= (Omega).N proof assume M c= N; then A1: M is Subspace of N by Def7; N is Subspace of (Omega).N by Th4; then M is Subspace of (Omega).N by A1,VECTSP_4:34; hence thesis by Def7; end; theorem W1 c= W1 + W2 & W2 c= W1 + W2 proof W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 by VECTSP_5:11; hence thesis by Def7; end; theorem W1 /\ W2 c= W1 & W1 /\ W2 c= W2 proof W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 by VECTSP_5:20; hence thesis by Def7; end; theorem W1 c= W2 implies W1 /\ W3 c= W2 /\ W3 proof W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 by VECTSP_5:22; hence thesis by Def7; end; theorem W1 c= W3 implies W1 /\ W2 c= W3 proof W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 by VECTSP_5:23; hence thesis by Def7; end; theorem W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3 proof W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 by VECTSP_5:24; hence thesis by Def7; end; theorem W1 /\ W2 c= W1 + W2 proof W1 /\ W2 is Subspace of W1 + W2 by VECTSP_5:29; hence thesis by Def7; end; theorem (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3) proof (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by VECTSP_5:32; hence thesis by Def7; end; theorem W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) proof W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by VECTSP_5:33; hence thesis by Def7; end; theorem W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3) proof W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by VECTSP_5:34; hence thesis by Def7; end; theorem W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) proof W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by VECTSP_5:35; hence thesis by Def7; end; theorem W1 c= W2 implies W1 c= W2 + W3 proof W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 by VECTSP_5:39; hence thesis by Def7; end; theorem W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3 proof W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 by VECTSP_5:40; hence thesis by Def7; end; theorem for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B) proof let A,B be Subset of V; assume A c= B; then Lin(A) is Subspace of Lin(B) by MOD_3:17; hence thesis by Def7; end; theorem for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B) proof let A,B be Subset of V; Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B) by MOD_3:20; hence thesis by Def7; end; theorem Th40: M1 c= M2 implies [#]M1 c= [#]M2 proof assume A1: M1 c= M2; let x; assume x in [#]M1; then x in M1 by Th10; then x in M2 by A1,Th16; hence thesis by Th10; end; theorem Th41: W1 c= W2 iff for a st a in W1 holds a in W2 proof W1 c= W2 iff W1 is Subspace of W2 by Def7; hence thesis by VECTSP_4:16,36; end; theorem Th42: W1 c= W2 iff [#]W1 c= [#]W2 proof thus W1 c= W2 implies [#]W1 c= [#]W2 by Th40; assume A1: [#]W1 c= [#]W2; now let a; assume a in W1; then a in [#]W1 by Th10; hence a in W2 by A1,Th10;end; hence thesis by Th41; end; theorem W1 c= W2 iff @[#]W1 c= @[#]W2 proof @[#]W1 = [#]W1 & @[#]W2 = [#]W2 by Def5; hence thesis by Th42; end; theorem (0).W c= V & (0).V c= W & (0).W1 c= W2 proof A1: (0).W is Subspace of V by VECTSP_4:49; A2: (0).V is Subspace of W by VECTSP_4:50; A3: (0).W1 is Subspace of W2 by VECTSP_4:51; thus (0).W c= V by A1,Def7; thus (0).V c= W by A2,Def7; thus (0).W1 c= W2 by A3,Def7; end;

Back to top