The abstract of the Mizar article:

Operations on Subspaces in Real Linear Space

by

Wojciech A. Trybulec

Received September 20, 1989

MML identifier: RLSUB_2

[ Mizar article, MML identifier index ]

environ

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


begin

 reserve V for RealLinearSpace;
 reserve W,W1,W2,W3 for Subspace of V;
 reserve u,u1,u2,v,v1,v2 for VECTOR of V;
 reserve a,a1,a2 for Real;
 reserve X,Y for set;
 reserve x,y,y1,y2 for set;

::
::  Definitions of sum and intersection of subspaces.
::

 definition let V; let W1,W2;
  func W1 + W2 -> strict Subspace of V means
:: RLSUB_2:def 1
    the carrier of it = {v + u : v in W1 & u in W2};
 end;

 definition let V; let W1,W2;
  func W1 /\ W2 -> strict Subspace of V means
:: RLSUB_2:def 2
    the carrier of it = (the carrier of W1) /\ (the carrier of W2);
 end;

::
::  Definitional theorems of sum and intersection of subspaces.
::

canceled 4;

theorem :: RLSUB_2:5
 x in W1 + W2 iff
  (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2);

theorem :: RLSUB_2:6
 v in W1 or v in W2 implies v in W1 + W2;

theorem :: RLSUB_2:7
 x in W1 /\ W2 iff x in W1 & x in W2;

theorem :: RLSUB_2:8
  for W being strict Subspace of V holds
 W + W = W;

theorem :: RLSUB_2:9
   W1 + W2 = W2 + W1;

theorem :: RLSUB_2:10
 W1 + (W2 + W3) = (W1 + W2) + W3;

theorem :: RLSUB_2:11
 W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2;

theorem :: RLSUB_2:12
 for W2 being strict Subspace of V holds
 W1 is Subspace of W2 iff W1 + W2 = W2;

theorem :: RLSUB_2:13
 for W being strict Subspace of V holds
 (0).V + W = W & W + (0).V = W;

theorem :: RLSUB_2:14
 (0).V + (Omega).V = the RLSStruct of V & (Omega).
V + (0).V = the RLSStruct of V;

theorem :: RLSUB_2:15
 (Omega).V + W = the RLSStruct of V & W + (Omega).V = the RLSStruct of V;

theorem :: RLSUB_2:16
   for V being strict RealLinearSpace holds
 (Omega).V + (Omega).V = V;

theorem :: RLSUB_2:17
   for W being strict Subspace of V holds
 W /\ W = W;

theorem :: RLSUB_2:18
 W1 /\ W2 = W2 /\ W1;

theorem :: RLSUB_2:19
 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;

theorem :: RLSUB_2:20
 W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2;

theorem :: RLSUB_2:21
 for W1 being strict Subspace of V holds
 W1 is Subspace of W2 iff W1 /\ W2 = W1;

theorem :: RLSUB_2:22
 (0).V /\ W = (0).V & W /\ (0).V = (0).V;

theorem :: RLSUB_2:23
   (0).V /\ (Omega).V = (0).V & (Omega).V /\ (0).V = (0).V;

theorem :: RLSUB_2:24
 for W being strict Subspace of V holds
 (Omega).V /\ W = W & W /\ (Omega).V = W;

theorem :: RLSUB_2:25
   for V being strict RealLinearSpace holds
 (Omega).V /\ (Omega).V = V;

theorem :: RLSUB_2:26
   W1 /\ W2 is Subspace of W1 + W2;

theorem :: RLSUB_2:27
 for W2 being strict Subspace of V holds
 (W1 /\ W2) + W2 = W2;

theorem :: RLSUB_2:28
 for W1 being strict Subspace of V holds
 W1 /\ (W1 + W2) = W1;

theorem :: RLSUB_2:29
   (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3);

theorem :: RLSUB_2:30
 W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);

theorem :: RLSUB_2:31
   W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3);

theorem :: RLSUB_2:32
   W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);

theorem :: RLSUB_2:33
 W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

theorem :: RLSUB_2:34
   for W1,W2 being strict Subspace of V holds
 W1 + W2 = W2 iff W1 /\ W2 = W1;

theorem :: RLSUB_2:35
   for W2,W3 being strict Subspace of V holds
 W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3;

theorem :: RLSUB_2:36
   (ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2)) iff
  W1 is Subspace of W2 or W2 is Subspace of W1;

::
::  Introduction of a set of subspaces of real linear space.
::

 definition let V;
  func Subspaces(V) -> set means
:: RLSUB_2:def 3
    for x holds x in it iff x is strict Subspace of V;
 end;

 definition let V;
  cluster Subspaces(V) -> non empty;
end;



canceled 2;

theorem :: RLSUB_2:39
   for V being strict RealLinearSpace holds
 V in Subspaces(V);

::
::  Introduction of the direct sum of subspaces and
::  linear complement of subspace.
::

definition let V; let W1,W2;
 pred V is_the_direct_sum_of W1,W2 means
:: RLSUB_2:def 4
   the RLSStruct of V = W1 + W2 & W1 /\ W2 = (0).V;
end;

definition let V be RealLinearSpace; let W be Subspace of V;
 mode Linear_Compl of W -> Subspace of V means
:: RLSUB_2:def 5
   V is_the_direct_sum_of it,W;
end;

definition let V be RealLinearSpace; let W be Subspace of V;
 cluster strict Linear_Compl of W;
end;

canceled 2;

theorem :: RLSUB_2:42
   for V being RealLinearSpace, W1,W2 being Subspace of V holds
 V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;

