The abstract of the Mizar article:

On the Lattice of Subspaces of a Vector Space

by

Andrzej Iwaniuk

Received May 23, 1995

MML identifier: VECTSP_8

[ Mizar article, MML identifier index ]

environ

 vocabulary VECTSP_1, GROUP_4, LATTICES, RLSUB_2, RLSUB_1, BOOLE, GROUP_2,
      FUNCT_1, RELAT_1, RLVECT_1, SETFAM_1, BHSP_3, LATTICE3, RLVECT_3,
      GROUP_6, PRE_TOPC, INCSP_1, VECTSP_8;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1,
      STRUCT_0, VECTSP_1, PRE_TOPC, LATTICES, VECTSP_5, LATTICE3, VECTSP_4,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, VECTSP_7, MOD_2;
 constructors LATTICE4, VECTSP_5, LATTICE3, BINOP_1, VECTSP_7, MOD_2, VECTSP_2;
 clusters LATTICES, VECTSP_4, VECTSP_2, STRUCT_0, VECTSP_5, RELSET_1, SUBSET_1,
      FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

 reserve F for Field;
 reserve VS for strict VectSp of F;

definition let F, VS;
   func lattice VS -> strict bounded Lattice equals
:: VECTSP_8:def 1
           LattStr (# Subspaces(VS), SubJoin(VS), SubMeet(VS) #);
end;

definition let F,VS;
  mode SubVS-Family of VS means
:: VECTSP_8:def 2
                     for x be set st x in it holds x is Subspace of VS;
end;

definition let F,VS;
  cluster non empty SubVS-Family of VS;
end;

definition let F,VS;
  redefine func Subspaces(VS) -> non empty SubVS-Family of VS;

let X be non empty SubVS-Family of VS;
 mode Element of X -> Subspace of VS;
end;

definition
 let F,VS;
 let x be Element of Subspaces VS;
 func carr(x) -> Subset of VS means
:: VECTSP_8:def 3
  ex X being Subspace of VS st
        x=X & it = the carrier of X;
end;

reserve u,e for set;

definition let F,VS;
  func carr VS -> Function of Subspaces(VS),bool the carrier of VS means
:: VECTSP_8:def 4
    for h being Element of Subspaces(VS), H being Subspace of VS
   st h = H holds it.h = the carrier of H;
end;

theorem :: VECTSP_8:1
 for VS being strict VectSp of F
 for H being non empty Subset of Subspaces VS holds
                                  (carr VS).:H is non empty;

theorem :: VECTSP_8:2
   for VS being strict VectSp of F
 for H being strict Subspace of VS holds 0.VS in (carr VS).H;

reserve x for set;

definition let F,VS;
 let G be non empty Subset of Subspaces(VS);
 func meet G -> strict Subspace of VS means
:: VECTSP_8:def 5
     the carrier of it = meet ((carr VS).:G);
end;

theorem :: VECTSP_8:3
  Subspaces(VS) = the carrier of lattice VS;

theorem :: VECTSP_8:4
 the L_meet of lattice VS = SubMeet(VS);

 theorem :: VECTSP_8:5
  the L_join of lattice VS = SubJoin(VS);

theorem :: VECTSP_8:6
 for VS being strict VectSp of F,
     p,q being Element of lattice VS,
     H1,H2 being strict Subspace of VS st p=H1 & q=H2
 holds p [= q iff the carrier of H1 c= the carrier of H2;

theorem :: VECTSP_8:7
  for VS being strict VectSp of F,
     p,q being Element of lattice VS,
     H1,H2 being Subspace of VS st p=H1 & q=H2
     holds p"\/"q = H1+H2;

theorem :: VECTSP_8:8
  for VS being strict VectSp of F,
     p,q being Element of lattice VS,
     H1,H2 being Subspace of VS st p=H1 & q=H2
     holds p"/\"q = H1 /\ H2;

definition let L be non empty LattStr;
 redefine attr L is complete means
:: VECTSP_8:def 6
    for X being Subset of L
   ex a being Element of L
    st a is_less_than X &
     for b being Element of L
      st b is_less_than X holds b [= a;
end;

reserve Z1 for set;

theorem :: VECTSP_8:9
        for VS holds lattice VS is complete;

theorem :: VECTSP_8:10
   for x being set
   for VS being strict VectSp of F
   for S being Subset of VS st
                        S is non empty & S is lineary-closed holds
          x in Lin S implies x in S;

definition
 let F be Field;
 let A,B be strict VectSp of F;
 let f be Function of the carrier of A,the carrier of B;
  func FuncLatt f -> Function of the carrier of lattice A,
                                the carrier of lattice B means
:: VECTSP_8:def 7
  for S being strict Subspace of A, B0 being Subset of B
            st B0 = f.:the carrier of S
                                         holds it.S = Lin B0;
 end;

definition
 let L1, L2 be Lattice;
 mode Semilattice-Homomorphism of L1,L2 ->
 Function of the carrier of L1, the carrier of L2 means
:: VECTSP_8:def 8
   for a, b being Element of L1 holds
                              it.(a "/\" b) = it.a "/\" it.b;
end;

definition
 let L1, L2 be Lattice;
 mode sup-Semilattice-Homomorphism of L1, L2 ->
 Function of the carrier of L1, the carrier of L2 means
:: VECTSP_8:def 9
    for a, b being Element of L1 holds
                              it.(a "\/" b) = it.a "\/" it.b;
end;

theorem :: VECTSP_8:11
    for L1,L2 being Lattice
  for f being Function of the carrier of L1, the carrier of L2 holds
      f is Homomorphism of L1, L2 iff
       f is sup-Semilattice-Homomorphism of L1, L2 &
       f is Semilattice-Homomorphism of L1, L2;

theorem :: VECTSP_8:12
 for F being Field
 for A,B being strict VectSp of F
 for f be map of A, B st f is linear holds
   FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B;

theorem :: VECTSP_8:13
   for F being Field
 for A,B being strict VectSp of F
 for f be map of A,B st f is one-to-one linear holds
            FuncLatt f is Homomorphism of lattice A, lattice B;

theorem :: VECTSP_8:14
   for A,B being strict VectSp of F
 for f being map of A, B st
  f is linear & f is one-to-one holds FuncLatt f is one-to-one;

theorem :: VECTSP_8:15
   for A being strict VectSp of F holds
               FuncLatt id the carrier of A = id the carrier of lattice A;