The abstract of the Mizar article:

Operations on Subspaces in Vector Space

by

Wojciech A. Trybulec

Received July 27, 1990

MML identifier: VECTSP_5

[ Mizar article, MML identifier index ]

environ

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


begin

 reserve GF for add-associative right_zeroed right_complementable
      Abelian associative left_unital distributive (non empty doubleLoopStr);
 reserve M for Abelian add-associative right_zeroed
           right_complementable VectSp-like (non empty VectSpStr over GF);
 reserve W,W1,W2,W3 for Subspace of M;
 reserve u,u1,u2,v,v1,v2 for Element of M;
 reserve X,Y,x,y,y1,y2 for set;

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

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

canceled 4;

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

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

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

theorem :: VECTSP_5:8
  for W being strict Subspace of M holds W + W = W;

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

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

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

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

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

theorem :: VECTSP_5:14
 (0).M + (Omega).M = the VectSpStr of M & (Omega).
M + (0).M = the VectSpStr of M;

theorem :: VECTSP_5:15
 (Omega).M + W = the VectSpStr of M & W + (Omega).M = the VectSpStr of M;

theorem :: VECTSP_5:16
   for M being strict Abelian add-associative right_zeroed
               right_complementable VectSp-like (non empty VectSpStr over GF)
 holds (Omega).M + (Omega).M = M;

theorem :: VECTSP_5:17
   for W being strict Subspace of M
 holds W /\ W = W;

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

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

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

theorem :: VECTSP_5:21
 (for W1 being strict Subspace of M
  holds W1 is Subspace of W2 implies W1 /\ W2 = W1) &
 for W1 st W1 /\ W2 = W1 holds W1 is Subspace of W2;

theorem :: VECTSP_5:22
   W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3;

theorem :: VECTSP_5:23
   W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3;

theorem :: VECTSP_5:24
   W1 is Subspace of W2 & W1 is Subspace of W3 implies
  W1 is Subspace of W2 /\ W3;

theorem :: VECTSP_5:25
 (0).M /\ W = (0).M & W /\ (0).M = (0).M;

canceled;

theorem :: VECTSP_5:27
 for W being strict Subspace of M
 holds (Omega).M /\ W = W & W /\ (Omega).M = W;

theorem :: VECTSP_5:28
   for M being strict Abelian add-associative right_zeroed
              right_complementable VectSp-like (non empty VectSpStr over GF)
 holds (Omega).M /\ (Omega).M = M;

theorem :: VECTSP_5:29
   W1 /\ W2 is Subspace of W1 + W2;

theorem :: VECTSP_5:30
 for W2 being strict Subspace of M
 holds (W1 /\ W2) + W2 = W2;

theorem :: VECTSP_5:31
 for W1 being strict Subspace of M
 holds W1 /\ (W1 + W2) = W1;

theorem :: VECTSP_5:32
   (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3);

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

theorem :: VECTSP_5:34
   W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3);

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

theorem :: VECTSP_5:36
 for W1 being strict Subspace of M
 holds W1 is Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

theorem :: VECTSP_5:37
   for W1,W2 being strict Subspace of M
 holds W1 + W2 = W2 iff W1 /\ W2 = W1;

theorem :: VECTSP_5:38
   for W2,W3 being strict Subspace of M
 holds W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3;

theorem :: VECTSP_5:39
   W1 is Subspace of W2 implies W1 is Subspace of W2 + W3;

theorem :: VECTSP_5:40
   W1 is Subspace of W3 & W2 is Subspace of W3 implies
       W1 + W2 is Subspace of W3;