theorem :: RLSUB_2:43
 for V being RealLinearSpace, W being Subspace of V,
     L being Linear_Compl of W holds
 V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;

::
::  Theorems concerning the direct sum of a subspaces,
::  linear complement of a subspace and coset of a subspace.
::

theorem :: RLSUB_2:44
 for V being RealLinearSpace, W being Subspace of V,
  L being Linear_Compl of W holds
 W + L = the RLSStruct of V & L + W = the RLSStruct of V;

theorem :: RLSUB_2:45
 for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W holds
 W /\ L = (0).V & L /\ W = (0).V;

theorem :: RLSUB_2:46
   V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1;

theorem :: RLSUB_2:47
 for V being RealLinearSpace holds
 V is_the_direct_sum_of (0).V,(Omega).V &
  V is_the_direct_sum_of (Omega).V,(0).V;

theorem :: RLSUB_2:48
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W holds
 W is Linear_Compl of L;

theorem :: RLSUB_2:49
   for V being RealLinearSpace holds
 (0).V is Linear_Compl of (Omega).V &
  (Omega).V is Linear_Compl of (0).V;

reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;

theorem :: RLSUB_2:50
 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;

theorem :: RLSUB_2:51
 for V being RealLinearSpace, W1,W2 being Subspace of V holds
 V is_the_direct_sum_of W1,W2 iff
  for C1 being Coset of W1, C2 being Coset of W2
   ex v being VECTOR of V st C1 /\ C2 = {v};

::
::  Decomposition of a vector.
::

theorem :: RLSUB_2:52
   for V being RealLinearSpace, W1,W2 being Subspace of V holds
 W1 + W2 = the RLSStruct of V iff
  for v being VECTOR of V
   ex v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2;

theorem :: RLSUB_2:53
 V is_the_direct_sum_of W1,W2 &
  v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies
   v1 = u1 & v2 = u2;

theorem :: RLSUB_2:54
   V = W1 + W2 &
  (ex v st for v1,v2,u1,u2 st
    v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
     v1 = u1 & v2 = u2) implies V is_the_direct_sum_of W1,W2;

reserve t1,t2 for Element of [:the carrier of V, the carrier of V:];



definition let V; let v; let W1,W2;
 assume  V is_the_direct_sum_of W1,W2;
 func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:] means
:: RLSUB_2:def 6
   v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;

canceled 4;

theorem :: RLSUB_2:59
 V is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;

theorem :: RLSUB_2:60
 V is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;

theorem :: RLSUB_2:61
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W, v being VECTOR of V,
   t being Element of [:the carrier of V, the carrier of V:] holds
 t`1 + t`2 = v & t`1 in W & t`2 in L implies t = v |-- (W,L);

theorem :: RLSUB_2:62
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 + (v |-- (W,L))`2 = v;

theorem :: RLSUB_2:63
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L;

theorem :: RLSUB_2:64
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 = (v |-- (L,W))`2;

theorem :: RLSUB_2:65
   for V being RealLinearSpace, W being Subspace of V,
   L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`2 = (v |-- (L,W))`1;

::
::  Introduction of operations on set of subspaces as binary operations.
::

reserve A1,A2,B for Element of Subspaces(V);

 definition let V;
  func SubJoin(V) -> BinOp of Subspaces(V) means
:: RLSUB_2:def 7
    for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
 end;

 definition let V;
  func SubMeet(V) -> BinOp of Subspaces(V) means
:: RLSUB_2:def 8
    for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
 end;

::
::  Definitional theorems of functions SubJoin, SubMeet.
::



definition let X be non empty set, m,u be BinOp of X;
 cluster LattStr(#X,m,u#) -> non empty;
end;

canceled 4;

theorem :: RLSUB_2:70
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is Lattice;

definition let V;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> Lattice-like;
end;

theorem :: RLSUB_2:71
 for V being RealLinearSpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is lower-bounded;

theorem :: RLSUB_2:72
 for V being RealLinearSpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is upper-bounded;

theorem :: RLSUB_2:73
 for V being RealLinearSpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is 01_Lattice;

theorem :: RLSUB_2:74
 for V being RealLinearSpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is modular;

reserve l for Lattice;
reserve a,b for Element of l;

theorem :: RLSUB_2:75
 for V being RealLinearSpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is complemented;

definition let V;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) ->
    lower-bounded upper-bounded modular complemented;
end;

::
::  Theorems concerning operations on subspaces (continuation). Proven
::  on the basis that set of subspaces with operations is a lattice.
::

theorem :: RLSUB_2:76
   for V being RealLinearSpace,
     W1,W2,W3 being strict Subspace of V holds
 W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3;

::
::  Auxiliary theorems.
::

theorem :: RLSUB_2:77
   X c< Y implies ex x st x in Y & not x in X;

theorem :: RLSUB_2:78
  for V being add-associative right_zeroed right_complementable
 (non empty LoopStr),
    v,v1,v2 being Element of V holds
 v = v1 + v2 iff v1 = v - v2;

theorem :: RLSUB_2:79
   for V being RealLinearSpace, W being strict Subspace of V holds
 (for v being VECTOR of V holds v in W) implies W = the RLSStruct of V;

theorem :: RLSUB_2:80
   ex C st v in C;

canceled 3;

theorem :: RLSUB_2:84
   (for a holds a "/\" b = b) implies b = Bottom l;

theorem :: RLSUB_2:85
   (for a holds a "\/" b = b) implies b = Top l;