:: by Andrzej Iwaniuk

::

:: Received May 23, 1995

:: Copyright (c) 1995-2016 Association of Mizar Users

definition

let F be Field;

let VS be strict VectSp of F;

LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #) is strict bounded Lattice by VECTSP_5:60;

end;
let VS be strict VectSp of F;

func lattice VS -> strict bounded Lattice equals :: VECTSP_8:def 1

LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

coherence LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #) is strict bounded Lattice by VECTSP_5:60;

:: deftheorem defines lattice VECTSP_8:def 1 :

for F being Field

for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

for F being Field

for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

definition

let F be Field;

let VS be strict VectSp of F;

ex b_{1} being set st

for x being set st x in b_{1} holds

x is Subspace of VS

end;
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 for x being set st x in it holds

x is Subspace of VS;

ex b

for x being set st x in b

x is Subspace of VS

proof end;

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

for F being Field

for VS being strict VectSp of F

for b_{3} being set holds

( b_{3} is SubVS-Family of VS iff for x being set st x in b_{3} holds

x is Subspace of VS );

for F being Field

for VS being strict VectSp of F

for b

( b

x is Subspace of VS );

registration

let F be Field;

let VS be strict VectSp of F;

existence

not for b_{1} being SubVS-Family of VS holds b_{1} is empty

end;
let VS be strict VectSp of F;

existence

not for b

proof 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

:: original: Element

redefine mode Element of X -> Subspace of VS;

coherence

for b_{1} being Element of X holds b_{1} is Subspace of VS
by Def2;

end;
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 b

definition

let F be Field;

let VS be strict VectSp of F;

let x be Element of Subspaces VS;

ex b_{1} being Subset of VS ex X being Subspace of VS st

( x = X & b_{1} = the carrier of X )

for b_{1}, b_{2} being Subset of VS st ex X being Subspace of VS st

( x = X & b_{1} = the carrier of X ) & ex X being Subspace of VS st

( x = X & b_{2} = the carrier of X ) holds

b_{1} = b_{2}
;

end;
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 X being Subspace of VS st

( x = X & it = the carrier of X );

ex b

