LMOD_6

:: Submodules
::  by Micha{\l} Muzalewski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2026 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;
 definitions TARSKI, XBOOLE_0;
 equalities XBOOLE_0, REALSET1, STRUCT_0;
 expansions STRUCT_0;
 theorems FUNCT_2, MOD_3, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6,
      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;

notation
  let K, V;
  synonym Submodules(V) for Subspaces(V);
end;

theorem
  M1 = the ModuleStr of M2 implies (x in M1 iff x in M2);

theorem
  for v being Vector of the ModuleStr of V st a=v holds r*a = r*v
proof
  let v be Vector of (the ModuleStr of V) such that
A1: a=v;
  thus r*a = (the lmult of V).(r,a) by VECTSP_1:def 12
    .= r*v by A1,VECTSP_1:def 12;
end;

theorem Th3:
  the ModuleStr of V is strict Subspace of V
proof
  (Omega).V = the ModuleStr 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 ModuleStr of V by VECTSP_4:def 4;
  then
A2: 0.V = 0.W;
  dom(the lmult of W) = [:the carrier of K, the carrier of W:] by FUNCT_2:def 1
;
  then
A3: the lmult of V = (the lmult of W) | [:the carrier of K, the carrier of V
  :] by A1,RELAT_1:68;
  dom(the addF of W) = [:the carrier of W,the carrier of W:] by FUNCT_2:def 1;
  then the addF of V = (the addF of W)||the carrier of V by A1,RELAT_1:68;
  hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;

begin

definition
  let K;
  redefine attr K is trivial means  :: redefines trivial (STRUCT_0, redefinition) → trivial (STRUCT_0, redefinition) → trivial (STRUCT_0, definition)
  0.K = 1_K;
  compatibility
  proof
    thus K is trivial implies 0.K = 1_K;
    assume
A1: 0.K = 1_K;
    now
      let x be Scalar of K;
      thus x = x*(1_K)
        .= 0.K by A1;
    end;
    hence thesis;
  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;
A2: now
    let a;
    thus a = 1_K*a
      .= 0.V by A1,VECTSP_1:14;
  end;
  now
    let r;
    thus r = r*1_K
      .= 0.K by A1;
  end;
  hence thesis by A2;
end;

theorem
  K is trivial implies V is trivial
by Th5;

theorem
  V is trivial iff the ModuleStr of V = (0).V
proof
  set X = the carrier of (0).V;
  reconsider W = the ModuleStr of V as strict Subspace of V by Th3;
  reconsider Z=(0).V as Subspace of W by VECTSP_4:39;
A1: now
    assume W <> Z;
    then consider a such that
A2: not a in Z by VECTSP_4:32;
    not a in X by A2;
    then not a in {0.V} by VECTSP_4:def 3;
    then a <> 0.V by TARSKI:def 1;
    hence V is non trivial;
  end;
  now
    assume V is non trivial;
    then consider a such that
A3: a <> 0.V;
    not a in {0.V} by A3,TARSKI:def 1;
    then not a in X by VECTSP_4:def 3;
    hence W <> (0).V;
  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;

theorem Th8:
  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;
  hence thesis by XBOOLE_1:1;
end;

definition
  let K,V,W;
  let A be Subset of W;

  func @A -> Subset of V equals
  A;
  coherence by Th8;
end;

registration
  let K,V,W;
  let A be non empty Subset of W;
  cluster @A -> non empty;
  coherence;
end;

