The Mizar abstract of VECTSP

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Subspaces and Cosets of Subspaces in Vector Space
by
Wojciech A. Trybulec
Received July 27, 1990
MML identifier: VECTSP_4
[ Mizar article, MML identifier index ]
environ

 vocabulary RLVECT_1, VECTSP_1, ARYTM_1, BINOP_1, LATTICES, RLSUB_1, BOOLE,
      RELAT_1, FUNCT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      STRUCT_0, DOMAIN_1, BINOP_1, RLVECT_1, VECTSP_1;
 constructors GROUP_2, DOMAIN_1, BINOP_1, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin



 reserve x,y,y1,y2 for set;

 definition let GF be non empty HGrStr; let V be non empty VectSpStr over GF;
   let V1 be Subset of V;
  attr V1 is lineary-closed means
:: VECTSP_4:def 1
    (for v,u being Element of V st v in V1 & u in V1
       holds v + u in V1) &
    (for a being Element of GF,
        v being Element of V
     st v in V1 holds a * v in V1);
 end;

canceled 3;

theorem :: VECTSP_4:4
 for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1 be Subset of V
  st V1 <> {} & V1 is lineary-closed holds 0.V in V1;

theorem :: VECTSP_4:5
 for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1 be Subset of V
  st V1 is lineary-closed
  for v being Element of V st v in V1 holds - v in V1;

theorem :: VECTSP_4:6
   for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1 be Subset of V
  st V1 is lineary-closed
 for v,u being Element of V
     st v in V1 & u in V1 holds v - u in V1;

theorem :: VECTSP_4:7
 for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF)
  holds {0.V} is lineary-closed;

theorem :: VECTSP_4:8
   for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1 be Subset of V
 st the carrier of V = V1 holds V1 is lineary-closed;

theorem :: VECTSP_4:9
   for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1,V2,V3 be Subset of V
  st V1 is lineary-closed & V2 is lineary-closed &
     V3 = {v + u where
                 v is Element of V,
                 u is Element of V
             : v in V1 & u in V2}
  holds V3 is lineary-closed;

theorem :: VECTSP_4:10
   for GF be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
             right_complementable VectSp-like (non empty VectSpStr over GF),
     V1,V2 be Subset of V
   st V1 is lineary-closed & V2 is lineary-closed
 holds V1 /\ V2 is lineary-closed;

 definition
   let GF be add-associative right_zeroed right_complementable
            Abelian associative left_unital distributive
            (non empty doubleLoopStr),
       V be Abelian add-associative right_zeroed
            right_complementable VectSp-like (non empty VectSpStr over GF);
  mode Subspace of V -> Abelian add-associative right_zeroed
          right_complementable VectSp-like (non empty VectSpStr over GF) means
:: VECTSP_4:def 2

    the carrier of it c= the carrier of V &
    the Zero of it = the Zero of V &
    the add of it =
     (the add of V) | [:the carrier of it,the carrier of it:] &
    the lmult of it =
     (the lmult of V) | [:the carrier of GF, the carrier of it:];
 end;

 reserve GF for add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr),
         V,X,Y for Abelian add-associative right_zeroed
              right_complementable VectSp-like (non empty VectSpStr over GF);
 reserve a for Element of GF;
 reserve u,u1,u2,v,v1,v2 for Element of V;
 reserve W,W1,W2 for Subspace of V;
 reserve V1 for Subset of V;
 reserve w,w1,w2 for Element of W;

canceled 5;

theorem :: VECTSP_4:16
   x in W1 & W1 is Subspace of W2 implies x in W2;

theorem :: VECTSP_4:17
 x in W implies x in V;

theorem :: VECTSP_4:18
 w is Element of V;

theorem :: VECTSP_4:19
 0.W = 0.V;

theorem :: VECTSP_4:20
   0.W1 = 0.W2;

theorem :: VECTSP_4:21
 w1 = v & w2 = u implies w1 + w2 = v + u;

theorem :: VECTSP_4:22
 w = v implies a * w = a * v;

theorem :: VECTSP_4:23
 w = v implies - v = - w;

theorem :: VECTSP_4:24
 w1 = v & w2 = u implies w1 - w2 = v - u;