theorem :: VECTSP_5:41
   (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;

 definition let GF; let M;
  func Subspaces(M) -> set means
:: VECTSP_5:def 3
 for x holds x in it iff ex W being strict Subspace of M st W = x;
 end;

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



canceled 2;

theorem :: VECTSP_5:44
   for M being strict Abelian add-associative right_zeroed
               right_complementable VectSp-like (non empty VectSpStr over GF)
 holds M in Subspaces(M);

definition let GF; let M; let W1,W2;
 pred M is_the_direct_sum_of W1,W2 means
:: VECTSP_5:def 4
   the VectSpStr of M = W1 + W2 & W1 /\ W2 = (0).M;
end;

 reserve F for Field;
 reserve V for VectSp of F;
 reserve W for Subspace of V;

definition let F,V,W;
 mode Linear_Compl of W -> Subspace of V means
:: VECTSP_5:def 5
   V is_the_direct_sum_of it,W;
end;

 reserve W,W1,W2 for Subspace of V;

canceled 2;

theorem :: VECTSP_5:47
   V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;

theorem :: VECTSP_5:48
 for L being Linear_Compl of W
 holds V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;

theorem :: VECTSP_5:49
 for L being Linear_Compl of W
 holds W + L = the VectSpStr of V & L + W = the VectSpStr of V;

theorem :: VECTSP_5:50
 for L being Linear_Compl of W
 holds W /\ L = (0).V & L /\ W = (0).V;

 reserve W1,W2 for Subspace of M;

theorem :: VECTSP_5:51
   M is_the_direct_sum_of W1,W2 implies M is_the_direct_sum_of W2,W1;

theorem :: VECTSP_5:52
 M is_the_direct_sum_of (0).M,(Omega).M & M is_the_direct_sum_of (Omega).
M,(0).M;

 reserve W for Subspace of V;

theorem :: VECTSP_5:53
   for L being Linear_Compl of W holds W is Linear_Compl of L;

theorem :: VECTSP_5:54
   (0).V is Linear_Compl of (Omega).V & (Omega).V is Linear_Compl of (0).V;

 reserve W1,W2 for Subspace of M;
 reserve u,u1,u2,v for Element of M;
 reserve C1 for Coset of W1;
 reserve C2 for Coset of W2;

theorem :: VECTSP_5:55
 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;

theorem :: VECTSP_5:56
 M is_the_direct_sum_of W1,W2 iff
  for C1 being Coset of W1, C2 being Coset of W2
   ex v being Element of M st C1 /\ C2 = {v};

theorem :: VECTSP_5:57
   for M being strict Abelian add-associative right_zeroed
          right_complementable VectSp-like (non empty VectSpStr over GF),
     W1,W2 being Subspace of M
 holds W1 + W2 = M iff
  for v being Element of M
   ex v1,v2 being Element of M
    st v1 in W1 & v2 in W2 & v = v1 + v2;

theorem :: VECTSP_5:58
 for v,v1,v2,u1,u2 being Element of M
 holds M 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 :: VECTSP_5:59
   M = W1 + W2 &
  (ex v st for v1,v2,u1,u2 being Element of M 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 M is_the_direct_sum_of W1,W2;

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

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

canceled 4;

theorem :: VECTSP_5:64
 M is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;

theorem :: VECTSP_5:65
 M is_the_direct_sum_of W1,W2 implies
  (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;

 reserve W for Subspace of V;

theorem :: VECTSP_5:66
   for L being Linear_Compl of W, v being Element 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 :: VECTSP_5:67
   for L being Linear_Compl of W, v being Element of V
 holds (v |-- (W,L))`1 + (v |-- (W,L))`2 = v;

theorem :: VECTSP_5:68
   for L being Linear_Compl of W, v being Element of V
 holds (v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L;

theorem :: VECTSP_5:69
   for L being Linear_Compl of W, v being Element of V
 holds (v |-- (W,L))`1 = (v |-- (L,W))`2;

theorem :: VECTSP_5:70
   for L being Linear_Compl of W, v being Element of V
 holds (v |-- (W,L))`2 = (v |-- (L,W))`1;

reserve A1,A2,B for Element of Subspaces(M),
        W1,W2 for Subspace of M;

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

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





canceled 4;

theorem :: VECTSP_5:75
 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is Lattice;

theorem :: VECTSP_5:76
 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 0_Lattice;

theorem :: VECTSP_5:77
 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 1_Lattice;

theorem :: VECTSP_5:78
 LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is 01_Lattice;

theorem :: VECTSP_5:79
   LattStr (# Subspaces(M), SubJoin(M), SubMeet(M) #) is M_Lattice;

theorem :: VECTSP_5:80
   for F being Field, V being VectSp of F
 holds LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is C_Lattice;