( x = X & b

proof end;

uniqueness for b

( x = X & b

( x = X & b

b

:: 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 b_{4} being Subset of VS holds

( b_{4} = carr x iff ex X being Subspace of VS st

( x = X & b_{4} = the carrier of X ) );

for F being Field

for VS being strict VectSp of F

for x being Element of Subspaces VS

for b

( b

( x = X & b

definition

let F be Field;

let VS be strict VectSp of F;

ex b_{1} being Function of (Subspaces VS),(bool the carrier of VS) st

for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

b_{1} . h = the carrier of H

for b_{1}, b_{2} being Function of (Subspaces VS),(bool the carrier of VS) st ( for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

b_{1} . h = the carrier of H ) & ( for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

b_{2} . h = the carrier of H ) holds

b_{1} = b_{2}

end;
let VS be strict VectSp of F;

func carr VS -> Function of (Subspaces VS),(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 for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

it . h = the carrier of H;

ex b

for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

b

proof end;

uniqueness for b

for H being Subspace of VS st h = H holds

b

for H being Subspace of VS st h = H holds

b

b

proof end;

:: deftheorem Def4 defines carr VECTSP_8:def 4 :

for F being Field

for VS being strict VectSp of F

for b_{3} being Function of (Subspaces VS),(bool the carrier of VS) holds

( b_{3} = carr VS iff for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

b_{3} . h = the carrier of H );

for F being Field

for VS being strict VectSp of F

for b

( b

for H being Subspace of VS st h = H holds

b

theorem Th1: :: VECTSP_8:1

for F being Field

for VS being strict VectSp of F

for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty

for VS being strict VectSp of F

for H being non empty Subset of (Subspaces VS) 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

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 (Subspaces VS);

ex b_{1} being strict Subspace of VS st the carrier of b_{1} = meet ((carr VS) .: G)

for b_{1}, b_{2} being strict Subspace of VS st the carrier of b_{1} = meet ((carr VS) .: G) & the carrier of b_{2} = meet ((carr VS) .: G) holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
let VS be strict VectSp of F;

let G be non empty Subset of (Subspaces VS);

func meet G -> strict Subspace of VS means :Def5: :: VECTSP_8:def 5

the carrier of it = meet ((carr VS) .: G);

existence the carrier of it = meet ((carr VS) .: G);

ex b

proof end;

uniqueness for b

b

:: 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 (Subspaces VS)

for b_{4} being strict Subspace of VS holds

( b_{4} = meet G iff the carrier of b_{4} = meet ((carr VS) .: G) );

for F being Field

for VS being strict VectSp of F

for G being non empty Subset of (Subspaces VS)

for b

( b

theorem :: VECTSP_8:3

theorem :: VECTSP_8:4

theorem :: VECTSP_8:5

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 )

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

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

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 ;

( 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 ) ) )

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

( 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;

:: 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 ) ) );

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 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

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;

ex b_{1} being Function of the carrier of (lattice A), the carrier of (lattice B) st

for S being strict Subspace of A

for B0 being Subset of B st B0 = f .: the carrier of S holds

b_{1} . S = Lin B0

for b_{1}, b_{2} being Function of the carrier of (lattice A), the carrier of (lattice B) st ( for S being strict Subspace of A

for B0 being Subset of B st B0 = f .: the carrier of S holds

b_{1} . S = Lin B0 ) & ( for S being strict Subspace of A

for B0 being Subset of B st B0 = f .: the carrier of S holds

b_{2} . S = Lin B0 ) holds

b_{1} = b_{2}

end;
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 :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 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;

ex b

for S being strict Subspace of A

for B0 being Subset of B st B0 = f .: the carrier of S holds

b

proof end;

uniqueness for b

for B0 being Subset of B st B0 = f .: the carrier of S holds

b

for B0 being Subset of B st B0 = f .: the carrier of S holds

b

b

proof 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 b_{5} being Function of the carrier of (lattice A), the carrier of (lattice B) holds

( b_{5} = FuncLatt f iff for S being strict Subspace of A

for B0 being Subset of B st B0 = f .: the carrier of S holds

b_{5} . S = Lin B0 );

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 b

( b

for B0 being Subset of B st B0 = f .: the carrier of S holds

b

definition

let L1, L2 be Lattice;

ex b_{1} being Function of the carrier of L1, the carrier of L2 st

for a, b being Element of L1 holds b_{1} . (a "/\" b) = (b_{1} . a) "/\" (b_{1} . b)

end;
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 for a, b being Element of L1 holds it . (a "/\" b) = (it . a) "/\" (it . b);

ex b

for a, b being Element of L1 holds b

proof end;

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

for L1, L2 being Lattice

for b_{3} being Function of the carrier of L1, the carrier of L2 holds

( b_{3} is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b_{3} . (a "/\" b) = (b_{3} . a) "/\" (b_{3} . b) );

for L1, L2 being Lattice

for b

( b

definition

let L1, L2 be Lattice;

ex b_{1} being Function of the carrier of L1, the carrier of L2 st

for a, b being Element of L1 holds b_{1} . (a "\/" b) = (b_{1} . a) "\/" (b_{1} . b)

end;
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 for a, b being Element of L1 holds it . (a "\/" b) = (it . a) "\/" (it . b);

ex b

for a, b being Element of L1 holds b

proof end;

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

for L1, L2 being Lattice

for b_{3} being Function of the carrier of L1, the carrier of L2 holds

( b_{3} is sup-Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b_{3} . (a "\/" b) = (b_{3} . a) "\/" (b_{3} . b) );

for L1, L2 being Lattice

for b

( 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 ) )

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

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

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

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 (lattice A)

for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of (lattice A)

proof end;