The abstract of the Mizar article:

Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules

by

Michal Muzalewski

Received March 29, 1993

MML identifier: LMOD_7

[ Mizar article, MML identifier index ]

environ

 vocabulary BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2,
      FINSEQ_1, RMOD_3, ARYTM_1, RLVECT_1, REALSET1, RLVECT_3, BOOLE, MOD_3,
      RLSUB_1, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES,
      QC_LANG1, FINSEQ_4, ARYTM_3, LMOD_7;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, STRUCT_0, FUNCT_2,
      BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1, RLVECT_1,
      ANPROJ_1, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6,
      LMOD_5, MOD_3, LMOD_6;
 constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, ANPROJ_1, VECTSP_6,
      LMOD_5, MOD_3, LMOD_6, FINSOP_1, LATTICE2, MEMBERED, XBOOLE_0;
 clusters VECTSP_1, VECTSP_4, STRUCT_0, VECTSP_5, RELSET_1, SUBSET_1, LATTICES,
      LATTICE2, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin                     ::
                          ::  Schemes
                          ::

 scheme ElementEq {A()->set,P[set]} : for X1,X2 being Element of A() st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x])
 holds X1 = X2;

 scheme UnOpEq
  {A() -> non empty set, F(Element of A()) -> set}:
  for f1,f2 being UnOp of A() st
     (for a being Element of A() holds f1.(a) = F(a))
   & (for a being Element of A() holds f2.(a) = F(a))
  holds f1 = f2;

 scheme TriOpEq
  {A() -> non empty set,
   F(Element of A(),Element of A(),Element of A()) -> set}:
  for f1,f2 being TriOp of A() st
     (for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c))
   & (for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c))
  holds f1 = f2;

 scheme QuaOpEq {A() -> non empty set,
  F(Element of A(),Element of A(),Element of A(),Element of A()) -> set}:
  for f1,f2 being QuaOp of A() st
     (for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d))
   & (for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d))
  holds f1 = f2;

scheme Fraenkel1_Ex {A, D() -> non empty set,
 F(set) -> Element of D(), P[set]} : ex S being Subset of D()
 st S = {F(x) where x is Element of A() : P[x]};

scheme Fr_0 {A() -> non empty set, x() -> Element of A(), P[set]} : P[x()]
 provided  x() in {a where a is Element of A() : P[a]};

scheme Fr_1 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]} :
 a() in X() iff P[a()] provided
  X() = {a where a is Element of A() : P[a]};

scheme Fr_2 {X() -> set, A() -> non empty set, a() -> Element of A(), P[set]}:
  P[a()]
 provided  a() in X() and  X() = {a where a is Element of A() : P[a]};

scheme Fr_3 {x() -> set, X() -> set, A() -> non empty set, P[set]} :
 x() in X() iff ex a being Element of A() st x()=a & P[a]
 provided  X() = {a where a is Element of A() : P[a]};

scheme Fr_4 {D1,D2() -> non empty set, B() -> set,
 a() -> Element of D1(), F(set) -> set, P[set,set], Q[set,set]} :
 a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b]
 provided  F(B()) = {a where a is Element of D1() : Q[a,B()]} and
  Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b];

begin :: Main Part

reserve x for set,
        K for Ring,
        r for Scalar of K,
        V for LeftMod of K,
        a,b,a1,a2 for Vector of V,
        A,A1,A2 for Subset of V,
        l for Linear_Combination of A,
        W for Subspace of V,
        Li for FinSequence of Submodules(V);

            ::
            ::    1. Auxiliary theorems about free-modules
            ::

theorem :: LMOD_7:1
 K is non trivial & A is linearly-independent implies not 0.V in A;

theorem :: LMOD_7:2
 not a in A implies l.a = 0.K;

theorem :: LMOD_7:3
   K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial;

theorem :: LMOD_7:4
 V is non trivial implies for A st A is base holds A <> {};

theorem :: LMOD_7:5
 A1 \/ A2 is linearly-independent & A1 misses A2
  implies Lin A1 /\ Lin A2 = (0).V;

theorem :: LMOD_7:6
 A is base & A = A1 \/ A2 & A1 misses A2 implies
  V is_the_direct_sum_of Lin A1,Lin A2;

begin               ::
                    :: 2. Domains of submodules
                    ::

definition let K,V;
  mode SUBMODULE_DOMAIN of V -> non empty set means
:: LMOD_7:def 1

 x in it implies x is strict Subspace of V;
end;

definition let K,V;
 redefine func Submodules(V) -> SUBMODULE_DOMAIN of V;
end;

definition let K,V; let D be SUBMODULE_DOMAIN of V;
 redefine mode Element of D -> strict Subspace of V;
end;

definition let K,V; let D be SUBMODULE_DOMAIN of V;
 cluster strict Element of D;
end;

definition let K,V;
  assume  V is non trivial;
  mode LINE of V -> strict Subspace of V means
:: LMOD_7:def 2
   ex a st a<>0.V & it = <:a:>;
end;

definition let K,V;
  mode LINE_DOMAIN of V -> non empty set means
:: LMOD_7:def 3
 x in it implies x is LINE of V;
end;

definition let K,V;
  func lines(V) -> LINE_DOMAIN of V means
:: LMOD_7:def 4
   x in it iff x is LINE of V;
end;

definition let K,V; let D be LINE_DOMAIN of V;
 redefine mode Element of D -> LINE of V;
end;

