:: VECTSP_8 semantic presentation

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
func lattice c₂ -> strict bounded Lattice equals :: VECTSP_8:def 1
LattStr(# (Subspaces a₂),(SubJoin a₂),(SubMeet a₂) #);
coherence by VECTSP_5:78;

end;

:: deftheorem Def1 defines lattice VECTSP_8:def 1 :

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
mode SubVS-Family of c₂ -> set means :Def2: :: VECTSP_8:def 2
for b₁ being set st b₁ in a₃ holds
b₁ is Subspace of a₂;
existence

proof end;

end;

:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :

registration

let c₁ be Field;
let c₂ be strict VectSp of c₁;
cluster non empty SubVS-Family of a₂;
existence

proof end;

end;

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
redefine func Subspaces as Subspaces c₂ -> non empty SubVS-Family of a₂;
coherence

proof end;

let c₃ be non empty SubVS-Family of c₂;
redefine mode Element as Element of c₃ -> Subspace of a₂;
coherence by Def2;

end;

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
let c₃ be Element of Subspaces c₂;
func carr c₃ -> Subset of a₂ means :Def3: :: VECTSP_8:def 3
ex b₁ being Subspace of a₂ st
( a₃ = b₁ & a₄ = the carrier of b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines carr VECTSP_8:def 3 :

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
func carr c₂ -> Function of Subspaces a₂, bool the carrier of a₂ means :Def4: :: VECTSP_8:def 4
for b₁ being Element of Subspaces a₂
for b₂ being Subspace of a₂ st b₁ = b₂ holds
a₃ . b₁ = the carrier of b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines carr VECTSP_8:def 4 :

theorem Th1: :: VECTSP_8:1

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃ being non empty Subset of (Subspaces b₂) holds not (carr b₂) .: b₃ is empty

proof end;

theorem Th2: :: VECTSP_8:2

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃ being strict Subspace of b₂ holds 0. b₂ in (carr b₂) . b₃

proof end;

definition

let c₁ be Field;
let c₂ be strict VectSp of c₁;
let c₃ be non empty Subset of (Subspaces c₂);
func meet c₃ -> strict Subspace of a₂ means :Def5: :: VECTSP_8:def 5
the carrier of a₄ = meet ((carr a₂) .: a₃);
existence

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def5 defines meet VECTSP_8:def 5 :

theorem Th3: :: VECTSP_8:3

for b₁ being Field
for b₂ being strict VectSp of b₁ holds Subspaces b₂ = the carrier of (lattice b₂) ;

theorem Th4: :: VECTSP_8:4

for b₁ being Field
for b₂ being strict VectSp of b₁ holds the L_meet of (lattice b₂) = SubMeet b₂ ;

theorem Th5: :: VECTSP_8:5

for b₁ being Field
for b₂ being strict VectSp of b₁ holds the L_join of (lattice b₂) = SubJoin b₂ ;

theorem Th6: :: VECTSP_8:6

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃, b₄ being Element of (lattice b₂)
for b₅, b₆ being strict Subspace of b₂ st b₃ = b₅ & b₄ = b₆ holds
( b₃ [= b₄ iff the carrier of b₅ c= the carrier of b₆ )

proof end;

theorem Th7: :: VECTSP_8:7

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃, b₄ being Element of (lattice b₂)
for b₅, b₆ being Subspace of b₂ st b₃ = b₅ & b₄ = b₆ holds
b₃ "\/" b₄ = b₅ + b₆

proof end;

theorem Th8: :: VECTSP_8:8

for b₁ being Field
for b₂ being strict VectSp of b₁
for b₃, b₄ being Element of (lattice b₂)
for b₅, b₆ being Subspace of b₂ st b₃ = b₅ & b₄ = b₆ holds
b₃ "/\" b₄ = b₅ /\ b₆

proof end;

definition

let c₁ be non empty LattStr ;
redefine attr a₁ is complete means :: VECTSP_8:def 6
for b₁ being Subset of a₁ ex b₂ being Element of a₁ st
( b₂ is_less_than b₁ & ( for b₃ being Element of a₁ st b₃ is_less_than b₁ holds
b₃ [= b₂ ) );
compatibility

proof end;

end;

:: deftheorem Def6 defines complete VECTSP_8:def 6 :

theorem Th9: :: VECTSP_8:9

for b₁ being Field
for b₂ being strict VectSp of b₁ holds lattice b₂ is complete

proof end;

theorem Th10: :: VECTSP_8:10

for b₁ being Field
for b₂ being set
for b₃ being strict VectSp of b₁
for b₄ being Subset of b₃ st not b₄ is empty & b₄ is lineary-closed & b₂ in Lin b₄ holds
b₂ in b₄

proof end;

definition

let c₁ be Field;
let c₂, c₃ be strict VectSp of c₁;
let c₄ be Function of the carrier of c₂,the carrier of c₃;
func FuncLatt c₄ -> Function of the carrier of (lattice a₂),the carrier of (lattice a₃) means :Def7: :: VECTSP_8:def 7
for b₁ being strict Subspace of a₂
for b₂ being Subset of a₃ st b₂ = a₄ .: the carrier of b₁ holds
a₅ . b₁ = Lin b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :

definition

let c₁, c₂ be Lattice;
mode Semilattice-Homomorphism of c₁,c₂ -> Function of the carrier of a₁,the carrier of a₂ means :Def8: :: VECTSP_8:def 8
for b₁, b₂ being Element of a₁ holds a₃ . (b₁ "/\" b₂) = (a₃ . b₁) "/\" (a₃ . b₂);
existence

proof end;

end;

:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :

definition

let c₁, c₂ be Lattice;
mode sup-Semilattice-Homomorphism of c₁,c₂ -> Function of the carrier of a₁,the carrier of a₂ means :Def9: :: VECTSP_8:def 9
for b₁, b₂ being Element of a₁ holds a₃ . (b₁ "\/" b₂) = (a₃ . b₁) "\/" (a₃ . b₂);
existence

proof end;

end;

:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def 9 :

theorem Th11: :: VECTSP_8:11

for b₁, b₂ being Lattice
for b₃ being Function of the carrier of b₁,the carrier of b₂ holds
( b₃ is Homomorphism of b₁,b₂ iff ( b₃ is sup-Semilattice-Homomorphism of b₁,b₂ & b₃ is Semilattice-Homomorphism of b₁,b₂ ) )

proof end;

theorem Th12: :: VECTSP_8:12

for b₁ being Field
for b₂, b₃ being strict VectSp of b₁
for b₄ being Function of b₂,b₃ st b₄ is linear holds
FuncLatt b₄ is sup-Semilattice-Homomorphism of lattice b₂, lattice b₃

proof end;

theorem Th13: :: VECTSP_8:13

for b₁ being Field
for b₂, b₃ being strict VectSp of b₁
for b₄ being Function of b₂,b₃ st b₄ is one-to-one & b₄ is linear holds
FuncLatt b₄ is Homomorphism of lattice b₂, lattice b₃

proof end;

theorem Th14: :: VECTSP_8:14

for b₁ being Field
for b₂, b₃ being strict VectSp of b₁
for b₄ being Function of b₂,b₃ st b₄ is linear & b₄ is one-to-one holds
FuncLatt b₄ is one-to-one

proof end;

theorem Th15: :: VECTSP_8:15

for b₁ being Field
for b₂ being strict VectSp of b₁ holds FuncLatt (id the carrier of b₂) = id the carrier of (lattice b₂)

proof end;