theorem :: VECTSP_4:25
 0.V in W;

theorem :: VECTSP_4:26
   0.W1 in W2;

theorem :: VECTSP_4:27
   0.W in V;

theorem :: VECTSP_4:28
 u in W & v in W implies u + v in W;

theorem :: VECTSP_4:29
 v in W implies a * v in W;

theorem :: VECTSP_4:30
 v in W implies - v in W;

theorem :: VECTSP_4:31
 u in W & v in W implies u - v in W;

theorem :: VECTSP_4:32
 V is Subspace of V;

theorem :: VECTSP_4:33
 for X,V being strict Abelian add-associative right_zeroed
              right_complementable VectSp-like (non empty VectSpStr over GF)
 holds V is Subspace of X & X is Subspace of V implies V = X;

theorem :: VECTSP_4:34
 V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;

theorem :: VECTSP_4:35
 the carrier of W1 c= the carrier of W2 implies
  W1 is Subspace of W2;

theorem :: VECTSP_4:36
   (for v st v in W1 holds v in W2) implies W1 is Subspace of W2;

definition let GF be add-associative right_zeroed right_complementable
             Abelian associative left_unital distributive
             (non empty doubleLoopStr),
               V be Abelian add-associative right_zeroed
                right_complementable VectSp-like (non empty VectSpStr over GF);
 cluster strict Subspace of V;
end;

theorem :: VECTSP_4:37
 for W1,W2 being strict Subspace of V st
 the carrier of W1 = the carrier of W2
  holds W1 = W2;

theorem :: VECTSP_4:38
 for W1,W2 being strict Subspace of V st
 (for v holds v in W1 iff v in W2)
 holds W1 = W2;

theorem :: VECTSP_4:39
   for V being strict Abelian add-associative right_zeroed
              right_complementable VectSp-like (non empty VectSpStr over GF),
     W being strict Subspace of V holds
 the carrier of W = the carrier of V implies
  W = V;

theorem :: VECTSP_4:40
   for V being strict Abelian add-associative right_zeroed
              right_complementable VectSp-like (non empty VectSpStr over GF),
     W being strict Subspace of V holds
 (for v being Element of V holds v in W) implies W = V;

theorem :: VECTSP_4:41
   the carrier of W = V1 implies V1 is lineary-closed;

theorem :: VECTSP_4:42
 V1 <> {} & V1 is lineary-closed implies
  ex W being strict Subspace of V st
   V1 = the carrier of W;

 definition let GF; let V;
  func (0).V -> strict Subspace of V means
:: VECTSP_4:def 3
    the carrier of it = {0.V};
 end;

 definition let GF; let V;
  func (Omega).V -> strict Subspace of V equals
:: VECTSP_4:def 4
    the VectSpStr of V;
 end;

canceled 3;

theorem :: VECTSP_4:46
   x in (0).V iff x = 0.V;

theorem :: VECTSP_4:47
 (0).W = (0).V;

theorem :: VECTSP_4:48
 (0).W1 = (0).W2;

theorem :: VECTSP_4:49
   (0).W is Subspace of V;

theorem :: VECTSP_4:50
   (0).V is Subspace of W;

theorem :: VECTSP_4:51
   (0).W1 is Subspace of W2;

canceled;

theorem :: VECTSP_4:53
   for V being strict Abelian add-associative right_zeroed
           right_complementable VectSp-like (non empty VectSpStr over GF) holds
 V is Subspace of (Omega).V;

 definition let GF; let V; let v,W;
  func v + W -> Subset of V equals
:: VECTSP_4:def 5
    {v + u : u in W};
 end;

 definition let GF; let V; let W;
  mode Coset of W -> Subset of V means
:: VECTSP_4:def 6
    ex v st it = v + W;
 end;

reserve B,C for Coset of W;

canceled 3;

theorem :: VECTSP_4:57
x in v + W iff ex u st u in W & x = v + u;

theorem :: VECTSP_4:58
 0.V in v + W iff v in W;

theorem :: VECTSP_4:59
 v in v + W;

theorem :: VECTSP_4:60
   0.V + W = the carrier of W;

theorem :: VECTSP_4:61
 v + (0).V = {v};

