let F be Field; :: thesis: for VS being strict VectSp of F holds lattice VS is complete

let VS be strict VectSp of F; :: thesis: lattice VS is complete

let Y be Subset of (lattice VS); :: according to VECTSP_8:def 6 :: thesis: ex a being Element of (lattice VS) st

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

let VS be strict VectSp of F; :: thesis: lattice VS is complete

let Y be Subset of (lattice VS); :: according to VECTSP_8:def 6 :: thesis: ex a being Element of (lattice VS) st

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

per cases
( Y = {} or Y <> {} )
;

end;

suppose A1:
Y = {}
; :: thesis: ex a being Element of (lattice VS) st

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

thus
ex a being Element of (lattice VS) st

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) ) :: thesis: verum

end;( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) ) :: thesis: verum

proof

take
Top (lattice VS)
; :: thesis: ( Top (lattice VS) is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= Top (lattice VS) ) )

thus Top (lattice VS) is_less_than Y by A1; :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds

b [= Top (lattice VS)

let b be Element of (lattice VS); :: thesis: ( b is_less_than Y implies b [= Top (lattice VS) )

assume b is_less_than Y ; :: thesis: b [= Top (lattice VS)

thus b [= Top (lattice VS) by LATTICES:19; :: thesis: verum

end;b [= Top (lattice VS) ) )

thus Top (lattice VS) is_less_than Y by A1; :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds

b [= Top (lattice VS)

let b be Element of (lattice VS); :: thesis: ( b is_less_than Y implies b [= Top (lattice VS) )

assume b is_less_than Y ; :: thesis: b [= Top (lattice VS)

thus b [= Top (lattice VS) by LATTICES:19; :: thesis: verum

suppose
Y <> {}
; :: thesis: ex a being Element of (lattice VS) st

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= a ) )

then reconsider X = Y as non empty Subset of (Subspaces VS) ;

reconsider p = meet X as Element of (lattice VS) by VECTSP_5:def 3;

take p ; :: thesis: ( p is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= p ) )

set x = the Element of X;

thus p is_less_than Y :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds

b [= p

consider H being strict Subspace of VS such that

A4: H = r by VECTSP_5:def 3;

assume A5: r is_less_than Y ; :: thesis: r [= p

A6: for Z1 being set st Z1 in (carr VS) .: X holds

the carrier of H c= Z1

then the carrier of H c= meet ((carr VS) .: X) by A6, SETFAM_1:5;

then the carrier of H c= the carrier of (meet X) by Def5;

hence r [= p by A4, Th6; :: thesis: verum

end;reconsider p = meet X as Element of (lattice VS) by VECTSP_5:def 3;

take p ; :: thesis: ( p is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds

b [= p ) )

set x = the Element of X;

thus p is_less_than Y :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds

b [= p

proof

let r be Element of (lattice VS); :: thesis: ( r is_less_than Y implies r [= p )
let q be Element of (lattice VS); :: according to LATTICE3:def 16 :: thesis: ( not q in Y or p [= q )

consider H being strict Subspace of VS such that

A2: H = q by VECTSP_5:def 3;

reconsider h = q as Element of Subspaces VS ;

assume A3: q in Y ; :: thesis: p [= q

(carr VS) . h = the carrier of H by A2, Def4;

then meet ((carr VS) .: X) c= the carrier of H by A3, FUNCT_2:35, SETFAM_1:3;

then the carrier of (meet X) c= the carrier of H by Def5;

hence p [= q by A2, Th6; :: thesis: verum

end;consider H being strict Subspace of VS such that

A2: H = q by VECTSP_5:def 3;

reconsider h = q as Element of Subspaces VS ;

assume A3: q in Y ; :: thesis: p [= q

(carr VS) . h = the carrier of H by A2, Def4;

then meet ((carr VS) .: X) c= the carrier of H by A3, FUNCT_2:35, SETFAM_1:3;

then the carrier of (meet X) c= the carrier of H by Def5;

hence p [= q by A2, Th6; :: thesis: verum

consider H being strict Subspace of VS such that

A4: H = r by VECTSP_5:def 3;

assume A5: r is_less_than Y ; :: thesis: r [= p

A6: for Z1 being set st Z1 in (carr VS) .: X holds

the carrier of H c= Z1

proof

(carr VS) . the Element of X in (carr VS) .: X
by FUNCT_2:35;
let Z1 be set ; :: thesis: ( Z1 in (carr VS) .: X implies the carrier of H c= Z1 )

assume A7: Z1 in (carr VS) .: X ; :: thesis: the carrier of H c= Z1

then reconsider Z2 = Z1 as Subset of VS ;

consider z1 being Element of Subspaces VS such that

A8: z1 in X and

A9: Z2 = (carr VS) . z1 by A7, FUNCT_2:65;

reconsider z1 = z1 as Element of (lattice VS) ;

A10: r [= z1 by A5, A8;

consider z3 being strict Subspace of VS such that

A11: z3 = z1 by VECTSP_5:def 3;

Z1 = the carrier of z3 by A9, A11, Def4;

hence the carrier of H c= Z1 by A4, A11, A10, Th6; :: thesis: verum

end;assume A7: Z1 in (carr VS) .: X ; :: thesis: the carrier of H c= Z1

then reconsider Z2 = Z1 as Subset of VS ;

consider z1 being Element of Subspaces VS such that

A8: z1 in X and

A9: Z2 = (carr VS) . z1 by A7, FUNCT_2:65;

reconsider z1 = z1 as Element of (lattice VS) ;

A10: r [= z1 by A5, A8;

consider z3 being strict Subspace of VS such that

A11: z3 = z1 by VECTSP_5:def 3;

Z1 = the carrier of z3 by A9, A11, Def4;

hence the carrier of H c= Z1 by A4, A11, A10, Th6; :: thesis: verum

then the carrier of H c= meet ((carr VS) .: X) by A6, SETFAM_1:5;

then the carrier of H c= the carrier of (meet X) by Def5;

hence r [= p by A4, Th6; :: thesis: verum