:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
::
:: Copyright (c) 1995-2018 Association of Mizar Users

definition
let F be Field;
let VS be strict VectSp of F;
func lattice VS -> strict bounded Lattice equals :: VECTSP_8:def 1
LattStr(# (),(SubJoin VS),(SubMeet VS) #);
coherence
LattStr(# (),(SubJoin VS),(SubMeet VS) #) is strict bounded Lattice
by VECTSP_5:60;
end;

:: deftheorem defines lattice VECTSP_8:def 1 :
for F being Field
for VS being strict VectSp of F holds lattice VS = LattStr(# (),(SubJoin VS),(SubMeet VS) #);

definition
let F be Field;
let VS be strict VectSp of F;
mode SubVS-Family of VS -> set means :Def2: :: VECTSP_8:def 2
for x being set st x in it holds
x is Subspace of VS;
existence
ex b1 being set st
for x being set st x in b1 holds
x is Subspace of VS
proof end;
end;

:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :
for F being Field
for VS being strict VectSp of F
for b3 being set holds
( b3 is SubVS-Family of VS iff for x being set st x in b3 holds
x is Subspace of VS );

registration
let F be Field;
let VS be strict VectSp of F;
cluster non empty for SubVS-Family of VS;
existence
not for b1 being SubVS-Family of VS holds b1 is empty
proof end;
end;

definition
let F be Field;
let VS be strict VectSp of F;
:: original: Subspaces
redefine func Subspaces VS -> non empty SubVS-Family of VS;
coherence
Subspaces VS is non empty SubVS-Family of VS
proof end;
let X be non empty SubVS-Family of VS;
:: original: Element
redefine mode Element of X -> Subspace of VS;
coherence
for b1 being Element of X holds b1 is Subspace of VS
by Def2;
end;

definition
let F be Field;
let VS be strict VectSp of F;
let x be Element of Subspaces VS;
func carr x -> Subset of VS means :Def3: :: VECTSP_8:def 3
ex X being Subspace of VS st
( x = X & it = the carrier of X );
existence
ex b1 being Subset of VS ex X being Subspace of VS st
( x = X & b1 = the carrier of X )
proof end;
uniqueness
for b1, b2 being Subset of VS st ex X being Subspace of VS st
( x = X & b1 = the carrier of X ) & ex X being Subspace of VS st
( x = X & b2 = the carrier of X ) holds
b1 = b2
;
end;

:: deftheorem Def3 defines carr VECTSP_8:def 3 :
for F being Field
for VS being strict VectSp of F
for x being Element of Subspaces VS
for b4 being Subset of VS holds
( b4 = carr x iff ex X being Subspace of VS st
( x = X & b4 = the carrier of X ) );

definition
let F be Field;
let VS be strict VectSp of F;
func carr VS -> Function of (),(bool the carrier of VS) means :Def4: :: VECTSP_8:def 4
for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
it . h = the carrier of H;
existence
ex b1 being Function of (),(bool the carrier of VS) st
for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H
proof end;
uniqueness
for b1, b2 being Function of (),(bool the carrier of VS) st ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H ) & ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b2 . h = the carrier of H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines carr VECTSP_8:def 4 :
for F being Field
for VS being strict VectSp of F
for b3 being Function of (),(bool the carrier of VS) holds
( b3 = carr VS iff for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b3 . h = the carrier of H );

theorem Th1: :: VECTSP_8:1
for F being Field
for VS being strict VectSp of F
for H being non empty Subset of () holds not (carr VS) .: H is empty
proof end;

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

definition
let F be Field;
let VS be strict VectSp of F;
let G be non empty Subset of ();
func meet G -> strict Subspace of VS means :Def5: :: VECTSP_8:def 5
the carrier of it = meet ((carr VS) .: G);
existence
ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G)
proof end;
uniqueness
for b1, b2 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G) & the carrier of b2 = meet ((carr VS) .: G) holds
b1 = b2
by VECTSP_4:29;
end;

:: deftheorem Def5 defines meet VECTSP_8:def 5 :
for F being Field
for VS being strict VectSp of F
for G being non empty Subset of ()
for b4 being strict Subspace of VS holds
( b4 = meet G iff the carrier of b4 = meet ((carr VS) .: G) );

theorem :: VECTSP_8:3
for F being Field
for VS being strict VectSp of F holds Subspaces VS = the carrier of (lattice VS) ;

theorem :: VECTSP_8:4
for F being Field
for VS being strict VectSp of F holds the L_meet of (lattice VS) = SubMeet VS ;

theorem :: VECTSP_8:5
for F being Field
for VS being strict VectSp of F holds the L_join of (lattice VS) = SubJoin VS ;

theorem Th6: :: VECTSP_8:6
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for 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 )
proof end;

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

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

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 ) );
compatibility
( L is complete iff 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 ) ) )
proof end;
end;

:: deftheorem defines complete VECTSP_8:def 6 :
for L being non empty LattStr holds
( L is complete iff 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 ) ) );

theorem :: VECTSP_8:9
for F being Field
for VS being strict VectSp of F holds lattice VS is complete
proof end;

theorem Th10: :: VECTSP_8:10
for F being Field
for x being object
for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
proof end;

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 (), the carrier of () means :Def7: :: VECTSP_8:def 7
for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
it . S = Lin B0;
existence
ex b1 being Function of the carrier of (), the carrier of () st
for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0
proof end;
uniqueness
for b1, b2 being Function of the carrier of (), the carrier of () st ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0 ) & ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b2 . S = Lin B0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :
for F being Field
for A, B being strict VectSp of F
for f being Function of the carrier of A, the carrier of B
for b5 being Function of the carrier of (), the carrier of () holds
( b5 = FuncLatt f iff for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b5 . S = Lin B0 );

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

:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :
for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "/\" b) = (b3 . a) "/\" (b3 . b) );

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

:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def 9 :
for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is sup-Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "\/" b) = (b3 . a) "\/" (b3 . b) );

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 ) )
proof end;

theorem Th12: :: VECTSP_8:12
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
proof end;

theorem :: VECTSP_8:13
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of lattice A, lattice B
proof end;

theorem :: VECTSP_8:14
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
proof end;

theorem :: VECTSP_8:15
for F being Field
for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of ()
proof end;