theorem :: VECTSP_4:62
 v + (Omega).V = the carrier of V;

theorem :: VECTSP_4:63
 0.V in v + W iff v + W = the carrier of W;

theorem :: VECTSP_4:64
   v in W iff v + W = the carrier of W;

theorem :: VECTSP_4:65
 v in W implies (a * v) + W = the carrier of W;

theorem :: VECTSP_4:66
 for GF being Field, V being VectSp of GF,
     a being Element of GF,
     v being Element of V,
     W being Subspace of V
  st a <> 0.GF & (a * v) + W = the carrier of W holds v in W;

theorem :: VECTSP_4:67
   for GF being Field, V being VectSp of GF,
     v being Element of V,
     W being Subspace of V
 holds v in W iff - v + W = the carrier of W;

theorem :: VECTSP_4:68
 u in W iff v + W = (v + u) + W;

theorem :: VECTSP_4:69
   u in W iff v + W = (v - u) + W;

theorem :: VECTSP_4:70
 v in u + W iff u + W = v + W;

theorem :: VECTSP_4:71
 u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: VECTSP_4:72
   for GF being Field, V being VectSp of GF,
     a being Element of GF,
     v being Element of V,
     W being Subspace of V
 st a <> 1_ GF & a * v in v + W holds v in W;

theorem :: VECTSP_4:73
 v in W implies a * v in v + W;

theorem :: VECTSP_4:74
   v in W implies - v in v + W;

theorem :: VECTSP_4:75
 u + v in v + W iff u in W;

theorem :: VECTSP_4:76
   v - u in v + W iff u in W;

canceled;

theorem :: VECTSP_4:78
   u in v + W iff
  (ex v1 st v1 in W & u = v - v1);

theorem :: VECTSP_4:79
 (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;

theorem :: VECTSP_4:80
 v + W = u + W implies
  (ex v1 st v1 in W & v + v1 = u);

theorem :: VECTSP_4:81
 v + W = u + W implies
  (ex v1 st v1 in W & v - v1 = u);

theorem :: VECTSP_4:82
 for W1,W2 being strict Subspace of V
  holds v + W1 = v + W2 iff W1 = W2;

theorem :: VECTSP_4:83
 for W1,W2 being strict Subspace of V st v + W1 = u + W2
  holds W1 = W2;

theorem :: VECTSP_4:84
ex C st v in C;

theorem :: VECTSP_4:85
   C is lineary-closed iff C = the carrier of W;

theorem :: VECTSP_4:86
   for W1,W2 being strict Subspace of V,
     C1 being Coset of W1, C2 being Coset of W2 st C1 = C2
     holds W1 = W2;

theorem :: VECTSP_4:87
   {v} is Coset of (0).V;

theorem :: VECTSP_4:88
   V1 is Coset of (0).V implies (ex v st V1 = {v});

theorem :: VECTSP_4:89
   the carrier of W is Coset of W;

theorem :: VECTSP_4:90
   the carrier of V is Coset of (Omega).V;

theorem :: VECTSP_4:91
   V1 is Coset of (Omega).V implies V1 = the carrier of V;

theorem :: VECTSP_4:92
   0.V in C iff C = the carrier of W;

theorem :: VECTSP_4:93
 u in C iff C = u + W;

theorem :: VECTSP_4:94
   u in C & v in C implies (ex v1 st v1 in W & u + v1 = v);

theorem :: VECTSP_4:95
   u in C & v in C implies (ex v1 st v1 in W & u - v1 = v);

theorem :: VECTSP_4:96
   (ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: VECTSP_4:97
   u in B & u in C implies B = C;

::
::  Auxiliary theorems.
::



canceled 5;

theorem :: VECTSP_4:103
   for GF be add-associative right_zeroed right_complementable
    Abelian commutative associative left_unital distributive
         (non empty doubleLoopStr),
     V be Abelian add-associative right_zeroed
          right_complementable VectSp-like (non empty VectSpStr over GF),
  a,b being Element of GF,
  v being Element of V
  holds (a - b) * v = a * v - b * v;
The abstract of the Mizar article:

Subspaces and Cosets of Subspaces in Vector Space
