The abstract of the Mizar article:

Subspaces and Cosets of Subspaces in Real Linear Space

by

Wojciech A. Trybulec

Received July 24, 1989

MML identifier: RLSUB_1

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, BOOLE, ARYTM_1, RELAT_1, FUNCT_1, BINOP_1, RLSUB_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, MCART_1,
      FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, BINOP_1, STRUCT_0, RLVECT_1;
 constructors REAL_1, DOMAIN_1, RLVECT_1, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, RLVECT_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

 reserve V,X,Y for RealLinearSpace;
 reserve u,u1,u2,v,v1,v2 for VECTOR of V;
 reserve a,b for Real;
 reserve V1,V2,V3 for Subset of V;
 reserve x for set;

::
::  Introduction of predicate lineary closed subsets of the carrier.
::

 definition let V; let V1;
  attr V1 is lineary-closed means
:: RLSUB_1:def 1

    (for v,u st v in V1 & u in V1 holds v + u in V1) &
    (for a,v st v in V1 holds a * v in V1);
 end;

canceled 3;

theorem :: RLSUB_1:4
 V1 <> {} & V1 is lineary-closed implies 0.V in V1;

theorem :: RLSUB_1:5
 V1 is lineary-closed implies (for v st v in V1 holds - v in V1);

theorem :: RLSUB_1:6
   V1 is lineary-closed implies
  (for v,u st v in V1 & u in V1 holds v - u in V1);

theorem :: RLSUB_1:7
 {0.V} is lineary-closed;

theorem :: RLSUB_1:8
   the carrier of V = V1 implies V1 is lineary-closed;

theorem :: RLSUB_1:9
   V1 is lineary-closed & V2 is lineary-closed &
  V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed;

theorem :: RLSUB_1:10
   V1 is lineary-closed & V2 is lineary-closed implies
  V1 /\ V2 is lineary-closed;

 definition let V;
  mode Subspace of V -> RealLinearSpace means
:: RLSUB_1: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 Mult of it = (the Mult of V) | [:REAL, the carrier of it:];
 end;

 reserve W,W1,W2 for Subspace of V;
 reserve w,w1,w2 for VECTOR of W;

::
::  Axioms of the subspaces of real linear spaces.
::

canceled 5;

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

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

theorem :: RLSUB_1:18
 w is VECTOR of V;

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

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

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

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

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

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

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

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

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

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

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

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

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

 reserve D for non empty set;
 reserve d1 for Element of D;
 reserve A for BinOp of D;
 reserve M for Function of [:REAL,D:],D;

theorem :: RLSUB_1:32
 V1 = D &
 d1 = 0.V &
 A = (the add of V) | [:V1,V1:] &
 M = (the Mult of V) | [:REAL,V1:] implies
           RLSStruct (# D,d1,A,M #) is Subspace of V;

theorem :: RLSUB_1:33
 V is Subspace of V;

theorem :: RLSUB_1:34
 for V,X being strict RealLinearSpace holds
 V is Subspace of X & X is Subspace of V implies V = X;

theorem :: RLSUB_1:35
 V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;

theorem :: RLSUB_1:36
 the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2;

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

definition let V;
 cluster strict Subspace of V;
end;

theorem :: RLSUB_1:38
 for W1,W2 being strict Subspace of V holds
 the carrier of W1 = the carrier of W2 implies W1 = W2;

theorem :: RLSUB_1:39
 for W1,W2 being strict Subspace of V holds
 (for v holds v in W1 iff v in W2) implies W1 = W2;

theorem :: RLSUB_1:40
   for V being strict RealLinearSpace, W being strict Subspace of V holds
 the carrier of W = the carrier of V implies W = V;

theorem :: RLSUB_1:41
   for V being strict RealLinearSpace, W being strict Subspace of V holds
 (for v being VECTOR of V holds v in W iff v in V) implies W = V;

theorem :: RLSUB_1:42
   the carrier of W = V1 implies V1 is lineary-closed;

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

::
::  Definition of zero subspace and improper subspace of real linear space.
::

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

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

::
::  Definitional theorems of zero subspace and improper subspace.
::

canceled 4;

theorem :: RLSUB_1:48
 (0).W = (0).V;

theorem :: RLSUB_1:49
 (0).W1 = (0).W2;

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

theorem :: RLSUB_1:51
   (0).V is Subspace of W;

theorem :: RLSUB_1:52
   (0).W1 is Subspace of W2;

canceled;

theorem :: RLSUB_1:54
   for V being strict RealLinearSpace holds V is Subspace of (Omega).V;

::
::  Introduction of the cosets of subspace.
::

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

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

reserve B,C for Coset of W;

::
::  Definitional theorems of the cosets.
::

canceled 3;

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

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

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

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

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

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

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

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

theorem :: RLSUB_1:66
 a <> 0 & (a * v) + W = the carrier of W implies v in W;

theorem :: RLSUB_1:67
 v in W iff - v + W = the carrier of W;

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

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

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

theorem :: RLSUB_1:71
 v + W = (- v) + W iff v in W;

theorem :: RLSUB_1:72
 u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: RLSUB_1:73
   u in v + W & u in (- v) + W implies v in W;

theorem :: RLSUB_1:74
 a <> 1 & a * v in v + W implies v in W;

theorem :: RLSUB_1:75
 v in W implies a * v in v + W;

theorem :: RLSUB_1:76
   - v in v + W iff v in W;

theorem :: RLSUB_1:77
 u + v in v + W iff u in W;

theorem :: RLSUB_1:78
   v - u in v + W iff u in W;

theorem :: RLSUB_1:79
 u in v + W iff
  (ex v1 st v1 in W & u = v + v1);

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

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

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

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

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

theorem :: RLSUB_1:85
 for W1,W2 being strict Subspace of V holds
 v + W1 = u + W2 implies W1 = W2;

::
::  Theorems concerning cosets of subspace
::  regarded as subsets of the carrier.
::




theorem :: RLSUB_1:86
   C is lineary-closed iff C = the carrier of W;

theorem :: RLSUB_1:87
   for W1,W2 being strict Subspace of V,
  C1 being Coset of W1, C2 being Coset of W2 holds
 C1 = C2 implies W1 = W2;

theorem :: RLSUB_1:88
   {v} is Coset of (0).V;

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

theorem :: RLSUB_1:90
   the carrier of W is Coset of W;

theorem :: RLSUB_1:91
   the carrier of V is Coset of (Omega).V;

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

theorem :: RLSUB_1:93
   0.V in C iff C = the carrier of W;

theorem :: RLSUB_1:94
 u in C iff C = u + W;

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

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

theorem :: RLSUB_1:97
   (ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: RLSUB_1:98
   u in B & u in C implies B = C;