theorem
  x in [#]V iff x in V;

theorem
  x in @[#]W iff x in W;

theorem Th11:
  A c= [#]Lin(A)
proof
  let x be object;
  assume x in A;
  then x in Lin(A) by MOD_3:5;
  hence thesis;
end;

theorem Th12:
  A<>{} & A is linearly-closed implies Sum(l) in A
proof
  assume
A1: A<>{} & A is linearly-closed;
  now
    per cases;
    suppose
      0.K<>1_K;
      hence thesis by A1,VECTSP_6:14;
    end;
    suppose
      0.K=1_K;
      then K is trivial;
      then Sum(l) = 0.V by Th5;
      hence thesis by A1,VECTSP_4:1;
    end;
  end;
  hence thesis;
end;

theorem
  0.V in A & A is linearly-closed implies A = [#]Lin(A)
proof
  assume
A1: 0.V in A & A is linearly-closed;
  thus A c= [#]Lin(A) by Th11;
  let x be object;
  assume x in [#]Lin(A);
  then x in Lin(A);
  then ex l st x = Sum(l) by MOD_3:4;
  hence thesis by A1,Th12;
end;

begin ::   2. Cyclic submodule

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

  M is Subspace of N;
  reflexivity by VECTSP_4:24;
end;

theorem Th14:
 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)
by VECTSP_4:9,VECTSP_4:10;

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)

by VECTSP_4:11,VECTSP_4:13,VECTSP_4:14,VECTSP_4:15,VECTSP_4:16,VECTSP_4:17,
VECTSP_4:19,VECTSP_4:20,VECTSP_4:21,VECTSP_4:22,VECTSP_4:23;

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
by VECTSP_4:12,VECTSP_4:18,VECTSP_4:27,VECTSP_4:28,VECTSP_4:29,VECTSP_4:40;

theorem
  for V,M being strict LeftMod of K holds V c= M & M c= V implies V = M
by VECTSP_4:25;

theorem
  V c= M & M c= N implies V c= N
by VECTSP_4:26;

theorem
  M c= N implies (0).M c= N
by VECTSP_4:38;

theorem
  M c= N implies (0).N c= M
by VECTSP_4:39;

theorem
  M c= N implies M c= (Omega).N
proof
  assume M c= N;
  then
A1: M is Subspace of N;
  N is Subspace of (Omega).N by Th4;
  then M is Subspace of (Omega).N by A1,VECTSP_4:26;
  hence thesis;
end;

theorem
  W1 c= W1 + W2 & W2 c= W1 + W2
by VECTSP_5:7;

theorem
  W1 /\ W2 c= W1 & W1 /\ W2 c= W2
by VECTSP_5:15;

theorem
  W1 c= W2 implies W1 /\ W3 c= W2 /\ W3
by VECTSP_5:17;

theorem
  W1 c= W3 implies W1 /\ W2 c= W3
by VECTSP_5:18;

theorem
  W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3
by VECTSP_5:19;

theorem
  W1 /\ W2 c= W1 + W2
by VECTSP_5:23;

theorem
  (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
by VECTSP_5:26;

theorem
  W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
by VECTSP_5:27;

theorem
  W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
by VECTSP_5:28;

theorem
  W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by VECTSP_5:29;

theorem
  W1 c= W2 implies W1 c= W2 + W3
by VECTSP_5:33;

theorem
  W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3
by VECTSP_5:34;

theorem
  for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B)
by MOD_3:10;

theorem
  for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B)
by MOD_3:13;

theorem Th36:
  M1 c= M2 implies [#]M1 c= [#]M2
proof
  assume
A1: M1 c= M2;
  let x be object;
  assume x in [#]M1;
  then x in M1;
  then x in M2 by A1,Th14;
  hence thesis;
end;

theorem Th37:
  W1 c= W2 iff for a st a in W1 holds a in W2
by VECTSP_4:8,VECTSP_4:28;

theorem Th38:
  W1 c= W2 iff [#]W1 c= [#]W2
proof
  thus W1 c= W2 implies [#]W1 c= [#]W2 by Th36;
  assume [#]W1 c= [#]W2;
  then for a st a in W1 holds a in W2;
  hence thesis by Th37;
end;

theorem
  W1 c= W2 iff @[#]W1 c= @[#]W2 by Th38;

theorem
  (0).W c= V & (0).V c= W & (0).W1 c= W2 by VECTSP_4:38,39,40;