let Q be Quantale; :: thesis: for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds

ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

let j be UnOp of Q; :: thesis: ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) )

assume A1: ( j is monotone & j is idempotent & j is \/-distributive ) ; :: thesis: ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

reconsider D = rng j as non empty Subset of Q ;

dom j = H_{1}(Q)
by FUNCT_2:def 1;

then reconsider j9 = j as Function of H_{1}(Q),D by RELSET_1:4;

deffunc H_{5}( Subset of D) -> Element of D = j9 . ("\/" ($1,Q));

consider f being Function of (bool D),D such that

A2: for X being Subset of D holds f . X = H_{5}(X)
from FUNCT_2:sch 4();

A3: dom f = bool D by FUNCT_2:def 1;

A4: for X being Subset-Family of D holds f . (f .: X) = f . (union X)

A23: H_{1}(L) = D
and

A24: for X being Subset of L holds "\/" X = f . X by A4, LATTICE3:55;

take L ; :: thesis: ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

thus H_{1}(L) = rng j
by A23; :: thesis: for X being Subset of L holds "\/" X = j . ("\/" (X,Q))

let X be Subset of L; :: thesis: "\/" X = j . ("\/" (X,Q))

thus "\/" X = f . X by A24

.= j . ("\/" (X,Q)) by A2, A23 ; :: thesis: verum

ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

let j be UnOp of Q; :: thesis: ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) )

assume A1: ( j is monotone & j is idempotent & j is \/-distributive ) ; :: thesis: ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

reconsider D = rng j as non empty Subset of Q ;

dom j = H

then reconsider j9 = j as Function of H

deffunc H

consider f being Function of (bool D),D such that

A2: for X being Subset of D holds f . X = H

A3: dom f = bool D by FUNCT_2:def 1;

A4: for X being Subset-Family of D holds f . (f .: X) = f . (union X)

proof

for a being Element of D holds f . {a} = a
let X be Subset-Family of D; :: thesis: f . (f .: X) = f . (union X)

set A = { (j . a) where a is Element of Q : a in f .: X } ;

set B = { (j . b) where b is Element of Q : b in union X } ;

reconsider Y = f .: X, X9 = union X as Subset of Q by XBOOLE_1:1;

{ (j . a) where a is Element of Q : a in f .: X } is_less_than "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)

thus f . (f .: X) = j . ("\/" Y) by A2

.= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by A1, Th10

.= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A20, A11, LATTICES:8

.= j . ("\/" X9) by A1, Th10

.= f . (union X) by A2 ; :: thesis: verum

end;set A = { (j . a) where a is Element of Q : a in f .: X } ;

set B = { (j . b) where b is Element of Q : b in union X } ;

reconsider Y = f .: X, X9 = union X as Subset of Q by XBOOLE_1:1;

now :: thesis: for a being Element of Q st a in { (j . b) where b is Element of Q : b in union X } holds

ex b being Element of the carrier of Q st

( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

then A11:
"\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) [= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q)
by LATTICE3:47;ex b being Element of the carrier of Q st

( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

let a be Element of Q; :: thesis: ( a in { (j . b) where b is Element of Q : b in union X } implies ex b being Element of the carrier of Q st

( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) )

assume a in { (j . b) where b is Element of Q : b in union X } ; :: thesis: ex b being Element of the carrier of Q st

( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

then consider b9 being Element of Q such that

A5: a = j . b9 and

A6: b9 in union X ;

consider Y being set such that

A7: b9 in Y and

A8: Y in X by A6, TARSKI:def 4;

reconsider Y = Y as Subset of D by A8;

A9: b9 [= "\/" (Y,Q) by A7, LATTICE3:38;

take b = j . ("\/" (Y,Q)); :: thesis: ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

b = f . Y by A2;

then A10: b in f .: X by A3, A8, FUNCT_1:def 6;

j . b = b by A1, Lm1;

hence ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) by A1, A5, A10, A9; :: thesis: verum

end;( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) )

assume a in { (j . b) where b is Element of Q : b in union X } ; :: thesis: ex b being Element of the carrier of Q st

( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

then consider b9 being Element of Q such that

A5: a = j . b9 and

A6: b9 in union X ;

consider Y being set such that

A7: b9 in Y and

A8: Y in X by A6, TARSKI:def 4;

reconsider Y = Y as Subset of D by A8;

A9: b9 [= "\/" (Y,Q) by A7, LATTICE3:38;

take b = j . ("\/" (Y,Q)); :: thesis: ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

b = f . Y by A2;

then A10: b in f .: X by A3, A8, FUNCT_1:def 6;

j . b = b by A1, Lm1;

hence ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) by A1, A5, A10, A9; :: thesis: verum

{ (j . a) where a is Element of Q : a in f .: X } is_less_than "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)

proof

then A20:
"\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)
by LATTICE3:def 21;
let a be Element of Q; :: according to LATTICE3:def 17 :: thesis: ( not a in { (j . a) where a is Element of Q : a in f .: X } or a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) )

assume a in { (j . a) where a is Element of Q : a in f .: X } ; :: thesis: a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)

then consider a9 being Element of Q such that

A12: a = j . a9 and

A13: a9 in f .: X ;

consider x being object such that

A14: x in dom f and

A15: x in X and

A16: a9 = f . x by A13, FUNCT_1:def 6;

reconsider x = x as Subset of D by A14;

reconsider Y = x as Subset of Q by XBOOLE_1:1;

A17: { (j . b) where b is Element of Q : b in Y } c= { (j . b) where b is Element of Q : b in union X }

then a9 = "\/" ( { (j . b) where b is Element of Q : b in Y } ,Q) by A1, Th10;

then a9 [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A17, LATTICE3:45;

then a [= j . ("\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)) by A1, A12;

then a [= j . (j . ("\/" X9)) by A1, Th10;

then a [= j . ("\/" X9) by A1, Lm1;

hence a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A1, Th10; :: thesis: verum

end;assume a in { (j . a) where a is Element of Q : a in f .: X } ; :: thesis: a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)

then consider a9 being Element of Q such that

A12: a = j . a9 and

A13: a9 in f .: X ;

consider x being object such that

A14: x in dom f and

A15: x in X and

A16: a9 = f . x by A13, FUNCT_1:def 6;

reconsider x = x as Subset of D by A14;

reconsider Y = x as Subset of Q by XBOOLE_1:1;

A17: { (j . b) where b is Element of Q : b in Y } c= { (j . b) where b is Element of Q : b in union X }

proof

a9 = j . ("\/" Y)
by A2, A16;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (j . b) where b is Element of Q : b in Y } or z in { (j . b) where b is Element of Q : b in union X } )

assume z in { (j . b) where b is Element of Q : b in Y } ; :: thesis: z in { (j . b) where b is Element of Q : b in union X }

then consider b being Element of Q such that

A18: z = j . b and

A19: b in Y ;

b in union X by A15, A19, TARSKI:def 4;

hence z in { (j . b) where b is Element of Q : b in union X } by A18; :: thesis: verum

end;assume z in { (j . b) where b is Element of Q : b in Y } ; :: thesis: z in { (j . b) where b is Element of Q : b in union X }

then consider b being Element of Q such that

A18: z = j . b and

A19: b in Y ;

b in union X by A15, A19, TARSKI:def 4;

hence z in { (j . b) where b is Element of Q : b in union X } by A18; :: thesis: verum

then a9 = "\/" ( { (j . b) where b is Element of Q : b in Y } ,Q) by A1, Th10;

then a9 [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A17, LATTICE3:45;

then a [= j . ("\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)) by A1, A12;

then a [= j . (j . ("\/" X9)) by A1, Th10;

then a [= j . ("\/" X9) by A1, Lm1;

hence a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A1, Th10; :: thesis: verum

thus f . (f .: X) = j . ("\/" Y) by A2

.= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by A1, Th10

.= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A20, A11, LATTICES:8

.= j . ("\/" X9) by A1, Th10

.= f . (union X) by A2 ; :: thesis: verum

proof

then consider L being strict complete Lattice such that
let a be Element of D; :: thesis: f . {a} = a

consider a9 being object such that

A21: a9 in dom j and

A22: a = j . a9 by FUNCT_1:def 3;

reconsider x = a as Element of Q ;

reconsider x9 = {x} as Subset of Q ;

reconsider a9 = a9 as Element of Q by A21;

thus f . {a} = j . ("\/" x9) by A2

.= j . (j . a9) by A22, LATTICE3:42

.= a by A1, A22, Lm1 ; :: thesis: verum

end;consider a9 being object such that

A21: a9 in dom j and

A22: a = j . a9 by FUNCT_1:def 3;

reconsider x = a as Element of Q ;

reconsider x9 = {x} as Subset of Q ;

reconsider a9 = a9 as Element of Q by A21;

thus f . {a} = j . ("\/" x9) by A2

.= j . (j . a9) by A22, LATTICE3:42

.= a by A1, A22, Lm1 ; :: thesis: verum

A23: H

A24: for X being Subset of L holds "\/" X = f . X by A4, LATTICE3:55;

take L ; :: thesis: ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

thus H

let X be Subset of L; :: thesis: "\/" X = j . ("\/" (X,Q))

thus "\/" X = f . X by A24

.= j . ("\/" (X,Q)) by A2, A23 ; :: thesis: verum