definition let K,V;
  assume that
 V is non trivial and
 V is free;
  mode HIPERPLANE of V -> strict Subspace of V means
:: LMOD_7:def 5
   ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it;
end;

definition let K,V;
  mode HIPERPLANE_DOMAIN of V -> non empty set means
:: LMOD_7:def 6

 x in it implies x is HIPERPLANE of V;
end;

definition let K,V;
  func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means
:: LMOD_7:def 7
   x in it iff x is HIPERPLANE of V;
end;

definition let K,V; let D be HIPERPLANE_DOMAIN of V;
 redefine mode Element of D -> HIPERPLANE of V;
end;

begin   ::
        :: 3. Join and meet of finite sequences of submodules
        ::

definition let K,V,Li;
  func Sum Li -> Element of Submodules(V) equals
:: LMOD_7:def 8
    SubJoin(V) $$ Li;
  func /\ Li -> Element of Submodules(V) equals
:: LMOD_7:def 9
    SubMeet(V) $$ Li;
end;

canceled 5;

theorem :: LMOD_7:12
   for G being Lattice holds the L_join of G is commutative associative &
  the L_meet of G is commutative associative;

canceled;

theorem :: LMOD_7:14
   SubJoin(V) is commutative associative & SubJoin(V) has_a_unity
  & (0).V = the_unity_wrt SubJoin(V);

theorem :: LMOD_7:15
   SubMeet(V) is commutative associative & SubMeet(V)
  has_a_unity & (Omega).V = the_unity_wrt SubMeet(V);

begin                ::
                     :: 4. Sum of subsets of module
                     ::

definition let K,V,A1,A2;
  func A1 + A2 -> Subset of V means
:: LMOD_7:def 10
  x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
end;

begin                ::
                     ::    5. Vector of subset
                     ::

definition let K,V,A;
  assume  A <> {};
  mode Vector of A -> Vector of V means
:: LMOD_7:def 11
 it is Element of A;
end;

theorem :: LMOD_7:16
   A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of
A2;

                        ::
                        ::  6. Quotient modules
                        ::

theorem :: LMOD_7:17
 a2 in a1 + W iff a1 - a2 in W;

theorem :: LMOD_7:18
 a1 + W = a2 + W iff a1 - a2 in W;

definition let K,V,W;
  func V..W -> set means
:: LMOD_7:def 12
 x in it iff ex a st x = a + W;
end;

definition let K,V,W;
  cluster V..W -> non empty;
end;

definition let K,V,W,a;
  func a..W -> Element of V..W equals
:: LMOD_7:def 13
  a + W;
end;

theorem :: LMOD_7:19
 for x being Element of V..W ex a st x = a..W;

theorem :: LMOD_7:20
 a1..W = a2..W iff a1 - a2 in W;

reserve S1,S2 for Element of V..W;

definition let K,V,W,S1;
  func -S1 -> Element of V..W means
:: LMOD_7:def 14
   S1 = a..W implies it = (-a)..W;
  let S2;
  func S1 + S2 -> Element of V..W means
:: LMOD_7:def 15
 S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W;
end;

definition let K,V,W;
  func COMPL W -> UnOp of V..W means
:: LMOD_7:def 16
   it.S1 = -S1;
  func ADD W -> BinOp of V..W means
:: LMOD_7:def 17
 it.(S1,S2) = S1 + S2;
end;

definition let K,V,W;
  func V.W -> strict LoopStr equals
:: LMOD_7:def 18
  LoopStr(#V..W,ADD W,(0.V)..W#);
end;

definition let K,V,W;
 cluster V.W -> non empty;
end;

theorem :: LMOD_7:21
 a..W is Element of V.W;

definition let K,V,W,a;
  func a.W -> Element of V.W equals
:: LMOD_7:def 19
  a..W;
end;

theorem :: LMOD_7:22
 for x being Element of V.W ex a st x = a.W;

theorem :: LMOD_7:23
 a1.W = a2.W iff a1 - a2 in W;

theorem :: LMOD_7:24
 a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W;

definition let K,V,W;
 cluster V.W -> Abelian add-associative right_zeroed right_complementable;
end;

reserve S for Element of V.W;

definition let K,V,W,r,S;
  func r*S -> Element of V.W means
:: LMOD_7:def 20
 S = a.W implies it = (r*a).W;
end;

definition let K,V,W;
  func LMULT W -> Function of [:the carrier of K,the carrier of V.W:],
                                 the carrier of V.W means
:: LMOD_7:def 21
 it.(r,S) = r*S;
end;

begin

definition let K,V,W;
  func V/W -> strict VectSpStr over K equals
:: LMOD_7:def 22
  VectSpStr(#the carrier of V.W,the add of V.W,
   the Zero of V.W,LMULT W#);
end;

definition let K,V,W;
 cluster V/W -> non empty;
end;

canceled;

theorem :: LMOD_7:26
 a.W is Vector of V/W;

theorem :: LMOD_7:27
 for x being Vector of V/W holds x is Element of V.W;

definition let K,V,W,a;
  func a/W -> Vector of V/W equals
:: LMOD_7:def 23
  a.W;
end;

theorem :: LMOD_7:28
 for x being Vector of V/W ex a st x = a/W;

theorem :: LMOD_7:29
   a1/W = a2/W iff a1 - a2 in W;

theorem :: LMOD_7:30
 a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W;

theorem :: LMOD_7:31
 V/W is strict LeftMod of K;

definition let K,V,W;
  cluster V/W -> VectSp-like;
end;